instCompleteSpace — Mathlib

English

Under the assumptions that E is a complete normed space and 1 ≤ p, the Banach space Lp(E,p,μ) is complete.

Русский

Предположим, что E полностью нормированное пространство, и 1 ≤ p. Тогда пространство Lp(E,p,μ) полно.

LaTeX

$$$\\text{Let } [CompleteSpace \\ E] \\text{ and } 1 \\le p. \\text{Then } Lp(E,p,\\mu) \\text{ is a complete space.}$$$

Lean4

/-- `Lp` is complete for `1 ≤ p`. -/
instance instCompleteSpace [CompleteSpace E] [hp : Fact (1 ≤ p)] : CompleteSpace (Lp E p μ) :=
  completeSpace_lp_of_cauchy_complete_eLpNorm fun _f hf _B hB h_cau => cauchy_complete_eLpNorm hp.elim hf hB.ne h_cau

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