Mathlib v3 is deprecated. Go to Mathlib v4

Theorem tendsto_prod_mk_nhds

Modification history

2020-02-18 12:09
src/topology/constructions.lean
chore(topology/constructions): rename `tendsto_prod_mk_nhds` (#2008) …
Deleted tendsto_prod_mk_nhdsView on Github →
2018-08-28 15:05
analysis/topology/continuity.lean
refactor(analysis): add nndist; add finite product of metric spaces; prepare for normed spaces
Added tendsto_prod_mk_nhdsView on Github →