Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous.tendsto'

Modification history

2020-12-18 09:12
src/topology/basic.lean
chore(analysis/normed_space/basic): `continuous_at.norm` etc (#5411) …
Added continuous.tendsto'View on Github →