← Copula mathematical handbook

Vector spaces over nontrivially normed fields are perfect spaces

theorem perfectSpace_of_module (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nontrivial E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] : PerfectSpace E

instance instPerfectSpace (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] : PerfectSpace 𝕜