Commit 2022-06-21 14:57 ee123628

View on Github →

feat(topology/metric_space/basic): Add ball_comm lemmas (#14858) This adds closed_ball and sphere comm lemmas to go with the existing mem_ball_comm.

Estimated changes

Modified src/topology/metric_space/basic.lean

modified theorem metric.mem_ball'

modified theorem metric.mem_closed_ball'

added theorem metric.mem_closed_ball_comm

added theorem metric.mem_sphere'

added theorem metric.mem_sphere_comm

Modified src/topology/metric_space/emetric_space.lean

modified theorem emetric.mem_ball'

added theorem emetric.mem_closed_ball'

added theorem emetric.mem_closed_ball_comm