instIsAsymmGt

Mathlib.Order.RelClasses

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

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 α (· > ·) :=
  IsAsymm.swap _

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

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

Разделы

Аффилиация

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