diracProba_diracProbaInverse — Mathlib

English

DiracProba composed with diracProbaInverse returns the original μ in the range.

Русский

Составление diracProba и diracProbaInverse возвращает исходное μ из диапазона.

LaTeX

$$$\\mathrm{diracProba}(\\mathrm{diracProbaInverse}(\\mu)) = \\mu$$$

Lean4

@[simp]
theorem diracProba_diracProbaInverse {X : Type*} [MeasurableSpace X] (μ : range (diracProba (X := X))) :
    diracProba (diracProbaInverse μ) = μ :=
  (mem_range.mp μ.prop).choose_spec

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