Theorems · Theorem · number theory

schnirelmannDensity_le_of_subset

∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {B : Set ℕ} [inst_1 : DecidablePred fun x => x ∈ B],
  A ⊆ B → schnirelmannDensity A ≤ schnirelmannDensity B

The Schnirelmann density is increasing with the set.

Defined in

Mathlib.Combinatorics.Schnirelmann

Cited by

0 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidablePredDecidablePred