instOrderBot

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associates.instOrderBot

English

Associates M carries a bottom element, namely 1, with bot ≤ a for all a.

Русский

Associates(M) имеет нижнюю границу, равную 1, и 1 ≤ a для всех a.

LaTeX

$$$ \bot = 1 \quad \land \quad \forall a, \bot \le a $$$

Lean4

instance instOrderBot : OrderBot (Associates M) where
  bot := 1
  bot_le _ := one_le

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

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

Разделы

Аффилиация

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