primesBelow_succ — Mathlib

English

For every n, the set of primes below n+1 equals the primes below n, with n added if n is prime.

Русский

Для каждого n множество простых чисел меньше n+1 равно множеству простых ниже n плюс n, если n простое.

LaTeX

$$$\mathrm{primesBelow}(n+1) = \begin{cases} \mathrm{insert}(n, \mathrm{primesBelow}(n)) & \text{if } \mathrm{Prime}(n) \\ \mathrm{primesBelow}(n) & \text{otherwise} \end{cases}$$$

Lean4

theorem primesBelow_succ (n : ℕ) : primesBelow (n + 1) = if n.Prime then insert n (primesBelow n) else primesBelow n :=
  by rw [primesBelow, primesBelow, Finset.range_add_one, Finset.filter_insert]

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