completeSpace_continuousMultilinearMap_iff

English

If the space of continuous multilinear maps from a family M_i to F is complete, and each M_i contains a nonzero element, then F is complete.

Русский

Если пространство непрерывных многообразных отображений из семейства M_i в F полно, и каждый M_i содержит ненулевой элемент, то F полно.

LaTeX

$$$\text{CompleteSpace}(\mathrm{ContinuousMultilinearMap}\ \mathbb{K}\, M\, F) \Rightarrow \forall i, M_i \neq 0 \Rightarrow \text{CompleteSpace}(F)$$$

Lean4

theorem completeSpace_continuousMultilinearMap_iff {m : ∀ i, M i} (hm : ∀ i, m i ≠ 0) :
    CompleteSpace (ContinuousMultilinearMap 𝕜 M F) ↔ CompleteSpace F :=
  ⟨fun _h ↦ completeSpace_of_completeSpace_continuousMultilinearMap 𝕜 F hm, fun _h ↦ inferInstance⟩

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