instIsAntisymmLexOfIsAsymm — Mathlib

English

If IsAsymm ι r and ∀i IsAntisymm (α i) (s i), then Lex r s is antisymmetric.

Русский

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

LaTeX

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

Lean4

instance [IsAsymm ι r] [∀ i, IsAntisymm (α i) (s i)] : IsAntisymm _ (Lex r s) :=
  ⟨by
    rintro _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩) (⟨_, _, hji⟩ | ⟨_, _, hba⟩)
    · exact (asymm hij hji).elim
    · exact (irrefl _ hij).elim
    · exact (irrefl _ hji).elim
    · exact congr_arg (Sigma.mk _ ·) <| antisymm hab hba⟩

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