instIsAntisymmGt — Mathlib

English

Let α be a preorder. Then the strict order > on α is antisymmetric: for all a,b ∈ α, if a > b and b > a, then a = b.

Русский

Пусть α — множество с предпорядком. Тогда строгий порядок > на α антисимметричен: для любых a,b ∈ α, если a > b и b > a, то a = b.

LaTeX

$$$\forall a,b \in \alpha,\ a > b \rightarrow b > a \rightarrow a = b$$$

Lean4

instance [Preorder α] : IsAntisymm α (· > ·) :=
  IsAsymm.isAntisymm _

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