count_ne_zero''

Mathlib.MeasureTheory.Measure.Count

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

English

For any set s, the sum of 1 over s is at least the count of s: ∑' s 1 ≤ count s.

Русский

Сумма единиц по s не превосходит количество элементов s.

LaTeX

$$$$\\sum'_{x \\in s} 1 \\le \\mathrm{count}(s).$$$$

Lean4

@[simp]
theorem count_ne_zero'' [Nonempty α] : (count : Measure α) ≠ 0 := by simp [count]

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

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

Разделы

Аффилиация

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