count_eq_zero_iff — Mathlib

English

The counting measure of a set is zero exactly when the set is empty.

Русский

Счётная мера множества равна нулю тогда и только тогда, когда множество пустое.

LaTeX

$$$count\;s = 0 \iff s = \emptyset$$$

Lean4

@[simp]
theorem count_eq_zero_iff : count s = 0 ↔ s = ∅
    where
  mp
    h :=
    eq_empty_of_forall_notMem fun x hx ↦ by simpa [hx] using ((ENNReal.le_tsum x).trans <| le_sum_apply _ _).trans_eq h
  mpr := by rintro rfl; exact measure_empty

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