instIsPartialOrderGe — 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 \ge a\big) \land \big(\forall a,b \in \alpha\, a \ge b \land b \ge a \rightarrow a = b\big) \land \big(\forall a,b,c \in \alpha\, a \ge b \land b \ge c \rightarrow a \ge c\big)$$$

Lean4

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

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