Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-08 18:36 84dbe31d

View on Github →

feat(topology/basic): add explicit definition of continuous_at (#11296) This was convenient in a demo.

Estimated changes