instIsAntisymmLe

Mathlib.Order.RelClasses

URI: https://scilib.ai/kg/mathlib#instIsAntisymmLe

English

Let α be a partial order. Then ≤ is antisymmetric: if a ≤ b and b ≤ a, then a = b.

Русский

Пусть α — частичный порядок. Тогда ≤ антисимметрично: если a ≤ b и b ≤ a, то a = b.

LaTeX

$$$\forall a,b \in \alpha,\ a \le b \land b \le a \rightarrow a = b$$$

Lean4

instance [PartialOrder α] : IsAntisymm α (· ≤ ·) :=
  ⟨@le_antisymm _ _⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru