schnirelmannDensity_empty

Mathlib.Combinatorics.Schnirelmann

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

English

The Schnirelmann density of the empty set is 0.

Русский

Плотность пустого множества равна 0.

LaTeX

$$\\operatorname{schnirelmannDensity}(\\varnothing) = 0$$

Lean4

@[simp]
theorem schnirelmannDensity_empty : schnirelmannDensity ∅ = 0 :=
  schnirelmannDensity_eq_zero_of_one_notMem (by simp)

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

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

Разделы

Аффилиация

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