instIsLinearOrderGe — Mathlib

English

In a linear order, ≥ is a linear order relation: reflexive, antisymmetric, transitive, and total.

Русский

В линейном порядке ≥ является линейным порядком: рефлексивен, антисимметричен, транзитивен и полностью упорядочен.

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) \land \big(\forall a,b \in \alpha\, a \ge b \lor b \ge a\big)$$$

Lean4

instance [LinearOrder α] : IsLinearOrder α (· ≥ ·) where

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