Theorem Metric.isPathConnected_closedEBall

Modification history

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