English
There exists a homeomorphism diracProbaHomeomorph between X and the image of diracProba.
Русский
Существует гомеоморфизм между X и образом diracProba.
LaTeX
$$$\\mathrm{diracProbaHomeomorph}: X \\simeq_t range(\\mathrm{diracProba})$$$
Lean4
/-- In a completely regular T0 topological space `X`, `diracProbaEquiv` is a homeomorphism to
its image in `ProbabilityMeasure X`. -/
noncomputable def diracProbaHomeomorph [T0Space X] [CompletelyRegularSpace X] : X ≃ₜ range (diracProba (X := X)) :=
@Homeomorph.mk X _ _ _ diracProbaEquiv continuous_diracProbaEquiv continuous_diracProbaEquivSymm