preBeth_nat — Mathlib

English

For every natural n, preBeth(n.cast) equals the n-fold iterate of 2-power starting at 0.

Русский

Для каждого натурального n: preBeth(n) равно n-разовой итерации возведения 2 в степень начиная с 0.

LaTeX

$$preBeth(n.cast) = \operatorname{Nat.iterate}(\lambda x, 2^x, n, 0)$$

Lean4

theorem preBeth_nat : ∀ n : ℕ, preBeth n = (2 ^ ·)^[n] (0 : ℕ)
  | 0 => by simp
  | n + 1 => by
    rw [natCast_succ, preBeth_succ, Function.iterate_succ_apply', preBeth_nat]
    simp

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