Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nhds_within_Ici_self_ne_bot

Modification history

2020-12-09 04:36
src/topology/algebra/ordered.lean
feat(analysis/special_functions): `real.log` is infinitely smooth away from zero (#5116) …
Modified nhds_within_Ici_self_ne_botView on Github →
2020-07-21 15:23
src/topology/algebra/ordered.lean
feat(topology): more lemmas about Ici and Iic neighborhoods (#3474) …
Added nhds_within_Ici_self_ne_botView on Github →