Theorem Metric.isPathConnected_ball

Modification history

2025-04-07 17:33
Mathlib/Analysis/NormedSpace/Connected.lean
feat(Analysis/NormedSpace): ball is contractible and connected (#23747) …
Added Metric.isPathConnected_ballView on Github →