Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nhds_within_eq_of_open

Modification history

2021-09-14 04:32
src/topology/continuous_on.lean
feat(topology): one-point compactification of a topological space (#8579) …
Deleted nhds_within_eq_of_openView on Github →
2019-10-08 13:51
src/topology/basic.lean
refactor(topology/continuous_on): move continuous_{on,within_at} to own file (#1516) …
Modified nhds_within_eq_of_openView on Github →
2019-04-10 17:49
src/topology/basic.lean
feat(analysis/normed_space/deriv): show that the differential is unique (2) (#916) …
Added nhds_within_eq_of_openView on Github →