le_antisymm

Mathlib.Order.Defs.PartialOrder

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

English

If α is a PartialOrder, and 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

theorem le_antisymm : a ≤ b → b ≤ a → a = b :=
  PartialOrder.le_antisymm _ _

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

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

Разделы

Аффилиация

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