Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-11 20:48 d1ef181c

View on Github →

feat(topology/metric_space/gluing): Gluing metric spaces (#695)

Estimated changes

Modified src/topology/metric_space/basic.lean

deleted def metric_space_sum

deleted theorem sum.dist_eq

deleted theorem sum.one_dist_le'

deleted theorem sum.one_dist_le

Created src/topology/metric_space/gluing.lean

added def metric.glue_dist

added theorem metric.glue_dist_glued_points

added def metric.glue_metric_approx

added def metric.glue_premetric

added def metric.glue_space

added theorem metric.isometry_on_inl

added theorem metric.isometry_on_inr

added def metric.metric_space_sum

added def metric.sum.dist

added theorem metric.sum.dist_eq

added theorem metric.sum.dist_eq_glue_dist

added theorem metric.sum.one_dist_le'

added theorem metric.sum.one_dist_le

added theorem metric.to_glue_commute

added def metric.to_glue_l

added theorem metric.to_glue_l_isometry

added def metric.to_glue_r

added theorem metric.to_glue_r_isometry