English
Equality expressing that the definitional fixInduction coincides with the operational recursion described by H, i.e., fixInduction h H equals H a h (λ a' h' => fixInduction (fix_fwd h h') H).
Русский
Определение равенства показывает, что определение fixInduction совпадает с рекурсией, описанной через H: fixInduction h H = H a h (λ a' h' → fixInduction (fix_fwd h h') H).
LaTeX
$$$\\text{fixInduction } h\\ H = H\\ a\\ h\\ (\\lambda a'\\ h' \\; \\Rightarrow \\; \\text{fixInduction } (\\text{fix_fwd } h\\ h')\\ H$)$$
Lean4
theorem fixInduction_spec {C : α → Sort*} {f : α →. β ⊕ α} {b : β} {a : α} (h : b ∈ f.fix a)
(H : ∀ a', b ∈ f.fix a' → (∀ a'', Sum.inr a'' ∈ f a' → C a'') → C a') :
@fixInduction _ _ C _ _ _ h H = H a h fun _ h' => fixInduction (fix_fwd h h') H :=
by
unfold fixInduction
generalize_proofs
induction ‹Acc _ _›
rfl
