instLinearOrderAntisymmetrizationLeOfDecidableLEOfDecidableLTOfIsTotal

English

Equivalence of WellFoundedLT between Antisymmetrization and original LT, via a lifting argument.

Русский

Эквивалентность WellFoundedLT между антисимметризацией и исходным LT через перенос-аргумент.

LaTeX

$$$\\text{WellFoundedLT}(\\text{Antisymmetrization}(α, ≤)) \\iff \\text{WellFoundedLT}(α)$$$

Lean4

instance [DecidableLE α] [DecidableLT α] [IsTotal α (· ≤ ·)] : LinearOrder (Antisymmetrization α (· ≤ ·)) :=
  { instPartialOrderAntisymmetrization with le_total := fun a b => Quotient.inductionOn₂' a b <| total_of (· ≤ ·),
    toDecidableLE := fun _ _ => show Decidable (Quotient.liftOn₂' _ _ _ _) from inferInstance,
    toDecidableLT := fun _ _ => show Decidable (Quotient.liftOn₂' _ _ _ _) from inferInstance }

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