Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nhds_within_ne_bot_of_mem

Modification history

2019-12-18 09:23

src/topology/continuous_on.lean

refactor(topology/*): use dot notation with `compact`, prove `compact.image` with `continuous_on` (#1809) …

Added nhds_within_ne_bot_of_mem View on Github →