schnirelmannDensity_eq_one_iff_of_zero_mem

English

If A contains 0, then schnirelmannDensity(A) = 1 if and only if A is the set of all naturals.

Русский

Если 0 ∈ A, то плотность Шниррельмана A равна 1 тогда и только тогда, когда A — множество всех натуральных чисел.

LaTeX

$$schnirelmannDensity(A) = 1 \\iff A = \\mathbb{N}, \\text{ if } 0 \\in A$$

Lean4

/-- The Schnirelmann density of `A` containing `0` is `1` if and only if `A` is the naturals. -/
theorem schnirelmannDensity_eq_one_iff_of_zero_mem (hA : 0 ∈ A) : schnirelmannDensity A = 1 ↔ A = Set.univ :=
  by
  rw [schnirelmannDensity_eq_one_iff]
  constructor
  · refine fun h => Set.eq_univ_of_forall fun x => ?_
    rcases eq_or_ne x 0 with rfl | hx
    · exact hA
    · exact h hx
  · rintro rfl
    exact Set.subset_univ {0}ᶜ

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