Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-02 08:23 f385ad6b

View on Github →

Inductive limit of metric spaces (#732)

Estimated changes

Modified src/topology/metric_space/gluing.lean

added def metric.inductive_limit

added def metric.inductive_limit_dist

added theorem metric.inductive_limit_dist_eq_dist

added def metric.inductive_premetric

added def metric.to_inductive_limit

added theorem metric.to_inductive_limit_commute

added theorem metric.to_inductive_limit_isometry