continuous_compLp — Mathlib

English

Under the same hypotheses as above, the map hg.compLp g0 : L^p(μ;E) → L^p(μ;F) is a continuous map.

Русский

При тех же предположениях отображение hg.compLp g0: L^p(μ;E) → L^p(μ;F) непрерывно.

LaTeX

$$$1 \\le p \\le \\infty \\;\\wedge\\; hg: L\\,ipschitzWith c\\; g,\\ g0: g(0)=0 \\Rightarrow \\text{Continuous}((hg.compLp\\ g0): L^p(E,p,\\mu) \\to L^p(F,p,\\mu)).$$$

Lean4

theorem continuous_compLp [Fact (1 ≤ p)] (hg : LipschitzWith c g) (g0 : g 0 = 0) :
    Continuous (hg.compLp g0 : Lp E p μ → Lp F p μ) :=
  (lipschitzWith_compLp hg g0).continuous

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