instIsOrderedAddMonoid — Mathlib

English

The space C_c(α, β) forms an ordered additive monoid under pointwise addition and order, i.e., if f ≤ g then f + h ≤ g + h for all h.

Русский

Пространство C_c(α, β) образует упорядоченную аддитивную монаду: если f ≤ g, то f + h ≤ g + h для любого h.

LaTeX

$$$$ \forall f,g,h \in C_c(\alpha, \beta),\ f \le g \Rightarrow f + h \le g + h. $$$$

Lean4

instance : IsOrderedAddMonoid C_c(α, β) where add_le_add_left _ _ hfg c := add_le_add_left hfg c

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