Mathlib v3 is deprecated. Go to Mathlib v4

Theorem to_nhds_mono

Modification history

2021-04-13 23:14
src/topology/uniform_space/basic.lean
refactor(src/analysis/normed_space/linear_isometry): generalize to semi_normed_group (#7122) …
Added to_nhds_monoView on Github →