Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-10 15:17 08545369

View on Github →

feat(topology/constructions): add map_fst_nhds and map_snd_nhds (#6142)

  • Move the definition of nhds_within to topology/basic. The theory is still in continuous_on.
  • Add filter.map_inf_principal_preimage.
  • Add map_fst_nhds_within, map_fst_nhds, map_snd_nhds_within, and map_snd_nhds.

Estimated changes

added def nhds_within
added theorem map_fst_nhds
added theorem map_fst_nhds_within
added theorem map_snd_nhds
added theorem map_snd_nhds_within
deleted def nhds_within