instIsLinearOrderLe — Mathlib

English

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

Русский

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

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

Lean4

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

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