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