continuous_toLp — Mathlib

English

The map f ↦ f.toLp p μ is a continuous map from Schwartz maps to the Lp-space; thus f ↦ f.toLp p μ is a continuous function on 𝓢(E,F).

Русский

Отображение f ↦ f.toLp p μ непрерывно по 𝓢(E,F) в пространство Lp.

LaTeX

$$$$ \\text{continuous_toLp} : 𝓢(E,F) \\to C(\\text{Lp}(E, F, μ)). $$$$

Lean4

@[fun_prop]
theorem continuous_toLp {p : ℝ≥0∞} [Fact (1 ≤ p)] {μ : Measure E} [hμ : μ.HasTemperateGrowth] :
    Continuous (fun f : 𝓢(E, F) ↦ f.toLp p μ) :=
  (toLpCLM ℝ F p μ).continuous

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