infinite_odd_deficient — Mathlib

English

There are infinitely many odd deficient numbers.

Русский

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

LaTeX

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

Lean4

theorem infinite_odd_deficient : {n : ℕ | Odd n ∧ n.Deficient}.Infinite :=
  by
  rw [Set.infinite_iff_exists_gt]
  intro n
  obtain ⟨p, ⟨_, h2⟩⟩ := exists_infinite_primes (max (n + 1) 3)
  exact ⟨p, Set.mem_setOf.mpr ⟨Prime.odd_of_ne_two h2 (Ne.symm (ne_of_lt (by omega))), Prime.deficient h2⟩, by omega⟩

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