not_lt_bot

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithBot.not_lt_bot

English

Bottom is strictly less than x in WithBot α if and only if x is not the bottom element.

Русский

Нижний элемент строго меньше x в WithBot α тогда и только тогда, когда x не является нижним элементом.

LaTeX

$$$ \bot < x \iff x \neq \bot $$$

Lean4

@[simp]
protected theorem not_lt_bot (a : WithBot α) : ¬a < ⊥ := by simp [lt_def]

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

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

Разделы

Аффилиация

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