lt_self_iff_false

Mathlib.Order.Basic

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

English

For any x, x < x is false.

Русский

Для любого x верно, что x < x ложно.

LaTeX

$$$x < x \\leftrightarrow \\text{False}$$$

Lean4

@[simp]
theorem lt_self_iff_false (x : α) : x < x ↔ False :=
  ⟨lt_irrefl x, False.elim⟩

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

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

Разделы

Аффилиация

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