English
For ENNReal, the map (a,b) ↦ a − b is continuous at any (a,b) with not both a and b equal to ∞; i.e., if a ≠ ∞ or b ≠ ∞, then the map is continuous at (a,b).
Русский
Для ENNReal отображение (a,b) ↦ a − b непрерывно в любой точке, где не пара ∞, ∞; то есть, если a ≠ ∞ или b ≠ ∞, отображение непрерывно в точке (a,b).
LaTeX
$$$\\\\forall a,b : ENNReal, \\\\ (a \\\\neq \\\\infty \\,\\\\lor \\\\ b \\\\neq \\\\infty) \\\\Rightarrow \\\\text{Tendsto } (\\\\lambda p: ENNReal \\\\times ENNReal, p.1 - p.2) (\\\\mathit{nhds} (a,b)) (\\\\mathit{nhds} (a-b)).$$$
Lean4
theorem tendsto_sub :
∀ {a b : ℝ≥0∞}, (a ≠ ∞ ∨ b ≠ ∞) → Tendsto (fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 - p.2) (𝓝 (a, b)) (𝓝 (a - b))
| ∞, ∞, h => by simp only [ne_eq, not_true_eq_false, or_self] at h
| ∞, (b : ℝ≥0), _ => by
rw [top_sub_coe, tendsto_nhds_top_iff_nnreal]
refine fun x =>
((lt_mem_nhds <| @coe_lt_top (b + 1 + x)).prod_nhds (ge_mem_nhds <| coe_lt_coe.2 <| lt_add_one b)).mono
fun y hy => ?_
rw [lt_tsub_iff_left]
calc
y.2 + x ≤ ↑(b + 1) + x := add_le_add_right hy.2 _
_ < y.1 := hy.1
| (a : ℝ≥0), ∞, _ => by
rw [sub_top]
refine (tendsto_pure.2 ?_).mono_right (pure_le_nhds _)
exact
((gt_mem_nhds <| coe_lt_coe.2 <| lt_add_one a).prod_nhds (lt_mem_nhds <| @coe_lt_top (a + 1))).mono fun x hx =>
tsub_eq_zero_iff_le.2 (hx.1.trans hx.2).le
| (a : ℝ≥0), (b : ℝ≥0), _ =>
by
simp only [nhds_coe_coe, tendsto_map'_iff, ← ENNReal.coe_sub, Function.comp_def, tendsto_coe]
exact continuous_sub.tendsto (a, b)
