dens_le_one

Mathlib.Data.Finset.Density

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

← MathLib Explorer

English

For any Finset s, dens(s) is at most 1.

Русский

Плотность любого Finset не превосходит единицы.

LaTeX

$$$ \\operatorname{dens}(s) \\le 1 $$$

Lean4

@[simp]
theorem dens_le_one : s.dens ≤ 1 := by
  cases isEmpty_or_nonempty α
  · simp [Subsingleton.elim s ∅]
  · simpa using dens_le_dens s.subset_univ

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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