English
A recursion principle for f.fix: for a property C on α, if b ∈ f.fix(a) and for every a' with b ∈ f.fix(a') the step from a' to successors a'' implies C(a''), then C(a) holds.
Русский
Принцип рекурсии для f.fix: пусть C — свойство над элементами α. Если b ∈ f.fix(a) и для каждого a' с b ∈ f.fix(a') переход к любому a'' с Sum.inr(a'') ∈ f(a') влечёт выполнение C(a''), тогда C(a) верно.
LaTeX
$$$\\forall C:\\alpha \\to \\mathrm{Sort}^*,\\; (b \\in f.fix(a)) \\rightarrow (\\forall a'\\; (b \\in f.fix(a') \\rightarrow (\\forall a''\\; Sum.inr(a'') \\in f(a') \\rightarrow C(a'') ) \\rightarrow C(a'))) \\rightarrow C(a)$$$
Lean4
/-- A recursion principle for `PFun.fix`. -/
@[elab_as_elim]
def fixInduction {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') : C a :=
by
have h₂ := (Part.mem_assert_iff.1 h).snd
generalize_proofs at h₂
clear h
induction ‹Acc _ _› with
| intro a ha IH => _
have h : b ∈ f.fix a := Part.mem_assert_iff.2 ⟨⟨a, ha⟩, h₂⟩
exact H a h fun a' fa' => IH a' fa' (Part.mem_assert_iff.1 (fix_fwd h fa')).snd
