instIsAntisymmLiftRel — Mathlib

English

If α and β are antisymmetric under r and s, then LiftRel r s is antisymmetric on α ⊕ β.

Русский

Если r и s антисимметричны, то LiftRel r s антисимметрично на α ⊕ β.

LaTeX

$$$[IsAntisymm\\; α\\ r] [IsAntisymm\\; β\\ s] ⇒ IsAntisymm(α ⊕ β)(LiftRel r s)$$$

Lean4

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

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