schnirelmannDensity_eq_zero_of_one_notMem

English

Let A be a subset of the natural numbers with 1 not in A. Then the Schnirelmann density of A equals 0.

Русский

Пусть A — подмножество натуральных чисел, не содержащее 1. Тогда плотность Шниррельмана A равна 0.

LaTeX

$$$1 \\notin A \\Rightarrow \\operatorname{schnirelmannDensity}(A) = 0$$$

Lean4

/-- The Schnirelmann density of a set not containing `1` is `0`. -/
theorem schnirelmannDensity_eq_zero_of_one_notMem (h : 1 ∉ A) : schnirelmannDensity A = 0 :=
  ((schnirelmannDensity_le_of_notMem h).trans (by simp)).antisymm schnirelmannDensity_nonneg

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