Theorem Metric.contractibleSpace_closedBall

Modification history

2026-02-02 21:52
Mathlib/Analysis/Normed/Module/Connected.lean
feat(Analysis/../Connected): balls are (pre)connected (#33514) …
Added Metric.contractibleSpace_closedBallView on Github →