schnirelmannDensity_le_div — Mathlib

English

For any n ≠ 0, schnirelmannDensity(A) ≤ |{a ∈ Ioc 0 n | a ∈ A}| / n.

Русский

Для любого n ≠ 0 плотность Шнирельмана не превосходит доли элементов A в {1, ..., n}.

LaTeX

$$$ \\operatorname{schnirelmannDensity}(A) \\le \\frac{\\#\\{ a \\in Ioc 0 n \\mid a \\in A \\}}{n} \\quad (n \\neq 0) $$$

Lean4

theorem schnirelmannDensity_le_div {n : ℕ} (hn : n ≠ 0) : schnirelmannDensity A ≤ #({a ∈ Ioc 0 n | a ∈ A}) / n :=
  ciInf_le ⟨0, fun _ ⟨_, hx⟩ => hx ▸ by positivity⟩ (⟨n, hn.bot_lt⟩ : { n : ℕ // 0 < n })

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