one_ne_bot

Mathlib.Algebra.Order.Interval.Basic

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

English

The unit element is not equal to the bottom element in Interval.

Русский

Единица не равна нижнему элементу в Interval.

LaTeX

$$$ (1 : Interval \alpha) \neq \bot $$$

Lean4

@[to_additive]
theorem one_ne_bot : (1 : Interval α) ≠ ⊥ :=
  pure_ne_bot

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

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

Разделы

Аффилиация

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