Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-22 04:19 6958d8cd

View on Github →

feat(topology/metric_space/{basic,emetric_space}): product of balls of the same size (#5846)

Estimated changes

Modified src/topology/metric_space/basic.lean

added theorem ball_prod_same

added theorem closed_ball_prod_same

Modified src/topology/metric_space/emetric_space.lean

added theorem emetric.ball_prod_same

added theorem emetric.closed_ball_prod_same