Theorem Metric.ball_contractible

Modification history

2026-02-02 21:52
Mathlib/Analysis/Normed/Module/Connected.lean
feat(Analysis/../Connected): balls are (pre)connected (#33514) …
Deleted Metric.ball_contractibleView on Github →
2025-04-07 17:33
Mathlib/Analysis/NormedSpace/Connected.lean
feat(Analysis/NormedSpace): ball is contractible and connected (#23747) …
Added Metric.ball_contractibleView on Github →