instIsPartialOrderIsSuffix — Mathlib

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

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