English
Alternative formulation of bot-based induction: given ha: Acc r a and the same ih as above, conclude C a → C bot.
Русский
Альтернативная формулировка индукции по bot: имея ha: Acc r a и то же ih, заключаем C a → C bot.
LaTeX
$$$\\text{Alt: }\\text{Acc } r\\ a \\to (\\forall b, f b \\neq f bot \\to C(f b) \\to \\exists c, r\\ c b \\wedge C(f c)) \\to (C a \\to C bot)$$$
Lean4
/-- Let `r` be a well-founded 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` 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} (hwf : WellFounded r) {a bot : α} {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) :=
(hwf.apply a).induction_bot' ih
