Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nhds_of_nhds_within_of_nhds

Modification history

2020-06-22 13:19
src/topology/continuous_on.lean
feat(analysis/calculus): C^1 implies strictly differentiable (#3119) …
Added nhds_of_nhds_within_of_nhdsView on Github →