Commit 2026-09-29 20:44 ce482de4

View on Github →

feat(Analysis/Normed/Affine): mapping ball/sphere by homothety (#43214)

Estimated changes

Modified Mathlib/Analysis/Normed/Affine/AddTorsor.lean

added theorem Metric.image_homothety_ball

added theorem Metric.image_homothety_closedBall

added theorem Metric.image_homothety_closedBall_of_nonneg

added theorem Metric.image_homothety_sphere

added theorem Metric.image_homothety_sphere_of_nonneg

Modified Mathlib/Analysis/Normed/Group/Pointwise.lean

Modified Mathlib/Analysis/Normed/Module/Convex.lean

Modified Mathlib/Topology/MetricSpace/IsometricSMul.lean

deleted theorem Metric.smul_ball

deleted theorem Metric.smul_closedBall

deleted theorem Metric.smul_sphere