instIsOrderedAddMonoid — Mathlib

English

If β is an ordered additive monoid, then the bounded continuous functions α →ᵇ β form an ordered additive monoid under pointwise addition and order: (f ≤ g) is defined pointwise, and addition respects this order.

Русский

Если β упорядоченная аддитивная моноида, то пространство ограниченно непрерывных функций α →ᵇ β образует упорядоченную аддитивную моноиду: сравнение происходит по точкам и сложение сохраняет порядок.

LaTeX

$$$f \le g \;\text{iff}\; \forall x, f(x) \le g(x)$ и $f + h$ удовлетворяет $f \le g \Rightarrow f + h \le g + h$.$$

Lean4

instance instIsOrderedAddMonoid : IsOrderedAddMonoid (α →ᵇ β) :=
  {
    add_le_add_left := by
      intro f g h₁ h t
      simp only [ContinuousMap.toFun_eq_coe, coe_toContinuousMap, coe_add, Pi.add_apply, add_le_add_iff_left]
      exact h₁ _ }

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