inv_measure_univ_smul_eq_self — Mathlib

English

For any μ that is zero-or-probability, scaling by the inverse of μ(univ) leaves μ unchanged: (μ(univ))^{-1} • μ = μ.

Русский

Для μ, нулевой или вероятностной, нормализация масштаба на обратную величину μ(все пространство) не меняет μ: (μ(все пространство))^{-1} • μ = μ.

LaTeX

$$$(\mu(\mathrm{univ}))^{-1} \cdot \mu = \mu$$$

Lean4

@[simp]
theorem inv_measure_univ_smul_eq_self : (μ univ)⁻¹ • μ = μ := by
  rcases eq_zero_or_isProbabilityMeasure μ with h | h <;> simp [h]

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