Commit 2025-04-07 17:33 bf29636a
View on Github →feat(Analysis/NormedSpace): ball is contractible and connected (#23747)
Prove that balls (Metric.ball and EMetric.ball) in normed spaces over reals are contractible, path-connected and connected.
feat(Analysis/NormedSpace): ball is contractible and connected (#23747)
Prove that balls (Metric.ball and EMetric.ball) in normed spaces over reals are contractible, path-connected and connected.