schnirelmannDensity_finite

Mathlib.Combinatorics.Schnirelmann

URI: https://scilib.ai/kg/mathlib#schnirelmannDensity_finite

← MathLib Explorer

English

The Schnirelmann density of a finite set A is 0.

Русский

Плотность Шниррельмана конечного множества A равна 0.

LaTeX

$$schnirelmannDensity(A) = 0$$

Lean4

/-- The Schnirelmann density of any finite set is `0`. -/
theorem schnirelmannDensity_finite {A : Set ℕ} [DecidablePred (· ∈ A)] (hA : A.Finite) : schnirelmannDensity A = 0 := by
  simpa using schnirelmannDensity_finset hA.toFinset

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

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

Разделы

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

Аффилиация

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