Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-08 09:28 e0b82533

View on Github →

feat (analysis/topology/topological_space): properties of nhds, nhds_within

Estimated changes

added theorem all_mem_nhds
added theorem all_mem_nhds_filter
added theorem map_nhds_within
added theorem mem_nhds_induced
added theorem mem_nhds_subtype
added theorem mem_nhds_within
added theorem nhds_induced
added theorem nhds_subtype
added def nhds_within
added theorem nhds_within_empty
added theorem nhds_within_eq
added theorem nhds_within_inter'
added theorem nhds_within_inter
added theorem nhds_within_mono
added theorem nhds_within_restrict
added theorem nhds_within_subtype
added theorem nhds_within_union
added theorem nhds_within_univ
added theorem nhs_within_eq_of_open
added theorem principal_subtype
added theorem ptendsto'_nhds
added theorem ptendsto_nhds
added theorem rtendsto'_nhds
added theorem rtendsto_nhds
added theorem tendsto_if_nhds_within
modified theorem tendsto_nhds