dens_ne_zero

Mathlib.Data.Finset.Density

URI: https://scilib.ai/kg/mathlib#Finset.dens_ne_zero

English

The density is nonzero exactly when s is nonempty.

Русский

Плотность ненулевая тогда, когда s не пусто.

LaTeX

$$$\\mathrm{dens}(s) \\neq 0 \\iff s\\neq \\emptyset$$$

Lean4

theorem dens_ne_zero : dens s ≠ 0 ↔ s.Nonempty :=
  dens_eq_zero.not.trans nonempty_iff_ne_empty.symm

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

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

Разделы

Аффилиация

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