schnirelmannDensity_le_iff_forall

English

The Schnirelmann density is ≤ x iff for all ε > 0 there exists n > 0 with #(...)/n < x + ε.

Русский

Плотность Шниррельмана меньше или равна x тогда и только тогда, когда для всякого ε > 0 существует n > 0 такое, что #(...)/n < x + ε.

LaTeX

$$\\operatorname{schnirelmannDensity}(A) \\le x \\\\iff \\\\forall \\varepsilon>0, \\exists n>0, \\\\#\\left\\{a \\in Ioc 0 n \\mid a \\in A\\right\\}/n < x + \\varepsilon$$

Lean4

theorem schnirelmannDensity_le_iff_forall {x : ℝ} :
    schnirelmannDensity A ≤ x ↔ ∀ ε : ℝ, 0 < ε → ∃ n : ℕ, 0 < n ∧ #({a ∈ Ioc 0 n | a ∈ A}) / n < x + ε :=
  by
  rw [le_iff_forall_pos_lt_add]
  simp only [schnirelmannDensity_lt_iff]

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