Commit 2023-04-28 06:56 1eb993fe

View on Github →

chore: forward-port leanprover-community/mathlib#18869 (#3676)

Estimated changes

added theorem frontier_sphere'
added theorem frontier_sphere
added theorem interior_sphere'
added theorem interior_sphere
added theorem Metric.closure_sphere