Commit 2025-11-21 15:41 4c34f6c6

View on Github →

feat: ContinuousLinearEquiv.submoduleMap and friends (#31899) The continuous analogue of LinearEquiv.{submoduleMap, submoduleMap', ofSubmodules}. Also add ContinuousLinearMap.ofEq and Homeomorph.ofEqSubtypes, as these are necessary for the proof. This will be used in #28793 for dealing with a universe-polymorphic definition for smooth immersions.

Estimated changes

Modified Mathlib/Topology/Algebra/Module/Equiv.lean

added def ContinuousLinearEquiv.ofEq

added def ContinuousLinearEquiv.ofSubmodule'

added theorem ContinuousLinearEquiv.ofSubmodule'_apply

added theorem ContinuousLinearEquiv.ofSubmodule'_symm_apply

added theorem ContinuousLinearEquiv.ofSubmodule'_toContinuousLinearMap

added def ContinuousLinearEquiv.ofSubmodules

added theorem ContinuousLinearEquiv.ofSubmodules_apply

added theorem ContinuousLinearEquiv.ofSubmodules_symm_apply

added def ContinuousLinearEquiv.submoduleMap

added theorem ContinuousLinearEquiv.submoduleMap_apply

added theorem ContinuousLinearEquiv.submoduleMap_symm_apply

Modified Mathlib/Topology/Constructions.lean

added def Homeomorph.ofEqSubtypes

added theorem Homeomorph.ofEqSubtypes_toEquiv