instIsTransLex — Mathlib

English

If IsTrans ι r and ∀i IsTrans (α i) (s i), then Lex r s is transitive.

Русский

Если IsTrans ι r и ∀i IsTrans (α i) (s i), то Lex r s транзитивен.

LaTeX

$$$[IsTrans ι r] [\\forall i, IsTrans (\\alpha i) (s i)] : IsTrans ((i, \\alpha i)) (Sigma.Lex r s).$$$

Lean4

instance [IsTrans ι r] [∀ i, IsTrans (α i) (s i)] : IsTrans _ (Lex r s) :=
  ⟨by
    rintro _ _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩) (⟨_, c, hk⟩ | ⟨_, c, hc⟩)
    · exact Lex.left _ _ (_root_.trans hij hk)
    · exact Lex.left _ _ hij
    · exact Lex.left _ _ hk
    · exact Lex.right _ _ (_root_.trans hab hc)⟩

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