t2Space — Mathlib

English

Under suitable conditions (HasOuterApproxClosed and Borel space), the topology of convergence in distribution on ProbabilityMeasure Ω is Hausdorff.

Русский

При условиях HasOuterApproxClosed и BorelSpace топология сходимости по распределению на ProbabilityMeasure Ω т2 (Гаусдорфова).

LaTeX

$$$\\text{ToFiniteMeasure isEmbedding } \\Rightarrow \\text{t2Space}(\\text{ProbabilityMeasure } \\Omega)$$$

Lean4

/-- On topological spaces where indicators of closed sets have decreasing approximating sequences of
continuous functions (`HasOuterApproxClosed`), the topology of convergence in distribution of Borel
probability measures is Hausdorff (`T2Space`). -/
instance t2Space : T2Space (ProbabilityMeasure Ω) :=
  (toFiniteMeasure_isEmbedding Ω).t2Space

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