eq_bot_of_lt

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#IsSimpleOrder.eq_bot_of_lt

English

If a < b in a simple order, then a equals the bottom.

Русский

Если a < b в простом порядке, то a = ⊥.

LaTeX

$$$a < b \;\Rightarrow\; a = \bot$$$

Lean4

theorem eq_bot_of_lt : a = ⊥ :=
  (IsSimpleOrder.eq_bot_or_eq_top _).resolve_right h.ne_top

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

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

Разделы

Аффилиация

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