Theorem Metric.isPathConnected_eball

Modification history

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