schnirelmannDensity_univ

Mathlib.Combinatorics.Schnirelmann

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

English

The Schnirelmann density of Set.univ is 1.

Русский

Плотность Шниррельмана множества всеобщее равна 1.

LaTeX

$$\\operatorname{schnirelmannDensity}(Set.univ) = 1$$

Lean4

@[simp]
theorem schnirelmannDensity_univ : schnirelmannDensity Set.univ = 1 :=
  (schnirelmannDensity_eq_one_iff_of_zero_mem (by simp)).2 (by simp)

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

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

Разделы

Аффилиация

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