normalize_eq_of_nonzero — Mathlib

English

If μ ≠ 0, then μ.normalize s = μ.mass⁻¹ · μ s for any set s.

Русский

Если μ ≠ 0, то для любого множества s выполняется μ.normalize s = μ.mass⁻¹ · μ s.

LaTeX

$$$\\mu\\normalize s = \\mu.mass^{-1} \\cdot \\mu s$$$

Lean4

theorem normalize_eq_of_nonzero (nonzero : μ ≠ 0) (s : Set Ω) : μ.normalize s = μ.mass⁻¹ * μ s := by
  simp only [μ.self_eq_mass_mul_normalize, μ.mass_nonzero_iff.mpr nonzero, inv_mul_cancel_left₀, Ne, not_false_iff]

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