continuousAt_add_top_top — Mathlib

English

The addition on EReal is continuous at the point (top, top).

Русский

Сложение в EReal непрерывно в точке (top, top).

LaTeX

$$$\\mathrm{ContinuousAt}\\bigl((x,y) \\mapsto x+y\\bigr)\\bigl((\\top)^{EReal}, (\\top)^{EReal}\\bigr)$$$

Lean4

theorem continuousAt_add_top_top : ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (⊤, ⊤) :=
  by
  simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_top]
  refine fun r ↦ ((lt_mem_nhds (coe_lt_top 0)).prod_nhds (lt_mem_nhds <| coe_lt_top r)).mono fun _ h ↦ ?_
  simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2

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