Commit 2025-03-19 19:17 1d296d55

View on Github →

chore: make isOpen_ball simp (#23109) This is useful for simp to close silly goals. From my PhD (MiscYD)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean

modified theorem Euclidean.isOpen_ball

Modified Mathlib/Topology/EMetricSpace/Defs.lean

modified theorem EMetric.isOpen_ball

Modified Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

modified theorem Metric.isOpen_ball