bot_lt_iff_eq_top

Mathlib.Order.Atoms

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

English

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

Русский

Для каждого элемента a выполняется: ⊥ < a тогда и только тогда, когда a = ⊤.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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