univ_eq_zero_iff — Mathlib

English

An outer measure is zero if and only if it assigns zero to the entire universe; equivalently, m(univ) = 0 iff m = 0.

Русский

Внешняя мера равна нулю тогда и только тогда, когда она присваивает нуль всему множеству Universe; эквивалентно m(univ) = 0 ⇔ m = 0.

LaTeX

$$$m(\mathrm{univ}) = 0 \iff m = 0$.$$

Lean4

theorem univ_eq_zero_iff (m : OuterMeasure α) : m univ = 0 ↔ m = 0 :=
  ⟨fun h => bot_unique fun s => (measure_mono <| subset_univ s).trans_eq h, fun h => h.symm ▸ rfl⟩

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