Theorem Metric.image_homothety_sphere_of_nonneg

Modification history

2026-09-29 20:44
Mathlib/Analysis/Normed/Affine/AddTorsor.lean
feat(Analysis/Normed/Affine): mapping ball/sphere by homothety (#43214)
Added Metric.image_homothety_sphere_of_nonnegView on Github →