continuousAt_add_coe_top — Mathlib

English

For any real a, the map is continuous at the point (a^EReal, top) in the product EReal × EReal.

Русский

Для любого a отображение непрерывно в точке (a^EReal, верхняя граница) в произведении EReal × EReal.

LaTeX

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

Lean4

theorem continuousAt_add_coe_top (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_top_coe a) (continuous_swap.tendsto ((a : EReal), ⊤))

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