English
Assuming completeness of the coordinate spaces and 1 ≤ p, the lp(E,p) space is complete: every Cauchy sequence converges within lp(E,p).
Русский
При условии полноты компонент и 1 ≤ p пространство lp(E,p) полно: каждая последовательность Коши сходится в lp(E,p).
LaTeX
$$$\\text{CompleteSpace}(lp(E,p)),$ given $1 \\le p$ and each E_i complete, i.e., every Cauchy sequence converges in lp(E,p).$$
Lean4
theorem uniformly_bounded [PseudoMetricSpace α] (g : α → ι → ℝ) {K : ℝ≥0} (hg : ∀ i, LipschitzWith K (g · i)) (a₀ : α)
(hga₀b : Memℓp (g a₀) ∞) (a : α) : Memℓp (g a) ∞ :=
by
rcases hga₀b with ⟨M, hM⟩
use ↑K * dist a a₀ + M
rintro - ⟨i, rfl⟩
calc
|g a i| = |g a i - g a₀ i + g a₀ i| := by simp
_ ≤ |g a i - g a₀ i| + |g a₀ i| := (abs_add_le _ _)
_ ≤ ↑K * dist a a₀ + M := by
gcongr
· exact lipschitzWith_iff_dist_le_mul.1 (hg i) a a₀
· exact hM ⟨i, rfl⟩
