instContinuousAdd — Mathlib

English

Addition on ENNReal is continuous.

Русский

Сложение на ENNReal непрерывно.

LaTeX

$$$ (x,y) \mapsto x+y $ is continuous on $\mathbb{R}_{\ge 0}^{\infty}$.$$

Lean4

instance : ContinuousAdd ℝ≥0∞ := by
  refine ⟨continuous_iff_continuousAt.2 ?_⟩
  rintro ⟨_ | a, b⟩
  · exact tendsto_nhds_top_mono' continuousAt_fst fun p => le_add_right le_rfl
  rcases b with (_ | b)
  · exact tendsto_nhds_top_mono' continuousAt_snd fun p => le_add_left le_rfl
  simp only [ContinuousAt, some_eq_coe, nhds_coe_coe, ← coe_add, tendsto_map'_iff, Function.comp_def, tendsto_coe,
    tendsto_add]

Похожие утверждения