toFinite_eq_zero_iff — Mathlib

English

For any α, μ.toFinite = 0 implies μ = 0; conversely 0 measure gives 0 finite part.

Русский

Любая мера μ с нулевым μ.toFinite эквивалентна нулевой мере; наоборот нулевая мера даёт нулевую конечную часть.

LaTeX

$$$ μ.toFinite = 0 \iff μ = 0 $$$

Lean4

@[simp]
theorem toFinite_eq_zero_iff [SFinite μ] : μ.toFinite = 0 ↔ μ = 0 := by
  simp_rw [← Measure.measure_univ_eq_zero, toFinite_apply_eq_zero_iff]

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