exists_prime_lt_and_le_two_mul_succ

English

A stepping lemma: if p is a prime with p ≤ 2q and, from smaller n, a prime between n and 2n exists, then for every n with n < p the same fact holds.

Русский

Переходной лемм: если p — простое число и p ≤ 2q, и для меньших n существует простое между n и 2n, то для любого n с n < p существование такого простого продолжает выполняться.

LaTeX

$$$\forall q>0,\; \forall p \text{ prime},\; p \le 2q,\; (\forall n

Lean4

/-- Proves that Bertrand's postulate holds over all positive naturals less than n by identifying a
descending list of primes, each no more than twice the next, such that the list contains a witness
for each number ≤ n.
-/
theorem exists_prime_lt_and_le_two_mul_succ {n} (q) {p : ℕ} (prime_p : Nat.Prime p) (covering : p ≤ 2 * q)
    (H : n < q → ∃ p : ℕ, p.Prime ∧ n < p ∧ p ≤ 2 * n) (hn : n < p) : ∃ p : ℕ, p.Prime ∧ n < p ∧ p ≤ 2 * n := by grind

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