not_bddAbove_setOf_prime — Mathlib

English

The set of primes is not bounded above.

Русский

Множество простых не ограничено сверху.

LaTeX

$$$\\\\lnot \\\\mathrm{BddAbove} \\\\{p \\\\mid \\\\mathrm{Prime}(p)\\\\}$$$

Lean4

/-- A version of `Nat.exists_infinite_primes` using the `BddAbove` predicate. -/
theorem not_bddAbove_setOf_prime : ¬BddAbove {p | Prime p} :=
  by
  rw [not_bddAbove_iff]
  intro n
  obtain ⟨p, hi, hp⟩ := exists_infinite_primes n.succ
  exact ⟨p, hp, hi⟩

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