instIsAntisymmGe

Mathlib.Order.RelClasses

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

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 \ge b \land b \ge a \rightarrow a = b$$$

Lean4

instance [PartialOrder α] : IsAntisymm α (· ≥ ·) :=
  IsAntisymm.swap _

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

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

Разделы

Аффилиация

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