continuousAt_add_bot_bot — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem continuousAt_add_bot_bot : ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (⊥, ⊥) :=
  by
  simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]
  refine fun r ↦ ((gt_mem_nhds (bot_lt_coe 0)).prod_nhds (gt_mem_nhds <| bot_lt_coe r)).mono fun _ h ↦ ?_
  simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2

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