Theorem Euclidean.isOpen_ball

Modification history

2025-03-19 19:17
Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean
chore: make `isOpen_ball` simp (#23109) …
Modified Euclidean.isOpen_ballView on Github →
2023-06-05 04:51
Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean
feat: port Analysis.InnerProductSpace.EuclideanDist (#4675)
Added Euclidean.isOpen_ballView on Github →