orderBot — Mathlib

English

The Lex order on α →₀ N has a bottom element (the zero finsupp) and this bottom is less than or equal to every element.

Русский

У порядка Lex на α →₀ N есть нулевой элемент (нулевая FinSupp) и он не больше любого элемента.

LaTeX

$$$0 \\le f \\quad \\text{for all } f \\in \\mathrm{Lex}(\\alpha \\to_0 N)$$$

Lean4

instance orderBot [AddCommMonoid N] [PartialOrder N] [CanonicallyOrderedAdd N] : OrderBot (Lex (α →₀ N))
    where
  bot := 0
  bot_le _ := Finsupp.toLex_monotone bot_le

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