isTotal_right — Mathlib

English

If α is trichotomous and β is total, then the lexicographic order Prod.Lex r s is total on α×β.

Русский

Если α тричотомно упорядочено и β полностью упорядочено, то лексикографический порядок на α×β тотален.

LaTeX

$$[IsTrichotomous α r] [IsTotal β s] : IsTotal (α × β) (Prod.Lex r s)$$

Lean4

instance isTotal_right {r : α → α → Prop} {s : β → β → Prop} [IsTrichotomous α r] [IsTotal β s] :
    IsTotal (α × β) (Prod.Lex r s) :=
  ⟨fun ⟨i, a⟩ ⟨j, b⟩ ↦ by
    obtain hij | rfl | hji := trichotomous_of r i j
    · exact Or.inl (.left _ _ hij)
    · exact (total_of s a b).imp (.right _) (.right _)
    · exact Or.inr (.left _ _ hji)⟩

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