bot_ne_one

Mathlib.Algebra.Order.Interval.Basic

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

English

The bottom element is not equal to 1 in Interval.

Русский

Нижний элемент не равен единице в Interval.

LaTeX

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

Lean4

@[to_additive]
theorem bot_ne_one : (⊥ : Interval α) ≠ 1 :=
  bot_ne_pure

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

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

Разделы

Аффилиация

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