instIsAsymmLt

Mathlib.Order.RelClasses

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

English

The relation < is asymmetric: if x < y then not y < x.

Русский

Относительно < ассимметрично: если x < y, то не y < x.

LaTeX

$$$ \\forall x,y : α,\ x < y \\Rightarrow \\neg(y < x) $$$

Lean4

instance [Preorder α] : IsAsymm α (· < ·) :=
  ⟨@lt_asymm _ _⟩

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

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

Разделы

Аффилиация

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