instIsPartialOrder_mathlib

Mathlib.Order.Defs.PartialOrder

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

English

If α is a PartialOrder, then ≤ is antisymmetric: if a ≤ b and b ≤ a, then a = b.

Русский

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

LaTeX

$$$a \le b ∧ b \le a \rightarrow a = b$$$

Lean4

instance [PartialOrder α] : Std.IsPartialOrder α where le_antisymm := PartialOrder.le_antisymm

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

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

Разделы

Аффилиация

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