schnirelmannDensity_lt_iff — Mathlib

English

The Schnirelmann density is less than x iff there exists n with 0 < n and the ratio of A in Ioc(0,n) to n is less than x.

Русский

Плотность Шниррельмана меньше x тогда и только тогда, когда существует n > 0 такое, что |{a ∈ Ioc(0,n) : a ∈ A}|/n < x.

LaTeX

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

Lean4

theorem schnirelmannDensity_lt_iff {x : ℝ} :
    schnirelmannDensity A < x ↔ ∃ n : ℕ, 0 < n ∧ #({a ∈ Ioc 0 n | a ∈ A}) / n < x := by
  rw [← not_le, le_schnirelmannDensity_iff]; simp

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