Commit 2023-07-24 15:23 d6ce56d8

View on Github →

chore(topology/metric_space): forward-port leanprover-community/mathlib#18875 (#6095)

Estimated changes

Modified Mathlib/Topology/MetricSpace/Basic.lean

added theorem Metric.closedBall_eq_sphere_of_nonpos

added theorem Metric.nonneg_of_mem_sphere

added theorem Metric.sphere_eq_empty_of_neg

added theorem dist_pi_eq_iff

added theorem nndist_pi_eq_iff

added theorem nndist_pi_lt_iff

added theorem sphere_pi

added theorem sphere_prod