bot_lt

Mathlib.Order.BoundedOrder.Basic

URI: https://scilib.ai/kg/mathlib#Ne.bot_lt

English

Within a namespace with a bottom element, if a ≠ ⊥, then ⊥ < a.

Русский

В области со знаком нижнего элемента, если a ≠ ⊥, то ⊥ < a.

LaTeX

$$$\bot < a$$$

Lean4

theorem bot_lt (h : a ≠ ⊥) : ⊥ < a :=
  bot_lt_iff_ne_bot.mpr h

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

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

Разделы

Аффилиация

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