isAsymm — Mathlib

English

If r is asymmetric on α, then the lexicographic extension Lex r on List α is asymmetric.

Русский

Если r асимметрично на α, то лексикографическое расширение Lex r на List α асимметрично.

LaTeX

$$$\\mathrm{IsAsymm}(\\mathrm{List}\\,\\alpha, \\mathrm{List.Lex}\\ r).$$$

Lean4

instance isAsymm (r : α → α → Prop) [IsAsymm α r] : IsAsymm (List α) (Lex r) where asymm := aux
where aux
    | _, _, Lex.rel h₁, Lex.rel h₂ => asymm h₁ h₂
    | _, _, Lex.rel h₁, Lex.cons _ => asymm h₁ h₁
    | _, _, Lex.cons _, Lex.rel h₂ => asymm h₂ h₂
    | _, _, Lex.cons h₁, Lex.cons h₂ => aux _ _ h₁ h₂

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