Theorem dist_ofAdd

Modification history

2024-08-16 01:08

Mathlib/Topology/MetricSpace/Basic.lean

chore: splitting up metric spaces files (#15790)

Modified dist_ofAdd View on Github →

2023-03-03 17:48

Mathlib/Topology/MetricSpace/Basic.lean

feat: port Topology.MetricSpace.Basic (#2425)

Added dist_ofAdd View on Github →