orderBot

Mathlib.Data.Finsupp.MonomialOrder

URI: https://scilib.ai/kg/mathlib#MonomialOrder.orderBot

← MathLib Explorer

English

The order on the exponent space m.syn has a bottom element given by 0, i.e., ⊥ is 0.

Русский

У экспоненциального пространства m.syn имеется нижний предел, равный 0, т.е. ⊥ = 0.

LaTeX

$$$$ \\bot = 0. $$$$

Lean4

instance orderBot : OrderBot (m.syn) where
  bot := 0
  bot_le
    a := by
    have := m.le_add_right 0 (m.toSyn.symm a)
    simpa [map_add, zero_add]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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