English
Let X be a completely regular T0 space with its Borel σ-algebra. The map x ↦ δ_x (the Dirac probability measure at x) defines an embedding of X into the space of probability measures on X.
Русский
Пусть X — полностью нормальное T0- пространство с борелевской сигма-алгеброй. Отображение x↦δ_x (дельта-меры в точке x) образует вложение X в множество вероятностных мер на X.
LaTeX
$$$$ \\text{If }X\\text{ is completely regular and }T_0\\text{ with its Borel }\\sigma\\text{-algebra, then }x\\mapsto \\delta_x\\text{ is an embedding }X\\hookrightarrow \\mathcal{P}(X). $$$$
Lean4
/-- If `X` is a completely regular T0 space with its Borel sigma algebra, then the mapping
that takes a point `x : X` to the delta-measure `diracProba x` is an embedding
`X → ProbabilityMeasure X`. -/
theorem isEmbedding_diracProba [T0Space X] [CompletelyRegularSpace X] : IsEmbedding (fun (x : X) ↦ diracProba x) :=
IsEmbedding.subtypeVal.comp diracProbaHomeomorph.isEmbedding
