English
The standard induction principle: if every a with Acc r a can be extended toward bot via r, then C a implies C bot.
Русский
Стандартный принцип индукции: если каждое a с Acc r a может быть продолжено к bot через r, тогда C a влечет C bot.
LaTeX
$$$\\text{WellFounded } r \\to \\bigl(\\forall a\\; (\\text{bot} \\text{ induction}) \\Rightarrow C a \\to C bot\\bigr)$$$
Lean4
/-- Let `r` be a well-founded relation on `α`, let `C : α → Prop`, and let `bot : α`.
This induction principle shows that `C bot` holds, given that
* some `a` satisfies `C a`, and
* for each `b` that satisfies `C b`, there is `c` satisfying `r c b` and `C c`.
The naming is inspired by the fact that when `r` is transitive, it follows that `bot` is
the smallest element w.r.t. `r` that satisfies `C`. -/
theorem induction_bot {α} {r : α → α → Prop} (hwf : WellFounded r) {a bot : α} {C : α → Prop}
(ih : ∀ b, b ≠ bot → C b → ∃ c, r c b ∧ C c) : C a → C bot :=
hwf.induction_bot' ih
