instQuasiCompleteSpaceOfCompleteSpace

English

If E is complete, then it is quasi-complete for any scalar field 𝕜.

Русский

Если пространство E полностью, то оно квази-полное для любого скалярного поля 𝕜.

LaTeX

$$$\\text{CompleteSpace}(E) \\Rightarrow \\text{QuasiCompleteSpace}_{\\mathbb{k}}(E)$$$

Lean4

/-- A complete space is quasi-complete with respect to any scalar ring. -/
instance [CompleteSpace E] : QuasiCompleteSpace 𝕜 E where quasiComplete _ _ := IsClosed.isComplete

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