instIsAntisymmLt — 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 _

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