diracProbaEquiv — Mathlib

English

There exists a homeomorphism diracProbaHomeomorph between X and range(diracProba).

Русский

Существует гомеоморфизм между X и range(diracProba).

LaTeX

$$$\\mathrm{diracProbaHomeomorph}: X \\simeq_t\\ range(\\mathrm{diracProba})$$$

Lean4

/-- In a T0 topological space `X`, the assignment `x ↦ diracProba x` is a bijection to its
range in `ProbabilityMeasure X`. -/
noncomputable def diracProbaEquiv [T0Space X] : X ≃ range (diracProba (X := X))
    where
  toFun := fun x ↦ ⟨diracProba x, by exact mem_range_self x⟩
  invFun := diracProbaInverse
  left_inv x := by apply diracProbaInverse_eq; rfl
  right_inv μ := Subtype.ext (by simp only [diracProba_diracProbaInverse])

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