isWellOrder — Mathlib

English

There exists a well-order on every type α (i.e., a linear order that is a well-order).

Русский

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

LaTeX

$$$\\exists (\\leq)\\, \\text{LinearOrder}(\\alpha) \\land \\text{WellFoundedLT}(\\alpha)$$$

Lean4

instance isWellOrder : IsWellOrder α WellOrderingRel :=
  (RelEmbedding.preimage _ _).isWellOrder

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