sup — Mathlib

English

If f and g belong to MemLp, then their pointwise supremum f ⊔ g also belongs to MemLp.

Русский

Если f и g принадлежат MemLp, то их покомпонентное максимум определяется и принадлежит MemLp.

LaTeX

$$$\\text{MemLp}\,f\\,p\\,\\mu \\;\;\\&\\;\\text{MemLp}\\,g\\,p\\,\\mu \\Rightarrow \\text{MemLp}\\,(f\\vee g)\\,p\\,\\mu.$$$

Lean4

theorem _root_.MeasureTheory.MemLp.sup {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) : MemLp (f ⊔ g) p μ :=
  MemLp.mono' (hf.norm.add hg.norm) (hf.1.sup hg.1) (Filter.Eventually.of_forall fun x => norm_sup_le_add (f x) (g x))

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