Def Metric.inductiveLimitDist

Modification history

2023-03-11 14:23

Mathlib/Topology/MetricSpace/Gluing.lean

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

Added Metric.inductiveLimitDist View on Github →