t2Space — Mathlib

English

Weak convergence topology on FiniteMeasure Ω is Hausdorff under reasonable hypotheses.

Русский

Слабая топология сходимости на FiniteMeasure Ω является Hausdorff при разумных предпосылках.

LaTeX

$$$ \text{T2Space} (\text{FiniteMeasure } \Omega). $$$

Lean4

/-- On topological spaces where indicators of closed sets have decreasing approximating sequences of
continuous functions (`HasOuterApproxClosed`), the topology of weak convergence of finite Borel
measures is Hausdorff (`T2Space`). -/
instance t2Space : T2Space (FiniteMeasure Ω) :=
  (isEmbedding_toWeakDualBCNN Ω).t2Space

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