instAddRightMono — Mathlib

English

Similarly, right addition preserves order: if f ≤ g then f + h ≤ g + h pointwise.

Русский

Аналогично, правое сложение сохраняет порядок: если f ≤ g, то f + h ≤ g + h по точкам.

LaTeX

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

Lean4

instance instAddRightMono [PartialOrder β] [AddZeroClass β] [ContinuousAdd β] [AddRightMono β] :
    AddRightMono C_c(α, β) :=
  ⟨fun _ _ _ hg₁₂ x => add_le_add_right (hg₁₂ x) _⟩
    -- TODO transfer this lattice structure to `BoundedContinuousFunction`

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