self_eq_mass_mul_normalize — Mathlib

English

For a finite measure μ, μ = μ.mass · μ.normalize.toFiniteMeasure.

Русский

Для конечной меры μ верно μ = μ.mass · μ.normalize.toFiniteMeasure.

LaTeX

$$$\\mu = \\mu.mass \\; \\cdot \\mu.normalize.toFiniteMeasure$$$

Lean4

@[simp]
theorem self_eq_mass_mul_normalize (s : Set Ω) : μ s = μ.mass * μ.normalize s :=
  by
  obtain rfl | h := eq_or_ne μ 0
  · simp
  have mass_nonzero : μ.mass ≠ 0 := by rwa [μ.mass_nonzero_iff]
  simp only [normalize, dif_neg mass_nonzero]
  simp [mul_inv_cancel_left₀ mass_nonzero, coeFn_def]

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