Commit 2023-03-11 14:23 2f0f752e

View on Github →

feat: port Topology.MetricSpace.Gluing (#2711)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Real/Basic.lean

added theorem Real.infᵢ_nonneg

Created Mathlib/Topology/MetricSpace/Gluing.lean

added def Metric.GlueSpace

added def Metric.InductiveLimit

added theorem Metric.Sigma.dist_ne

added theorem Metric.Sigma.dist_same

added theorem Metric.Sigma.fst_eq_of_dist_lt_one

added def Metric.Sigma.instDist

added theorem Metric.Sigma.isometry_mk

added theorem Metric.Sigma.one_le_dist_of_ne

added theorem Metric.Sum.dist_eq

added theorem Metric.Sum.dist_eq_glueDist

added theorem Metric.Sum.one_le_dist_inl_inr

added theorem Metric.Sum.one_le_dist_inr_inl

added def Metric.glueDist

added theorem Metric.glueDist_glued_points

added theorem Metric.glueDist_swap

added def Metric.glueMetricApprox

added def Metric.gluePremetric

added def Metric.inductiveLimitDist

added theorem Metric.inductiveLimitDist_eq_dist

added def Metric.inductivePremetric

added theorem Metric.isometry_inl

added theorem Metric.isometry_inr

added theorem Metric.le_glueDist_inl_inr

added theorem Metric.le_glueDist_inr_inl

added def Metric.metricSpaceSum

added def Metric.toGlueL

added theorem Metric.toGlueL_isometry

added def Metric.toGlueR

added theorem Metric.toGlueR_isometry

added theorem Metric.toGlue_commute

added def Metric.toInductiveLimit

added theorem Metric.toInductiveLimit_commute

added theorem Metric.toInductiveLimit_isometry