lt_irrefl

Mathlib.Order.Defs.PartialOrder

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

English

For every a, not a < a.

Русский

Для каждого a: не выполняется a < a.

LaTeX

$$$\\\\forall a : \\\\alpha, \\\\lnot(a < a)$$$

Lean4

theorem lt_irrefl (a : α) : ¬a < a := fun h ↦ not_le_of_gt h le_rfl

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

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

Разделы

Аффилиация

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