[Merged by Bors] - feat: transfer normed spaces and continuous linear equiv's across equ…#31896
[Merged by Bors] - feat: transfer normed spaces and continuous linear equiv's across equ…#31896grunweg wants to merge 24 commits intoleanprover-community:masterfrom
Conversation
…ivalences Analogous to existing instances for e.g. linear equivalences. This is required for adding Shrink instances for these, which in turns are necessary for making the definition of immersions in leanprover-community#28793 universe-polymorphic.
PR summary e2e5306e7eImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
@Vierkantor It seems there's still a bug around the |
|
CI errors now - so it seems fixed. Sorry for the false alarm - I'm glad the linter works now :-) |
fix variable explicitness, generalise to semirings and fix variable order
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
| /-- Transfer a `Dist` across an `Equiv` -/ | ||
| protected abbrev dist (e : α ≃ β) : ∀ [Dist β], Dist α := ⟨fun x y ↦ dist (e x) (e y)⟩ | ||
|
|
||
| /-- Transfer a `PseudoMetricSpace` across an `Equiv` -/ | ||
| protected abbrev pseudometricSpace (e : α ≃ β) : ∀ [PseudoMetricSpace β], PseudoMetricSpace α := | ||
| .induced e ‹_› | ||
|
|
||
| /-- Transfer a `MetricSpace` across an `Equiv` -/ | ||
| protected abbrev metricSpace (e : α ≃ β) : ∀ [MetricSpace β], MetricSpace α := | ||
| .induced e e.injective ‹_› |
There was a problem hiding this comment.
It feels like these belong in their own file inside Topology/MetricSpace, and maybe we should add the EMetric variants, although the latter is okay to wait for another PR when we actually need them. Maybe they don't come up often enough to matter.
There was a problem hiding this comment.
Fair point. I have moved them to a new file Topology/MetricSpace/TransferInstance.lean. I've chosen to not add the EMetricSpace versions for now: most applications will be fine with using .induced, and we can always add them later if we need them.
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
|
Thank you for the quick review! I have addressed all comments. |
Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>
|
-awaiting-author |
grunweg
left a comment
There was a problem hiding this comment.
Addressed all comments!
| zero_smul := by simp [smul_def, zero_smul, zero_def] | ||
| add_smul := by simp [add_def, smul_def, add_smul] } : | ||
| Module R α) | ||
| protected abbrev module (e : α ≃ β) [AddCommMonoid β] [Module R β] : |
There was a problem hiding this comment.
I also changed this in the same way - do you prefer me to split this into its own PR?
There was a problem hiding this comment.
I made #32037 --- and am equally happy with merging this PR (containing both changes) or merging the other one first.
There was a problem hiding this comment.
No need to split, it's fine to have them in the current PR.
|
bors d+ |
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Christian Merten <christian@merten.dev>
Co-authored-by: Christian Merten <christian@merten.dev>
|
Thanks for the quick review! Let me wait after lunch; if #32037 hasn't been merged then, I'll bors this PR as-is. |
|
bors merge |
|
Pull request successfully merged into master. Build succeeded: |
…ivalences
Analogous to existing instances for e.g. linear equivalences. This is required for adding Shrink instances for these, which in turns are necessary for making the definition of immersions in #28793 universe-polymorphic.