Commit 2023-05-20 01:21 81b31372

View on Github →

feat: port Analysis.NormedSpace.Banach (#4122)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Banach.lean

added theorem AffineMap.isOpenMap

added theorem ContinuousLinearEquiv.coeFn_ofBijective

added theorem ContinuousLinearEquiv.coe_ofBijective

added theorem ContinuousLinearEquiv.ofBijective_apply_symm_apply

added theorem ContinuousLinearEquiv.ofBijective_symm_apply_apply

added theorem ContinuousLinearMap.NonlinearRightInverse.bound

added theorem ContinuousLinearMap.NonlinearRightInverse.right_inv

added structure ContinuousLinearMap.NonlinearRightInverse

added theorem ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot

added theorem ContinuousLinearMap.closure_preimage

added theorem ContinuousLinearMap.coeFn_ofIsClosedGraph

added theorem ContinuousLinearMap.coeFn_ofSeqClosedGraph

added theorem ContinuousLinearMap.coe_ofIsClosedGraph

added theorem ContinuousLinearMap.coe_ofSeqClosedGraph

added theorem ContinuousLinearMap.exists_approx_preimage_norm_le

added theorem ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective

added theorem ContinuousLinearMap.exists_preimage_norm_le

added theorem ContinuousLinearMap.frontier_preimage

added theorem ContinuousLinearMap.interior_preimage

added theorem ContinuousLinearMap.nonlinearRightInverseOfSurjective_nnnorm_pos

added def ContinuousLinearMap.ofIsClosedGraph

added def ContinuousLinearMap.ofSeqClosedGraph

added theorem ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl

added theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous

added theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous_symm

added theorem LinearEquiv.continuous_symm

added def LinearEquiv.toContinuousLinearEquivOfContinuous

added theorem LinearMap.continuous_of_isClosed_graph

added theorem LinearMap.continuous_of_seq_closed_graph