Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-15 21:49 8218a788

View on Github →

feat(analysis/normed_space/basic): formula for c • sphere x r (#10814)

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem normed_space.sphere_nonempty

added theorem smul_sphere'

added theorem smul_sphere

Modified src/topology/metric_space/basic.lean

added theorem metric.sphere_zero