instIsPartialOrderLe — Mathlib

English

Let α be a type with a partial order relation ≤. Then ≤ is a partial order: reflexive, antisymmetric, and transitive.

Русский

Пусть α — тип с отношением частичного порядка ≤. Тогда ≤ образует частичный порядок: рефлексивен, антисимметричен и транзитивен.

LaTeX

$$$\big(\forall a \in \alpha\, a \le a\big) \land \big(\forall a,b \in \alpha\, a \le b \land b \le a \rightarrow a = b\big) \land \big(\forall a,b,c \in \alpha\, a \le b \land b \le c \rightarrow a \le c\big)$$$

Lean4

instance [PartialOrder α] : IsPartialOrder α (· ≤ ·) where

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