Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-22 15:49 a9c13002

View on Github →

refactor(topology/metric_space/basic): rename closed_ball_Icc (#8790)

  • rename closed_ball_Icc to real.closed_ball_eq;
  • add real.ball_eq, int.ball_eq, int.closed_ball_eq, int.preimage_ball, int.preimage_closed_ball.

Estimated changes

added theorem int.ball_eq
added theorem int.closed_ball_eq
modified theorem int.dist_cast_rat
modified theorem int.dist_cast_real
modified theorem int.dist_eq
added theorem int.preimage_ball
deleted theorem closed_ball_Icc
added theorem real.ball_eq
added theorem real.closed_ball_eq