smoothNumbers_compl — Mathlib

English

The non-zero non-n-smooth numbers lie in the complement of smoothNumbers(n) subject to a lower bound.

Русский

Не-нулевые не-n-гладкие числа лежат в комплементе smoothNumbers(n) с учётом нижней границы.

LaTeX

$$$(\mathrm{smoothNumbers}(n))^{c} \setminus \{0\} \subseteq \{m : n \le m\}$$$

Lean4

/-- The non-zero non-`N`-smooth numbers are `≥ N`. -/
theorem smoothNumbers_compl (N : ℕ) : (N.smoothNumbers)ᶜ \ {0} ⊆ {n | N ≤ n} := by
  simpa only [smoothNumbers_eq_factoredNumbers] using factoredNumbers_compl <| Finset.filter_subset _ (Finset.range N)

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