instCompleteSpace — Mathlib

English

If 𝕜 and A are complete, then WithLp 1 (Unitization 𝕜 A) is complete.

Русский

Если 𝕜 и A полны, то WithLp 1 (Unitization 𝕜 A) полна.

LaTeX

$$$$\\text{CompleteSpace} (WithLp 1 (Unitization 𝕜 A)).$$$$

Lean4

instance instCompleteSpace [CompleteSpace 𝕜] [CompleteSpace A] : CompleteSpace (WithLp 1 (Unitization 𝕜 A)) :=
  completeSpace_congr (uniformEquiv_unitization_addEquiv_prod 𝕜 A).isUniformEmbedding |>.mpr CompleteSpace.prod

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