diracProbaHomeomorph — Mathlib

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

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