instIsPartialOrderIsInfix — Mathlib

English

The infix relation on lists is a partial order: reflexive, transitive, antisymmetric.

Русский

Отношение инфикса на списках образует частичный порядок: рефлексивность, транзитивность и антисимметричность.

LaTeX

$$$\text{IsPartialOrder}(\text{List}(\alpha), \; {\lt_+^:})$ with refl, trans, and antisymm.$$

Lean4

instance : IsPartialOrder (List α) (· <:+: ·) where
  refl _ := infix_rfl
  trans _ _ _ := IsInfix.trans
  antisymm _ _ h₁ h₂ := h₁.eq_of_length <| h₁.length_le.antisymm h₂.length_le

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