English
For ENat, the subtraction function is continuous at (a,b) provided at least one of a,b is not ∞.
Русский
Для ENat функция вычитания непрерывна в точке (a,b), если хотя бы одно из a,b не бесконечно.
LaTeX
$$$$\\text{ContinuousAt}((\\cdot - \\cdot)\\,\\text{uncurry})(a,b)$$ при условии $a \\neq \\top$ или $b \\neq \\top$.$$
Lean4
protected theorem continuousAt_sub {a b : ℕ∞} (h : a ≠ ⊤ ∨ b ≠ ⊤) : ContinuousAt (· - ·).uncurry (a, b) := by
match a, b, h with
| (a : ℕ), (b : ℕ), _ => simp [ContinuousAt, nhds_prod_eq]
| (a : ℕ), ⊤,
_ =>
suffices ∀ᶠ b in 𝓝 ⊤, (a - b : ℕ∞) = 0 by simpa [ContinuousAt, nhds_prod_eq, tsub_eq_zero_of_le]
filter_upwards [le_mem_nhds (WithTop.coe_lt_top a)] with b using tsub_eq_zero_of_le
| ⊤, (b : ℕ),
_ =>
suffices ∀ n : ℕ, ∀ᶠ a : ℕ∞ in 𝓝 ⊤, b + n < a by
simpa [ContinuousAt, nhds_prod_eq, (· ∘ ·), lt_tsub_iff_left, tendsto_nhds_top_iff_natCast_lt]
exact fun n ↦ lt_mem_nhds <| WithTop.coe_lt_top (b + n)
