Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-12 15:43 dc4e5cb4

View on Github →

chore(analysis): move lemmas around (#12621)

move smul_unit_ball to analysis.normed_space.pointwise, rename it to smul_unit_ball_of_pos;
reorder lemmas in analysis.normed_space.pointwise;
add vadd_ball_zero, vadd_closed_ball_zero, smul_unit, affinity_unit_ball, affinity_unit_closed_ball.

Estimated changes

Modified src/analysis/convex/gauge.lean

deleted theorem smul_unit_ball

Modified src/analysis/normed_space/pointwise.lean

added theorem affinity_unit_ball

added theorem affinity_unit_closed_ball

modified theorem normed_space.sphere_nonempty

added theorem smul_closed_unit_ball

added theorem smul_closed_unit_ball_of_nonneg

modified theorem smul_sphere

added theorem smul_unit_ball

added theorem smul_unit_ball_of_pos

added theorem vadd_ball_zero

added theorem vadd_closed_ball_zero