exists_wellOrder — Mathlib

English

There exists a well-order on every type α, i.e., existence of a linear order that makes α well-founded.

Русский

Существует хорошо упорядочение на любом множестве α: существует линейный порядок, порождающий WellFoundedLT.

LaTeX

$$$\\exists L : LinearOrder(\\alpha), WellFoundedLT(\\alpha)$$$

Lean4

/-- The **well-ordering theorem** (or **Zermelo's theorem**): every type has a well-order -/
theorem exists_wellOrder : ∃ (_ : LinearOrder α), WellFoundedLT α := by
  classical exact ⟨linearOrderOfSTO WellOrderingRel, WellOrderingRel.isWellOrder.toIsWellFounded⟩

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