Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-03 00:36 e0946065

View on Github →

chore(topology/algebra/ordered,analysis/specific_limits): two more limits (#5573)

Estimated changes

Modified src/analysis/specific_limits.lean

added theorem tendsto_pow_at_top_nhds_within_0_of_lt_1

Modified src/topology/algebra/ordered.lean

added theorem filter.tendsto.div_at_top