[Merged by Bors] - feat(Topology): Introduce HomeomorphClass#18689
[Merged by Bors] - feat(Topology): Introduce HomeomorphClass#18689Thmoas-Guan wants to merge 16 commits intomasterfrom
Conversation
PR summary 2c2e1f18d6
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Topology.Homeomorph | 699 | 700 | +1 (+0.14%) |
Import changes for all files
| Files | Import difference |
|---|---|
79 filesMathlib.Topology.Instances.Nat Mathlib.Topology.MetricSpace.Antilipschitz Mathlib.Analysis.Polynomial.CauchyBound Mathlib.Algebra.Order.Hom.Ultra Mathlib.Topology.Instances.PNat Mathlib.Topology.MetricSpace.ShrinkingLemma Mathlib.Topology.Instances.Int Mathlib.Topology.MetricSpace.Pseudo.Real Mathlib.Topology.ExtremallyDisconnected Mathlib.Topology.MetricSpace.Sequences Mathlib.Analysis.BoxIntegral.Box.Basic Mathlib.Analysis.Oscillation Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.Topology.Algebra.ProperAction.Basic Mathlib.Topology.MetricSpace.Cauchy Mathlib.Topology.MetricSpace.Pseudo.Basic Mathlib.Topology.Sequences Mathlib.Analysis.Normed.Field.Basic Mathlib.Topology.Order.LowerUpperTopology Mathlib.Topology.UniformSpace.AbstractCompletion Mathlib.Topology.Maps.Proper.Basic Mathlib.Topology.UniformSpace.CompleteSeparated Mathlib.Topology.MetricSpace.ProperSpace Mathlib.Topology.Homeomorph Mathlib.Topology.MetricSpace.Pseudo.Pi Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.Topology.MetricSpace.Ultra.Basic Mathlib.Topology.MetricSpace.Isometry Mathlib.Topology.Algebra.MulAction Mathlib.Topology.MetricSpace.Infsep Mathlib.Topology.Compactness.PseudometrizableLindelof Mathlib.Analysis.NormedSpace.MStructure Mathlib.Analysis.BoxIntegral.Partition.Tagged Mathlib.Topology.Algebra.ProperConstSMul Mathlib.Topology.Algebra.ConstMulAction Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.Topology.MetricSpace.Pseudo.Lemmas Mathlib.Topology.EMetricSpace.Basic Mathlib.Analysis.Normed.Group.Bounded Mathlib.Topology.UniformSpace.UniformEmbedding Mathlib.Topology.UniformSpace.Completion Mathlib.Topology.Metrizable.Basic Mathlib.Analysis.Normed.Group.Int Mathlib.Algebra.Order.Hom.Normed Mathlib.Topology.UniformSpace.UniformConvergence Mathlib.Topology.Algebra.Constructions Mathlib.Topology.UniformSpace.Cauchy Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.Topology.EMetricSpace.Diam Mathlib.Dynamics.Minimal Mathlib.Topology.MetricSpace.Basic Mathlib.Topology.Maps.Proper.UniversallyClosed Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.Topology.MetricSpace.Gluing Mathlib.Topology.UniformSpace.HeineCantor Mathlib.Analysis.BoxIntegral.Partition.Basic Mathlib.Topology.EMetricSpace.Paracompact Mathlib.Analysis.CStarAlgebra.Module.Synonym Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle Mathlib.Topology.UniformSpace.Pi Mathlib.Topology.MetricSpace.ProperSpace.Lemmas Mathlib.Topology.EMetricSpace.Pi Mathlib.InformationTheory.Hamming Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.Analysis.Normed.Group.Submodule Mathlib.Topology.Compactness.Paracompact Mathlib.Analysis.NormedSpace.IndicatorFunction Mathlib.Analysis.Normed.Group.Constructions Mathlib.Topology.UniformSpace.UniformConvergenceTopology Mathlib.Topology.Metrizable.Uniformity Mathlib.Topology.UniformSpace.Equicontinuity Mathlib.Topology.Algebra.Constructions.DomMulAct Mathlib.Analysis.BoxIntegral.Partition.Split Mathlib.Topology.MetricSpace.Ultra.TotallySeparated Mathlib.Topology.Order.MonotoneContinuity Mathlib.Topology.UniformSpace.Equiv Mathlib.Analysis.Normed.Group.Basic Mathlib.Topology.MetricSpace.Pseudo.Constructions Mathlib.Topology.MetricSpace.Bounded |
1 |
Declarations diff
+ HomeomorphClass
+ coe_coe
+ instance (priority := 100) [EquivLike F M M₂]
+ instance : HomeomorphClass (α ≃ₜ β) α β
+ instance [HomeomorphClass F α β] : CoeOut F (α ≃ₜ β)
+ instance [HomeomorphClass F α β] : ContinuousMapClass F α β
+ toHomeomorph
+ toHomeomorph_injective
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
j-loreaux
left a comment
There was a problem hiding this comment.
Thanks for this addition! Can you please also add the analogue of this lemma, and address my comments below?
@[simp]
theorem RingHom.coe_coe {α : Type u_2} {β : Type u_3} :
∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {F : Type u_5} [inst : FunLike F α β]
[inst_1 : RingHomClass F α β] (f : F), ⇑↑f = ⇑fand fix docstring
|
I would say that an instance to |
So where should I add this, I have no idea. |
also fix naming to make it consistent with current naming
|
I think it's fine to import |
I think this PR is relative small, and I don't think leave it there and just let the mess grow is a very good idea, what about I just split |
|
If you want to make a new PR splitting this file, go for it. I just didn't want to force you to do it. I would suggest doing this in stages. First, create a PR which moves this to |
add import for now, need more design on splitting this file
|
I just add this import for now, I'll deal the splitting latter. |
|
No, that would break things. |
j-loreaux
left a comment
There was a problem hiding this comment.
Can you please add instances of this class downstream (e.g., for ContinuousSemilinearEquivClass, and anything else that makes sense)?
|
Sorry that I am not familiar with these things and doesn't know what things look like downsteam, beside, is |
|
Don't worry about refactoring |
|
Added for now, but I am asking for the refactoring of it. |
j-loreaux
left a comment
There was a problem hiding this comment.
Thanks!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by j-loreaux. |
Vierkantor
left a comment
There was a problem hiding this comment.
Coming back to this to confirm that this looks good, FunLike-wise. I'd like to ask a topology maintainer to make the final decision.
Introduce HomeomorphClass
|
Pull request successfully merged into master. Build succeeded: |
Introduce HomeomorphClass