false

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#LT.lt.false

English

For any x, x < x implies False (lt is irreflexive).

Русский

Для любого x, x < x ведёт к False (отношение < иррефлексивно).

LaTeX

$$$a < a \\to \\mathrm{False}$$$

Lean4

protected theorem false : a < a → False :=
  lt_irrefl a

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

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

Разделы

Аффилиация

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