bot_ne_one

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

English

The bottom element is not equal to the unit in WithBot α.

Русский

Нижняя граница в WithBot α не равна единице.

LaTeX

$$$ (⊥ : \\mathrm{WithBot}\\,\\alpha) \\neq 1 $$$

Lean4

@[to_additive (attr := simp)]
theorem bot_ne_one : (⊥ : WithBot α) ≠ 1 :=
  bot_ne_coe

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

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

Разделы

Аффилиация

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