Theorem ContractingWith.toLipschitzWith

Modification history

2023-04-10 15:18

Mathlib/Topology/MetricSpace/Contracting.lean

feat: port Topology.MetricSpace.Contracting (#3323)

Added ContractingWith.toLipschitzWith View on Github →