Def Metric.glueMetricApprox

Modification history

2024-08-07 07:08

Mathlib/Topology/MetricSpace/Gluing.lean

chore: backports for leanprover/lean4#4814 (part 21) (#15510)

Modified Metric.glueMetricApprox View on Github →

2023-03-11 14:23

Mathlib/Topology/MetricSpace/Gluing.lean

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

Added Metric.glueMetricApprox View on Github →