English
The suffix relation on lists is a partial order: reflexive, transitive, and antisymmetric.
Русский
Отношение суффикса на списках образует частичный порядок: рефлексивность, транзитивность и антисимметричность.
LaTeX
$$$\text{IsPartialOrder}(\text{List}(\alpha), \; {\lt_+^:})$ where l1 <+: l2 is reflexive, transitive, and antisymmetric.$$
Lean4
instance : IsPartialOrder (List α) (· <:+ ·) where
refl _ := suffix_rfl
trans _ _ _ := IsSuffix.trans
antisymm _ _ h₁ h₂ := h₁.eq_of_length <| h₁.length_le.antisymm h₂.length_le