English
Let r be a well-founded relation and a be an element with Acc r a. If for every b ≠ bot with C b there exists c with r c b ∧ C c, then C a → C bot.
Русский
Пусть r — хорошо основанное отношение и ha: Acc r a. Если для каждого b ≠ bot, для которого выполняется C b, существует c с r c b и C c, тогда C a → C bot.
LaTeX
$$$\\text{Acc } r\\ a \\to (\\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 a \\to C bot)$$$
Lean4
/-- Let `r` be a relation on `α`, let `C : α → Prop` and let `bot : α`.
This induction principle shows that `C bot` holds, given that
* some `a` that is accessible by `r` satisfies `C a`, and
* for each `b ≠ bot` such that `C b` holds, there is `c` satisfying `r c b` and `C c`. -/
theorem induction_bot {α} {r : α → α → Prop} {a bot : α} (ha : Acc r a) {C : α → Prop}
(ih : ∀ b, b ≠ bot → C b → ∃ c, r c b ∧ C c) : C a → C bot :=
ha.induction_bot' ih
