count_ne_zero_iff

Mathlib.MeasureTheory.Measure.Count

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.count_ne_zero_iff

English

The counting measure is nonzero if and only if the set is nonempty.

Русский

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

LaTeX

$$$count\;s \neq 0 \iff s.Nonempty$$$

Lean4

theorem count_ne_zero_iff : count s ≠ 0 ↔ s.Nonempty :=
  count_eq_zero_iff.not.trans nonempty_iff_ne_empty.symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru