diracProbaInverse_eq — Mathlib

English

The inverse of the equivalence diracProbaEquiv is continuous; the forward direction is continuous by diracProbaEquiv.

Русский

Обратное отображение эквивалентности diracProbaEquiv непрерывно; прямое отображение непрерывно по diracProbaEquiv.

LaTeX

$$$\\text{Continuous}(\\mathrm{diracProbaEquiv}^{-1})$$$

Lean4

theorem diracProbaInverse_eq [T0Space X] {x : X} {μ : range (diracProba (X := X))} (h : μ = diracProba x) :
    diracProbaInverse μ = x := by
  apply injective_diracProba (X := X)
  simp only [← h]
  exact (mem_range.mp μ.prop).choose_spec

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