Commit 2026-02-27 15:01 9e156ec0

feat: equivalent characterisation of split continuous linear maps (#35057) We add an equivalent characterisation of continuous linear maps with a continuous left inverse: f admits a continuous left inverse iff it is injective, has closed range and range f has a closed complement. This equivalence is used for extracting an explicit complement for immersions, hence transitively for proving that immersions are closed under composition. From the path towards immersions, submersions and embedded submanifolds.