instIsTransLex — Mathlib

English

If r on α and s on β are transitive, then the lexicographic order on α ⊕ β is transitive. That is, whenever x ≤ y and y ≤ z in the Lex order, we have x ≤ z.

Русский

Если r на α и s на β транзитивны, то лексикографический порядок на α ⊕ β транзитивен: если x ≤ y и y ≤ z в Lex, то x ≤ z.

LaTeX

$$$\operatorname{IsTrans}(\alpha \oplus \beta, \mathrm{Lex}(r,s))$$$

Lean4

instance [IsTrans α r] [IsTrans β s] : IsTrans (α ⊕ β) (Lex r s) :=
  ⟨by
    rintro _ _ _ (⟨hab⟩ | ⟨hab⟩) (⟨hbc⟩ | ⟨hbc⟩)
    exacts [.inl (_root_.trans hab hbc), .sep _ _, .inr (_root_.trans hab hbc), .sep _ _]⟩

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