English
The natural inclusion (coe) from lp(E,p) to the product ∀ i E_i is uniformly continuous, provided p ≥ 1.
Русский
Естественное включение из lp(E,p) в произведение ∀ i E_i равномерно непрерывно, при условии p ≥ 1.
LaTeX
$$$\\text{UniformContinuous}(\\mathrm{coe}: lp(E,p) \\to \\prod_{i} E_i).$$$
Lean4
/-- The coercion from `lp E p` to `∀ i, E i` is uniformly continuous. -/
theorem uniformContinuous_coe [_i : Fact (1 ≤ p)] : UniformContinuous (α := lp E p) ((↑) : lp E p → ∀ i, E i) :=
by
have hp : p ≠ 0 := (zero_lt_one.trans_le _i.elim).ne'
rw [uniformContinuous_pi]
intro i
rw [NormedAddCommGroup.uniformity_basis_dist.uniformContinuous_iff NormedAddCommGroup.uniformity_basis_dist]
intro ε hε
refine ⟨ε, hε, ?_⟩
rintro f g (hfg : ‖f - g‖ < ε)
have : ‖f i - g i‖ ≤ ‖f - g‖ := norm_apply_le_norm hp (f - g) i
exact this.trans_lt hfg
