Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-24 05:18 5ef365a3

View on Github →

feat(topology/separation): generalize tendsto_const_nhds_iff to t1_space (#12883) I noticed this when working on the sphere eversion project

Estimated changes

Modified src/measure_theory/integral/lebesgue.lean

Modified src/order/filter/basic.lean

added theorem filter.map_const

Modified src/topology/separation.lean

added theorem pure_le_nhds_iff

modified theorem tendsto_const_nhds_iff