[Merged by Bors] - feat: generalize normed instances on UniformSpace.Completion#17059
[Merged by Bors] - feat: generalize normed instances on UniformSpace.Completion#17059eric-wieser wants to merge 5 commits intomasterfrom
UniformSpace.Completion#17059Conversation
PR summary e4e68829f5
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Topology.MetricSpace.Algebra | 990 | 1002 | +12 (+1.21%) |
| Mathlib.Analysis.Normed.MulAction | 1100 | 1111 | +11 (+1.00%) |
| Mathlib.Topology.MetricSpace.Completion | 1085 | 1087 | +2 (+0.18%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Topology.MetricSpace.GromovHausdorff |
1 |
Mathlib.Topology.MetricSpace.Completion |
2 |
7 filesMathlib.Analysis.Normed.Group.Uniform Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Analysis.Normed.Group.Hom |
3 |
Mathlib.Analysis.Normed.MulAction |
11 |
Mathlib.Topology.MetricSpace.Algebra |
12 |
Declarations diff
+ instance (priority := 100) BoundedSMul.toUniformContinuousConstSMul :
+ instance [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
+ instance [NormedField 𝕜] [SeminormedCommRing A] [NormedAlgebra 𝕜 A] :
+ instance [SeminormedCommRing A] : NormedCommRing (Completion A)
+ instance {M} [Zero M] [Zero α] [SMul M α] [PseudoMetricSpace M] [BoundedSMul M α] :
- instance (priority := 100) NormedSpace.to_uniformContinuousConstSMul :
- instance : NormedSpace 𝕜 (Completion E)
- instance [SeminormedCommRing A] [NormedAlgebra 𝕜 A] [UniformContinuousConstSMul 𝕜 A] :
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.
| dist_eq := fun x y => by | ||
| refine Completion.induction_on₂ x y ?_ ?_ <;> clear x y | ||
| · refine isClosed_eq (Completion.uniformContinuous_extension₂ _).continuous ?_ | ||
| exact Continuous.comp Completion.continuous_extension continuous_sub | ||
| · intro x y | ||
| rw [← Completion.coe_sub, norm_coe, Completion.dist_eq, dist_eq_norm] |
There was a problem hiding this comment.
This proof was a duplicate of one in another file.
| dist_eq x y := by | ||
| refine induction_on₂ x y ?_ (by simp [← coe_sub, dist_eq_norm]) | ||
| exact isClosed_eq (uniformContinuous_extension₂ _).continuous (by fun_prop) |
There was a problem hiding this comment.
Apparently this result is really fun to reprove for a third time.
| existsi PUnit, inferInstance, inferInstance | ||
| ext x | ||
| simp only [Seminorm.zero_apply, Seminorm.comp_apply, coe_normSeminorm] | ||
| have heq : toDualContinuousMultilinearMap PUnit x = 0 := by ext _ |
There was a problem hiding this comment.
This have started specializing to PUnit.{0}, which broke the rw below. Inlining into the rw to force contextual unification seems to do the trick.
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
Notably, `NormedSpace.to_uniformContinuousConstSMul` is generalized to `BoundedSMul` on `PseudoMetricSpace`s, relaxing the scalar considerably from normed fields. Co-authored-by: Eric Wieser <efw@google.com>
|
Pull request successfully merged into master. Build succeeded: |
UniformSpace.CompletionUniformSpace.Completion
Notably, `NormedSpace.to_uniformContinuousConstSMul` is generalized to `BoundedSMul` on `PseudoMetricSpace`s, relaxing the scalar considerably from normed fields. Co-authored-by: Eric Wieser <efw@google.com>
Notably,
NormedSpace.to_uniformContinuousConstSMulis generalized toBoundedSMulonPseudoMetricSpaces, relaxing the scalar considerably from normed fields.