Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.tendsto.prod_mk_nhds

Modification history

2020-02-18 12:09
src/topology/constructions.lean
chore(topology/constructions): rename `tendsto_prod_mk_nhds` (#2008) …
Added filter.tendsto.prod_mk_nhdsView on Github →