instIsIrreflGt

Mathlib.Order.RelClasses

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

English

> is irreﬂexive: no element is greater than itself.

Русский

> иррефлексивно: нет такого элемента, который больше самого себя.

LaTeX

$$$ \\forall x : α,\ \\neg (x > x)$$$

Lean4

instance [Preorder α] : IsIrrefl α (· > ·) :=
  IsIrrefl.swap _

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

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

Разделы

Аффилиация

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