Notable Theorems

• Nat.exists_infinite_primes: Euclid's theorem that there exist infinitely many prime numbers. This also appears as Nat.not_bddAbove_setOfPred_prime and Nat.infinite_setOfPred_prime (the latter in Data.Nat.PrimeFin).

theorem Nat.exists_infinite_primes (n : ℕ) : ∃ (p : ℕ), n ≤ p ∧ Prime p

Euclid's theorem on the infinitude of primes. Here given in the form: for every n, there exists a prime number p ≥ n.

theorem Nat.not_bddAbove_setOfPred_prime : ¬BddAbove {p : ℕ | Prime p}

A version of Nat.exists_infinite_primes using the BddAbove predicate.

@[deprecated Nat.not_bddAbove_setOfPred_prime (since := "2026-07-09")]

theorem Nat.not_bddAbove_setOf_prime : ¬BddAbove {p : ℕ | Prime p}

Alias of Nat.not_bddAbove_setOfPred_prime.

---

A version of Nat.exists_infinite_primes using the BddAbove predicate.