instIsPartialOrderIsPrefix — Mathlib

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

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