Commit 2020-02-18 12:09 115e5135

View on Github →

chore(topology/constructions): rename tendsto_prod_mk_nhds (#2008) New name is tendsto.prod_mk_nhds. Also use it in a few proofs and generalize tendsto_smul to a topological_semimodule.

Estimated changes

Modified src/analysis/calculus/tangent_cone.lean

Modified src/analysis/normed_space/basic.lean

deleted theorem tendsto_smul

deleted theorem tendsto_smul_const

Modified src/topology/algebra/module.lean

modified theorem continuous.smul

added theorem filter.tendsto.smul

added theorem tendsto_smul

Modified src/topology/algebra/monoid.lean

Modified src/topology/constructions.lean

added theorem filter.tendsto.prod_mk_nhds

deleted theorem tendsto_prod_mk_nhds

Modified src/topology/continuous_on.lean

Modified src/topology/instances/ennreal.lean