English
If α has a strict order r and β is antisymmetric under s, then the lexicographic order Prod.Lex r s on α×β is antisymmetric.
Русский
Если на α задано строгое упорядочение r, а на β — антисимметрия s, то лексикографический порядок Prod.Lex r s на α×β антисимметричен.
LaTeX
$$[IsStrictOrder α r] [IsAntisymm β s] : IsAntisymm (α × β) (Prod.Lex r s)$$
Lean4
instance {r : α → α → Prop} {s : β → β → Prop} [IsStrictOrder α r] [IsAntisymm β s] :
IsAntisymm (α × β) (Prod.Lex r s) :=
⟨fun x₁ x₂ h₁₂ h₂₁ ↦
match x₁, x₂, h₁₂, h₂₁ with
| (a, _), (_, _), .left _ _ hr₁, .left _ _ hr₂ => (irrefl a (_root_.trans hr₁ hr₂)).elim
| (_, _), (_, _), .left _ _ hr₁, .right _ _ => (irrefl _ hr₁).elim
| (_, _), (_, _), .right _ _, .left _ _ hr₂ => (irrefl _ hr₂).elim
| (_, _), (_, _), .right _ hs₁, .right _ hs₂ => antisymm hs₁ hs₂ ▸ rfl⟩
