LpToLpRestrictCLM_coeFn — Mathlib

English

Restriction does not increase the Lp-norm: the norm of the restricted Lp-element is less than or equal to the norm of the unrestricted one.

Русский

Ограничение не увеличивает Lp-норму: норма ограниченного элемента Lp не превышает норму исходного элемента.

LaTeX

$$$$\\|((Lp.memLp f).restrict s).toLp f\\| ≤ \\|f\\|$$$$

Lean4

theorem LpToLpRestrictCLM_coeFn [Fact (1 ≤ p)] (s : Set X) (f : Lp F p μ) :
    LpToLpRestrictCLM X F 𝕜 μ p s f =ᵐ[μ.restrict s] f :=
  MemLp.coeFn_toLp ((Lp.memLp f).restrict s)

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