induction — Mathlib

English

If r is a well-order, then r is a strict total order (repeat of 166566).

Русский

Если r — хорошо упорядоченное отношение, то оно является строгим полным порядком (повтор 166566).

LaTeX

$$$\\forall {\\alpha} {r}, [IsWellOrder α r] \\Rightarrow IsStrictTotalOrder α r$$$

Lean4

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

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