le_schnirelmannDensity_iff — Mathlib

English

For any real x, x ≤ schnirelmannDensity(A) iff for all n, if 0 < n then x ≤ #({a ∈ Ioc 0 n | a ∈ A})/n.

Русский

Для любого вещественного x верно: x ≤ плотность Шниррельмана(A) эквивалентно тому, что для всех n, если 0 < n, то x ≤ #(A ∩ Ioc(0,n))/n.

LaTeX

$$x \\,\\le\\, \\operatorname{schnirelmannDensity}(A) \\iff \\forall n \\in \\mathbb{N},\\ 0 < n \\to x \\le \\#\\left\\{a \\in Ioc(0,n) \\mid a \\in A\\right\\}/n$$

Lean4

theorem le_schnirelmannDensity_iff {x : ℝ} :
    x ≤ schnirelmannDensity A ↔ ∀ n : ℕ, 0 < n → x ≤ #({a ∈ Ioc 0 n | a ∈ A}) / n :=
  (le_ciInf_iff ⟨0, fun _ ⟨_, hx⟩ => hx ▸ by positivity⟩).trans Subtype.forall

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