orderBot — Mathlib

English

There is a bottom element (the zero function) that is ≤ every element in the lexicographic order on dependent finitely supported functions.

Русский

Существует нижний элемент (нулевая функция), который не превосходит любой другой элемент в лексикографическом порядке зависимых функций с конечной опорой.

LaTeX

$$$$ 0 \\le f \\quad \\text{для всех } f \\in \\mathrm{Lex}(\\\\Pi_i α_i) $$$$

Lean4

instance orderBot [∀ i, AddCommMonoid (α i)] [∀ i, PartialOrder (α i)] [∀ i, CanonicallyOrderedAdd (α i)] :
    OrderBot (Lex (Π₀ i, α i)) where
  bot := 0
  bot_le _ := DFinsupp.toLex_monotone bot_le

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