inf — Mathlib

English

If f,g ∈ MemLp, then their pointwise infimum f ⊓ g belongs to MemLp.

Русский

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

LaTeX

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

Lean4

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

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