instIsAntisymmLex — Mathlib

English

If r on α and s on β are antisymmetric, then the lexicographic order on α ⊕ β is antisymmetric. If x ≤ y and y ≤ x, then x = y.

Русский

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

LaTeX

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

Lean4

instance [IsAntisymm α r] [IsAntisymm β s] : IsAntisymm (α ⊕ β) (Lex r s) :=
  ⟨by rintro _ _ (⟨hab⟩ | ⟨hab⟩) (⟨hba⟩ | ⟨hba⟩) <;> rw [antisymm hab hba]⟩

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