mass_zero_iff — Mathlib

English

For a finite measure μ, μ.mass = 0 iff μ = 0.

Русский

Для конечной меры μ, μ.mass = 0 тогда и только тогда, когда μ = 0.

LaTeX

$$theorem mass_zero_iff (μ : FiniteMeasure Ω) : μ.mass = 0 ↔ μ = 0$$

Lean4

@[simp]
theorem mass_zero_iff (μ : FiniteMeasure Ω) : μ.mass = 0 ↔ μ = 0 :=
  by
  refine ⟨fun μ_mass => ?_, fun hμ => by simp only [hμ, zero_mass]⟩
  apply toMeasure_injective
  apply Measure.measure_univ_eq_zero.mp
  rwa [← ennreal_mass, ENNReal.coe_eq_zero]

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