Mathlib v3 is deprecated. Go to Mathlib v4

Theorem metric.closed_ball_eq_bInter_ball

Modification history

2022-10-09 00:39
src/topology/metric_space/basic.lean
feat(analysis/seminorm): closed balls for a seminorm (#16676) …
Added metric.closed_ball_eq_bInter_ballView on Github →