Open mapping for complete metrizable real or complex vector spaces

This supplies the open-mapping argument needed for holomorphic function spaces with their compact-open topology. Baire's theorem first gives neighborhoods in closures of images; successive approximations and completeness remove the closure. The compatible metrics need not arise from norms and scalar multiplication need not preserve them.

Main results

isOpenMap_of_surjective_complete is the open mapping theorem for a surjective continuous linear map from a complete metrizable space to a Hausdorff metrizable Baire space. Its proof goes through a private neighborhood form: the image of every zero neighborhood is a zero neighborhood.

theorem ContinuousLinearMap.isOpenMap_of_surjective_complete {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [PseudoMetricSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [PseudoMetricSpace F] [IsUniformAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace E] [BaireSpace F] [T2Space F] (T : E →L[𝕜] F) (hs : Function.Surjective ⇑T) : IsOpenMap ⇑T

A surjective continuous real- or complex-linear map from a complete metrizable topological vector space to a Hausdorff metrizable Baire vector space is open. The metrics only need to induce the additive uniformities; they need not arise from norms.