Mathlib v3 is deprecated. Go to Mathlib v4

Theorem metric.sphere_zero

Modification history

2021-12-15 21:49
src/topology/metric_space/basic.lean
feat(analysis/normed_space/basic): formula for `c • sphere x r` (#10814)
Added metric.sphere_zeroView on Github →