completeSpace_continuousLinearMap_iff

English

If the space of continuous linear maps from E to F is complete, then F is complete.

Русский

Если пространство непрерывных линейных отображений E→F полно, то и F полно.

LaTeX

$$$\mathrm{CompleteSpace}(E \to_L F) \Rightarrow \mathrm{CompleteSpace}(F)$$$

Lean4

theorem completeSpace_continuousLinearMap_iff : CompleteSpace (E →L[𝕜] F) ↔ CompleteSpace F :=
  ⟨fun _h ↦ completeSpace_of_completeSpace_continuousLinearMap 𝕜 E F, fun _h ↦ inferInstance⟩

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