continuous_coe_iff — Mathlib

English

For any α, [TopologicalSpace α], and f: α → ℝ≥0, the map a ↦ (f(a) : ENNReal) is continuous iff f is continuous.

Русский

Для любого α с топологией и функций f: α → ℝ≥0, отображение a ↦ (f(a) как ENNReal) непрерывно тогда и только когда f непрерывна.

LaTeX

$$$\\bigl( \\operatorname{Continuous}\\bigl( a \\mapsto (f(a)) : \\mathbb{R}_{\\ge 0}^{\\infty} \\bigr) \\bigr) \\iff \\operatorname{Continuous}(f)$$$

Lean4

theorem continuous_coe_iff {α} [TopologicalSpace α] {f : α → ℝ≥0} : (Continuous fun a => (f a : ℝ≥0∞)) ↔ Continuous f :=
  isEmbedding_coe.continuous_iff.symm

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