dens_ne_one

Mathlib.Data.Finset.Density

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

English

For finite α and Finset s, dens(s) ≠ 1 iff s ≠ univ.

Русский

Для конечного α и Finset s верно: dens(s) ≠ 1 тогда и только тогда, когда s ≠ univ.

LaTeX

$$$ \\operatorname{dens}(s) \\neq 1 \\iff s \\neq \\mathrm{univ} $$$

Lean4

theorem dens_ne_one : dens s ≠ 1 ↔ s ≠ univ :=
  dens_eq_one.not

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

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

Разделы

Аффилиация

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