Notable Theorems

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

theorem Nat.exists_infinite_primes (n : ℕ) : ∃ (p : ℕ), n ≤ p ∧ Nat.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_setOf_prime : ¬BddAbove {p : ℕ | Nat.Prime p}

A version of Nat.exists_infinite_primes using the BddAbove predicate.