schnirelmannDensity_nonneg

Mathlib.Combinatorics.Schnirelmann

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

English

For any A ⊆ ℕ, schnirelmannDensity(A) ≥ 0.

Русский

Для любого A ⊆ ℕ плотность Шнирельмана неотрицательна.

LaTeX

$$$ 0 \\le \\operatorname{schnirelmanDensity}(A) $$$

Lean4

theorem schnirelmannDensity_nonneg : 0 ≤ schnirelmannDensity A :=
  Real.iInf_nonneg (fun _ => by positivity)

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

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

Разделы

Аффилиация

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