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']