infinite_deficient — Mathlib

English

There exist infinitely many deficient numbers.

Русский

Существует бесконечно много дефицитных чисел.

LaTeX

$$$\{n \in \mathbb{N} \mid \operatorname{Deficient}(n)\}$ is Infinite$$

Lean4

/-- There exists infinitely many deficient numbers -/
theorem infinite_deficient : {n : ℕ | n.Deficient}.Infinite :=
  by
  rw [Set.infinite_iff_exists_gt]
  intro a
  obtain ⟨b, h1, h2⟩ := exists_infinite_primes a.succ
  exact ⟨b, h2.deficient, h1⟩

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