continuous_coe_ennreal_iff — Mathlib

English

There is an equivalence: a map to EReal via the real-valued function f is continuous if and only if f is continuous when viewed as ENNReal.

Русский

Существует эквивалентность: отображение в EReal через функцию f непрерывно тогда и только тогда, когда f непрерывна в ENNReal.

LaTeX

$$$(\\text{Continuous fun } a \\Rightarrow (f(a) : \\mathrm{EReal})) \\iff (\\text{Continuous } f)$$$

Lean4

theorem continuous_coe_ennreal_iff {f : α → ℝ≥0∞} : (Continuous fun a => (f a : EReal)) ↔ Continuous f :=
  isEmbedding_coe_ennreal.continuous_iff.symm

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