pure_ne_bot

Mathlib.Order.Interval.Basic

URI: https://scilib.ai/kg/mathlib#Interval.pure_ne_bot

English

A singleton interval is never the bottom element.

Русский

Одиночный интервал никогда не равен нижнему элементу.

LaTeX

$$$ \forall a, \mathrm{pure}(a) \neq \bot $$$

Lean4

@[simp]
theorem pure_ne_bot {a : α} : pure a ≠ ⊥ :=
  WithBot.coe_ne_bot

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

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

Разделы

Аффилиация

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