Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-28 06:13 33afea82

View on Github →

feat(analysis/normed_space): generalize some lemmas (#12959)

  • add metric.closed_ball_zero', a version of metric.closed_ball_zero for a pseudo metric space;
  • merge metric.closed_ball_inf_dist_compl_subset_closure' with metric.closed_ball_inf_dist_compl_subset_closure, drop an unneeded assumption s ≠ univ;
  • assume r ≠ 0 instead of 0 < r in closure_ball, frontier_ball, and euclidean.closure_ball.

Estimated changes

modified theorem euclidean.closure_ball
modified theorem closure_ball
modified theorem frontier_ball
modified theorem metric.mem_of_closed'