Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-21 17:41 e0d568e5

View on Github →

feat(analysis/normed_space/basic): the rescaling of a ball is a ball (#9297) Also rename all statements with ball_0 to ball_zero for coherence.

Estimated changes

added theorem preimage_smul_inv'
added theorem preimage_smul_inv
deleted theorem ball_0_eq
added theorem ball_zero_eq
deleted theorem mem_ball_0_iff
added theorem mem_ball_zero_iff
deleted theorem mem_emetric_ball_0_iff
added theorem preimage_add_ball
added theorem preimage_add_sphere
added theorem smul_ball
added theorem smul_closed_ball'
added theorem smul_closed_ball