toFiniteMeasure_isEmbedding — Mathlib

English

The map toFiniteMeasure is an embedding: it is injective and induces the induced topology.

Русский

Отображение toFiniteMeasure является вложением: оно инъективно и индуцирует топологию.

LaTeX

$$$\\text{IsEmbedding} (\\text{toFiniteMeasure} : \\text{ProbabilityMeasure } \\Omega \\to \\text{FiniteMeasure } \\Omega)$$$

Lean4

theorem toFiniteMeasure_isEmbedding (Ω : Type*) [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] :
    IsEmbedding (toFiniteMeasure : ProbabilityMeasure Ω → FiniteMeasure Ω)
    where
  eq_induced := rfl
  injective _μ _ν h := Subtype.eq <| congr_arg FiniteMeasure.toMeasure h

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