toFiniteMeasure_continuous — Mathlib

English

The map μ ↦ μ.toFiniteMeasure is continuous from ProbabilityMeasure Ω to FiniteMeasure Ω under the induced topology.

Русский

Отображение μ ↦ μ.toFiniteMeasure непрерывно от ProbabilityMeasure Ω к FiniteMeasure Ω в индуцированной топологии.

LaTeX

$$$\\text{Continuous} \\bigl( \\text{toFiniteMeasure} : \\text{ProbabilityMeasure } \\Omega \\to \\text{FiniteMeasure } \\Omega \\bigr)$$$

Lean4

theorem toFiniteMeasure_continuous : Continuous (toFiniteMeasure : ProbabilityMeasure Ω → FiniteMeasure Ω) :=
  continuous_induced_dom

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