English
The Schnirelmann density of A is 1 if and only if A contains all positive naturals (i.e., {0}^c ⊆ A).
Русский
Плотность Шниррельмана A равна 1 тогда и только тогда, когда A содержит все положительные натуральные числа ({0}^c ⊆ A).
LaTeX
$$schnirelmannDensity(A) = 1 \\iff {0}^c \\subseteq A$$
Lean4
/-- The Schnirelmann density of `A` is `1` if and only if `A` contains all the positive naturals. -/
theorem schnirelmannDensity_eq_one_iff : schnirelmannDensity A = 1 ↔ {0}ᶜ ⊆ A :=
by
rw [le_antisymm_iff, and_iff_right schnirelmannDensity_le_one]
constructor
· rw [← not_imp_not, not_le]
simp only [Set.not_subset, forall_exists_index, and_imp]
intro x hx hx'
apply (schnirelmannDensity_le_of_notMem hx').trans_lt
simpa only [one_div, sub_lt_self_iff, inv_pos, Nat.cast_pos, pos_iff_ne_zero] using hx
· intro h
refine le_ciInf fun ⟨n, hn⟩ => ?_
rw [one_le_div (Nat.cast_pos.2 hn), Nat.cast_le, filter_true_of_mem, Nat.card_Ioc, Nat.sub_zero]
rintro x hx
exact h (mem_Ioc.1 hx).1.ne'
