instAddLeftMono — Mathlib

English

The operation of addition on the left preserves order in Lp.simpleFunc: if g1 ≤ g2 then f+g1 ≤ f+g2.

Русский

Операция сложения слева сохраняет порядок в Lp.simpleFunc: если g1 ≤ g2, то f+g1 ≤ f+g2.

LaTeX

$$$\text{AddLeftMono} \; (Lp.simpleFunc\, G\, p\, μ)$$$

Lean4

instance instAddLeftMono [PartialOrder G] [IsOrderedAddMonoid G] : AddLeftMono (Lp.simpleFunc G p μ) :=
  by
  refine ⟨fun f g₁ g₂ hg₁₂ => ?_⟩
  exact add_le_add_left hg₁₂ f

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