Commit 2024-04-04 21:40 d11fcd10

View on Github →

feat: allow the Open Mapping Theorem to apply to semilinear maps (#11722) this generalizes the Open Mapping Theorem for Banach spaces to semilinear maps. For now, we don't generalize the closed graph theorem. This is not because it's impossible, but only that it's currently prohibitively difficult since LinearMap.graph doesn't make sense for semilinear maps.

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Banach.lean

modified theorem AffineMap.isOpenMap

modified theorem ContinuousLinearEquiv.coeFn_ofBijective

modified theorem ContinuousLinearEquiv.coe_ofBijective

modified theorem ContinuousLinearEquiv.ofBijective_apply_symm_apply

modified theorem ContinuousLinearEquiv.ofBijective_symm_apply_apply

modified theorem ContinuousLinearMap.NonlinearRightInverse.bound

modified theorem ContinuousLinearMap.NonlinearRightInverse.right_inv

modified theorem ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot

modified theorem ContinuousLinearMap.coe_equivRange

modified theorem ContinuousLinearMap.coe_linearMap_equivRange

modified theorem ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective

modified theorem ContinuousLinearMap.nonlinearRightInverseOfSurjective_nnnorm_pos

modified theorem ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl

modified theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous

modified theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous_symm

modified theorem LinearEquiv.continuous_symm

modified def LinearEquiv.toContinuousLinearEquivOfContinuous