English
Let r be a relation on α, a,bot ∈ α, ha: Acc r a, and C: β → Prop with f: α → β. If for all b with f b ≠ f bot there exists C(b) → ∃ c with r c b ∧ C(f c), then C(f a) → C(f bot).
Русский
Пусть r — отношение на α, a и bot ∈ α, ha: Acc r a и C: β → Prop с f: α → β. Если для каждого b с f b ≠ f bot существует C(b) и C(f b) → ∃ c с r c b и C(f c), тогда C(f a) → C(f bot).
LaTeX
$$$\\text{Acc } r\\ a\\;\\Rightarrow\\; \\forall C\\,f,\\; (\\forall b, f b \\neq f\\,bot \\to C(f b) \\to \\exists c, r\\ c b \\wedge C(f c)) \\to (C(f a) \\to C(f bot))$$$
Lean4
/-- Let `r` be a relation on `α`, let `f : α → β` be a function, let `C : β → Prop`, and
let `bot : α`. This induction principle shows that `C (f bot)` holds, given that
* some `a` that is accessible by `r` satisfies `C (f a)`, and
* for each `b` such that `f b ≠ f bot` and `C (f b)` holds, there is `c`
satisfying `r c b` and `C (f c)`. -/
theorem induction_bot' {α β} {r : α → α → Prop} {a bot : α} (ha : Acc r a) {C : β → Prop} {f : α → β}
(ih : ∀ b, f b ≠ f bot → C (f b) → ∃ c, r c b ∧ C (f c)) : C (f a) → C (f bot) :=
(@Acc.recOn _ _ (fun x _ => C (f x) → C (f bot)) _ ha) fun x _ ih' hC =>
(eq_or_ne (f x) (f bot)).elim (fun h => h ▸ hC)
(fun h =>
let ⟨y, hy₁, hy₂⟩ := ih x h hC
ih' y hy₁ hy₂)
