Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-28 10:05 340fa146

View on Github →

feat(analysis/specific_limits): add a few more limits (#1832)

feat(analysis/specific_limits): add a few more limits
Drop 1 lemma, generalize two others.
Rename tendsto_inverse_at_top_nhds_0, fix compile

Estimated changes

Modified src/analysis/calculus/tangent_cone.lean

Modified src/analysis/complex/exponential.lean

Modified src/analysis/specific_limits.lean

added theorem lim_norm_zero'

added theorem normed_field.tendsto_norm_inverse_nhds_within_0_at_top

added theorem tendsto_inv_at_top_zero'

added theorem tendsto_inv_at_top_zero

deleted theorem tendsto_inverse_at_top_nhds_0

added theorem tendsto_norm_at_top_at_top

Modified src/topology/algebra/ordered.lean

added theorem tendsto_abs_at_top_at_top