Theorem Euclidean.isClosed_closedBall

Modification history

2023-06-05 04:51

Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean

feat: port Analysis.InnerProductSpace.EuclideanDist (#4675)

Added Euclidean.isClosed_closedBall View on Github →