Continuity at 0 on NNReal via 1/t: continuousWithinAt_compl_self and tendsto_inv_nhdsGT_zero

To prove ContinuousAt f 0 for f : NNReal -> R defined through 1/t (e.g. Brownian time inversion t * B(1/t), where 1/0 = 0 in Lean), rewrite with ← continuousWithinAt_compl_self, turn {0}ᶜ into Set.Ioi 0 (ext; simp [pos_iff_ne_zero]), and compose a limit at infinity with tendsto_inv_nhdsGT_zero, which holds in any linearly ordered semifield with the order topology, NNReal included. Use .congr' with filter_upwards [self_mem_nhdsWithin] with s (hs : 0 < s) to identify f s with g (s⁻¹). The same file has inv_nhdsGT_zero : (𝓝[>] 0)⁻¹ = atTop; with ← Filter.map_inv and ← limsup_comp it converts limsup over t -> 0+ into limsup over s -> infinity. Away from 0, continuousAt_const.div continuousAt_id ht works on NNReal. One gotcha: in a lambda side condition write the binder type, fun t (ht : (1 : NNReal) ≤ t) ↦ ..., or elaboration may coerce t to ℝ and you get a ↑t ≠ 0 vs t ≠ 0 mismatch.