Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nhds_comap_dist

Modification history

2019-11-12 11:23
src/topology/metric_space/basic.lean
style(*): use notation `𝓝` for `nhds` (#1582) …
Modified nhds_comap_distView on Github →
2019-02-08 09:28
analysis/metric_space.lean
chore(*): fix errors introduced by rebasing
Deleted nhds_comap_distView on Github →
2019-02-08 09:28
analysis/metric_space.lean
feat(analysis/topology/continuity): add some variations
Added nhds_comap_distView on Github →
2018-09-07 17:43
analysis/metric_space.lean
order(filter): rename `vmap` to `comap`
Added nhds_comap_distView on Github →