cantorFunctionAux_succ — Mathlib

English

CantorFunctionAux shifted by one index satisfies (cantorFunctionAux c f)(n+1) = c · cantorFunctionAux c (f ∘ (n+1))(n).

Русский

Перенос CantorFunctionAux на одну позицию удовлетворяет (cantorFunctionAux c f)(n+1) = c · cantorFunctionAux c (f ∘ S)(n).

LaTeX

$$$\\forall n, \\operatorname{cantorFunctionAux}(c,f)(n+1) = c \\cdot \\operatorname{cantorFunctionAux}(c,\\lambda n. f(n+1))(n)$$$

Lean4

theorem cantorFunctionAux_succ (f : ℕ → Bool) :
    (fun n => cantorFunctionAux c f (n + 1)) = fun n => c * cantorFunctionAux c (fun n => f (n + 1)) n :=
  by
  ext n
  cases h : f (n + 1) <;> simp [h, _root_.pow_succ']

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