continuousAt_add_coe_bot — Mathlib

English

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

Русский

Сложение в EReal непрерывно в точке (a, ⊥) для действительного a.

LaTeX

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

Lean4

theorem continuousAt_add_coe_bot (a : ℝ) : ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (a, ⊥) := by
  simpa only [add_comm, Function.comp_def, ContinuousAt, Prod.swap] using
    Tendsto.comp (continuousAt_add_bot_coe a) (continuous_swap.tendsto ((a : EReal), ⊥))

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