Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-08 00:38 90fab282

View on Github →

feat(topology/continuous_on): generalise lemma slightly (#16840) Generalise frequently_nhds_within_iff to allow within any set, not just complement of singleton

Estimated changes