uniformEquiv_unitization_addEquiv_prod

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

/-- Bundle `WithLp.unitization_addEquiv_prod` as a `UniformEquiv`. -/
noncomputable def uniformEquiv_unitization_addEquiv_prod : WithLp 1 (Unitization 𝕜 A) ≃ᵤ WithLp 1 (𝕜 × A) :=
  {
    unitization_addEquiv_prod 𝕜
      A with
    uniformContinuous_invFun := uniformContinuous_comap' uniformContinuous_id
    uniformContinuous_toFun := uniformContinuous_iff.mpr le_rfl }

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