continuousOn_toReal — Mathlib

English

The function EReal.toReal is continuous on the complement of {⊥,⊤} in EReal.

Русский

Функция EReal.toReal непрерывна на дополнении отрезков {⊥,⊤} в EReal.

LaTeX

$$$\\text{ContinuousOn } EReal.toReal\\ ((\\{⊥,⊤\\}^c) :\\mathrm{Set EReal})$$$

Lean4

theorem continuousOn_toReal : ContinuousOn EReal.toReal ({⊥, ⊤}ᶜ : Set EReal) := fun _a ha =>
  ContinuousAt.continuousWithinAt (tendsto_toReal (mt Or.inr ha) (mt Or.inl ha))

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