mono' — Mathlib

English

If hg MemLp g p μ, hf AEStronglyMeasurable f μ and h: ‖f a‖ ≤ g a, then MemLp f p μ.

Русский

Если hg MemLp g p μ, f измеримо, и ‖f a‖ ≤ g a, тогда MemLp f p μ.

LaTeX

$$$MemLp g p μ \rightarrow AEStronglyMeasurable f μ \rightarrow (\|f(a)\| ≤ g(a)) \Rightarrow MemLp f p μ.$$$

Lean4

theorem mono' {f : α → E} {g : α → ℝ} (hg : MemLp g p μ) (hf : AEStronglyMeasurable f μ) (h : ∀ᵐ a ∂μ, ‖f a‖ ≤ g a) :
    MemLp f p μ :=
  hg.of_le hf <| h.mono fun _x hx => le_trans hx (le_abs_self _)

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