continuousAt_add_bot_coe — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall a\\in\\mathbb{R},\\; \\mathrm{ContinuousAt}\\bigl((x,y) \\mapsto x+y\\bigr)\\bigl((\\bot)^{EReal}, a^{EReal}\\bigr)$$$

Lean4

theorem continuousAt_add_bot_coe (a : ℝ) : ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (⊥, a) :=
  by
  simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]
  refine fun r ↦
    ((gt_mem_nhds (bot_lt_coe (r - (a + 1)))).prod_nhds (gt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| lt_add_one _)).mono
      fun _ h ↦ ?_
  simpa only [← coe_add, _root_.sub_add_cancel] using add_lt_add h.1 h.2

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