[Merged by Bors] - feat: injective continuous linear map with closed range is a continuous linear equivalence

[winstonyin]

Added analogue of LinearEquiv.ofInjective but for ContinuousLinearEquiv on Banach spaces.

Added analogue of LinearMap.rangeRestrict but for ContinuousLinearMap.

Also I updated a docstring that had the old name of a theorem.

---

[j-loreaux]

Throughout the library we have things like ContinuousLinearMap.codRestrict which allow us to restrict a morphism to an appropriate codomain, and also versions specific to the range of the morphism (e.g., LinearMap.rangeRestrict). However, ContinuousLinearMap.rangeRestrict seems to be missing.

1. Can you add ContinuousLinearMap.rangeRestrict?
2. Provide a lemma linking your new definition to it?

[winstonyin]

I added ContinuousLinearMap.rangeRestrict and a simp lemma from rangeEquiv to it. Thanks for the quick review.

[j-loreaux]

Thanks! Almost there. Please wait for CI after you make the edits before merging.

bors d+

[mathlib-bors]

✌️ winstonyin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[j-loreaux]

@winstonyin this is delegated, you can now merge it yourself. No need to mark it awaiting-review. I'll let you merge in case there is some reason you were waiting.

EDIT: oops I see why you waited.

[j-loreaux]

FYI: I renamed to equivRange because I realized it's actually that which we have in other places in the library (which makes more sense because the symbols literally occur in the order ≃, then range). Sorry for miscommunicating before.

[j-loreaux]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style