instIsSymmLex — Mathlib

English

If IsSymm ι r and ∀i IsSymm (α i) (s i), then Lex r s is symmetric.

Русский

Если IsSymm ι r и ∀i IsSymm (α i) (s i), то Lex r s симметричен.

LaTeX

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

Lean4

instance [IsSymm ι r] [∀ i, IsSymm (α i) (s i)] : IsSymm _ (Lex r s) :=
  ⟨by
    rintro _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩)
    · exact Lex.left _ _ (symm hij)
    · exact Lex.right _ _ (symm hab)⟩

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