ulift — Mathlib

English

If α is well-ordered by r, then ULift α is well-ordered by the preimage of r along down via ULift.

Русский

Если α хорошо упорядочено порядком r, то ULift α также хорошо упорядочено по отношению, полученному как предобраз через down.

LaTeX

$$$$ \forall {\alpha} \ (IsWellOrder\ α\ r) \Rightarrow IsWellOrder(ULift\ α) (ULift.down^{-1}\circ r). $$$$

Lean4

instance ulift {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : IsWellOrder (ULift α) (ULift.down ⁻¹'o r) :=
  IsWellOrder.preimage r Equiv.ulift

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