Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-12 05:57 603db27a

View on Github →

feat(topology/metric_space/basic): some lemmas about dist (#13343) from the sphere eversion project

Estimated changes

added theorem dist_self_add_left
added theorem dist_self_add_right
modified theorem ball_prod_same
modified theorem closed_ball_prod_same
added theorem dist_prod_same_left
added theorem dist_prod_same_right
modified theorem prod.dist_eq