toWellOrderExtension — Mathlib

English

There is a natural order isomorphism between a well-founded order and its well-order extension; the equivalence is given by the identity map.

Русский

Существует естественное отображение-эквивалентность между хорошо упорядоченным порядком и его расширением до хорошо упорядоченного, задаваемое тождественным отображением.

LaTeX

$$$\\alpha \\simeq WellOrderExtension \\alpha$$$

Lean4

/-- "Identity" equivalence between a well-founded order and its well-order extension. -/
def toWellOrderExtension : α ≃ WellOrderExtension α :=
  Equiv.refl _

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