coeFn_compLp — Mathlib

English

The action of a Lipschitz map on Lp corresponds, almost everywhere, to composing the function with the original map on its representative.

Русский

Действие липшицевой карты на Lp почти повсеместно эквивалентно композиции функции с исходной картой на представителе.

LaTeX

$$coeFn_compLp$$

Lean4

theorem coeFn_compLp (hg : LipschitzWith c g) (g0 : g 0 = 0) (f : Lp E p μ) : hg.compLp g0 f =ᵐ[μ] g ∘ f :=
  AEEqFun.coeFn_comp _ hg.continuous _

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