coeFn_compLp — Mathlib

English

The pointwise application of a Lipschitz operator L to an L^p-function f coincides with the composition L ∘ f almost everywhere.

Русский

Точечное применение липшицевой операции L к функции f в L^p совпадает с композицией L ∘ f почти повсеместно.

LaTeX

$$$\\forall f \\in L^p(E,p,\\mu): (L \\circ f)(a) = L(f(a)) \\quad \\text{for a.e. } a.$$$

Lean4

theorem coeFn_compLp (L : E →SL[σ] F) (f : Lp E p μ) : ∀ᵐ a ∂μ, (L.compLp f) a = L (f a) :=
  LipschitzWith.coeFn_compLp _ _ _

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