schnirelmannDensity_le_of_subset — Mathlib

English

If A ⊆ B then the Schnirelmann density is nondecreasing: schnirelmannDensity(A) ≤ schnirelmannDensity(B).

Русский

Если A ⊆ B, то плотность Шниррельмана неубывающая: плотность(A) ≤ плотность(B).

LaTeX

$$A \\subseteq B \\Rightarrow \\operatorname{schnirelmannDensity}(A) \\le \\operatorname{schnirelmannDensity}(B)$$

Lean4

/-- The Schnirelmann density is increasing with the set. -/
theorem schnirelmannDensity_le_of_subset {B : Set ℕ} [DecidablePred (· ∈ B)] (h : A ⊆ B) :
    schnirelmannDensity A ≤ schnirelmannDensity B :=
  ciInf_mono ⟨0, fun _ ⟨_, hx⟩ ↦ hx ▸ by positivity⟩ fun _ ↦ by gcongr; exact h

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