induction — Mathlib

English

Induction on a well-founded < relation: for any C, if for all x, (for all y < x, C y) implies C x, then C a.

Русский

Индукция по хорошо основанному relation <: для любого C, если для всех x, все y < x удовлетворяют C, тогда C x.

LaTeX

$$$\\forall C:\\\\alpha \\to \\mathrm{Prop}\\, (a:\\\\alpha),\\ (\\\\forall x, (\\\\forall y, y < x \\\\to C y) \\\\to C x) \\\\to C a$$$

Lean4

/-- Inducts on a well-founded `<` relation. -/
theorem induction {C : α → Prop} (a : α) (ind : ∀ x, (∀ y, y < x → C y) → C x) : C a :=
  IsWellFounded.induction _ _ ind

Похожие утверждения