English
If α is asymmetric under r and β is asymmetric under s, then Prod.Lex r s is asymmetric.
Русский
Если на α и β выполняется асиммметрия по r и s, то лексикографический порядок на α×β асимметричен.
LaTeX
$$[IsAsymm α r] [IsAsymm β s] : IsAsymm (Prod α β) (Prod.Lex r s)$$
Lean4
instance [IsAsymm α r] [IsAsymm β s] : IsAsymm (α × β) (Prod.Lex r s) where
asymm
| (_a₁, _a₂), (_b₁, _b₂), .left _ _ h₁, .left _ _ h₂ => IsAsymm.asymm _ _ h₂ h₁
| (_a₁, _a₂), (_, _b₂), .left _ _ h₁, .right _ _ => IsAsymm.asymm _ _ h₁ h₁
| (_a₁, _a₂), (_, _b₂), .right _ _, .left _ _ h₂ => IsAsymm.asymm _ _ h₂ h₂
| (_a₁, _a₂), (_, _b₂), .right _ h₁, .right _ h₂ => IsAsymm.asymm _ _ h₁ h₂
