Glueing metric spaces #695
Conversation
cipher1024
force-pushed
the
master
branch
2 times, most recently
from
f623d34
to
1ed7ad1
Compare
|
So for example, if I tried to form the "line with two origins" by gluing two copies of R along the subset R - {0}, the two copies of 0 would get identified when passing to the metric space quotient so I just end up with R again, right? That is the underlying set of the glued space may not be the pushout of the original underlying sets and maps. I'm trying to think whether it makes sense to generalize any part of this to another setting, e.g., gluing sets, but it seems not to make sense, for this reason. (Which is fine, and simplifies matters in some sense.) |
|
Yes, if you want to glue metric spaces it has to be this way. For another example, if you take two copies of R and glue them along Q \cap (0,1), then in fact all the points in the closure of Q \cap (0,1) will be glued, i.e., you obtain two copies of R glued along [0,1], i.e., a tree. |
|
This looks good to me. @rwbarton Do you have any objection to merging it? |
| local attribute [instance] metric_space_sum | ||
|
|
||
| lemma sum.dist_eq {x y : α ⊕ β} : | ||
| dist x y = sum.dist x y := rfl |
| have : 0 ≤ infi (λp, dist x (Φ p) + dist y (Ψ p)) := | ||
| le_cinfi (λp, by simpa using add_le_add (@dist_nonneg _ _ x _) (@dist_nonneg _ _ y _)), | ||
| have : 0 + ε ≤ glue_dist Φ Ψ ε (inl x) (inr y) := add_le_add this (le_refl ε), | ||
| have : false, by linarith, |
There was a problem hiding this comment.
Maybe exfalso, linarith to finish the proof would be a bit more idiomatic.
|
Renamed to |
Glueing metric spaces along isometric or almost isometric subsets. The metric structure on disjoint unions in
metric_space/basic.leanis a particular case of this, so we move it from this file to the new file.