Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 13:55 c94a17c7

View on Github →

feat(topology): a few simple lemmas (#11360)

Estimated changes

Modified src/topology/basic.lean

added theorem eventually_mem_nhds

Modified src/topology/continuous_on.lean

added theorem continuous_at_update_same

added theorem continuous_within_at_compl_self

added theorem continuous_within_at_iff_continuous_at

modified theorem continuous_within_at_update_same

added theorem insert_mem_nhds_iff

Modified src/topology/separation.lean

added theorem continuous_at_update_of_ne

added theorem ne.nhds_within_diff_singleton