English
The projection map lp E p → ∀ i, E_i is uniformly continuous; this restates the previous fact in the lp context.
Русский
Проективное отображение lp E p → ∀ i, E_i равномерно непрерывно; это повторяет предыдущее свойство в контексте lp.
LaTeX
$$$\\text{UniformContinuous}(\\mathrm{Subtype.val}: lp(E,p) \\to ∀ i, E_i).$$$
Lean4
theorem norm_apply_le_of_tendsto {C : ℝ} {F : ι → lp E ∞} (hCF : ∀ᶠ k in l, ‖F k‖ ≤ C) {f : ∀ a, E a}
(hf : Tendsto (id fun i => F i : ι → ∀ a, E a) l (𝓝 f)) (a : α) : ‖f a‖ ≤ C :=
by
have : Tendsto (fun k => ‖F k a‖) l (𝓝 ‖f a‖) := (Tendsto.comp (continuous_apply a).continuousAt hf).norm
refine le_of_tendsto this (hCF.mono ?_)
intro k hCFk
exact (norm_apply_le_norm ENNReal.top_ne_zero (F k) a).trans hCFk
