lt_top_iff_eq_bot

Mathlib.Order.Atoms

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

English

For every a, a is strictly below top if and only if a equals bottom.

Русский

Для любого a: a < ⊤ тогда и только тогда, когда a = ⊥.

LaTeX

$$$\forall a:\alpha,\; a < \top \iff a = \bot$$$

Lean4

@[simp]
theorem lt_top_iff_eq_bot {a : α} : a < ⊤ ↔ a = ⊥ :=
  ⟨eq_bot_of_lt, fun h ↦ h ▸ bot_lt_top⟩

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

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

Разделы

Аффилиация

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