Theorem Metric.isConnected_ball

Modification history

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