Mathlib Changelog
v3
Changelog
About
Github
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
Modified
src/topology/basic.lean
added
theorem
all_mem_nhds
added
theorem
all_mem_nhds_filter
added
theorem
map_nhds_induced_of_surjective
added
theorem
map_nhds_within
added
theorem
mem_nhds_induced
added
theorem
mem_nhds_subtype
added
theorem
mem_nhds_within
added
theorem
mem_nhds_within_subtype
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_eq_map_subtype_val
added
theorem
nhds_within_eq_nhds_within
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_at_within_iff_subtype
added
theorem
tendsto_if_nhds_within
modified
theorem
tendsto_nhds