instAddLeftMono — Mathlib

English

For any f ∈ Lp(E, p, μ) and any g1, g2 ∈ Lp(E, p, μ) with g1 ≤ g2 (pointwise), we have f + g1 ≤ f + g2 in Lp, i.e., left addition is order-preserving.

Русский

Для любых f ∈ Lp(E, p, μ) и g1, g2 ∈ Lp(E, p, μ) таких, что g1 ≤ g2 покомпонентно, выполняется f + g1 ≤ f + g2 в Lp: слева сложение сохраняет порядок.

LaTeX

$$$\forall f,g_1,g_2\in L^p(E,\mu),\; g_1\le g_2\;\Rightarrow\; f+g_1\le f+g_2.$$$

Lean4

instance instAddLeftMono : AddLeftMono (Lp E p μ) :=
  by
  refine ⟨fun f g₁ g₂ hg₁₂ => ?_⟩
  rw [← coeFn_le] at hg₁₂ ⊢
  filter_upwards [coeFn_add f g₁, coeFn_add f g₂, hg₁₂] with _ h1 h2 h3
  rw [h1, h2, Pi.add_apply, Pi.add_apply]
  exact add_le_add le_rfl h3

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