orderBot

Mathlib.Data.Finsupp.Order

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

English

The bottom element in the finsupp space is the zero function; 0 ≤ f for all f.

Русский

Нижний элемент в пространстве Finsupp — нулевая функция; для любого f выполняется 0 ≤ f.

LaTeX

$$bot ≤ f$$

Lean4

instance orderBot : OrderBot (ι →₀ α) where
  bot := 0
  bot_le := by simp only [le_def, coe_zero, Pi.zero_apply, imp_true_iff, zero_le]

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

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

Разделы

Аффилиация

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