Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-18 21:34 4faf2e21

View on Github →

chore(order/filter): use implicit arguments in tendsto_at_top etc (#4672) Also weaken some assumptions from a decidable linear order to a linear order.

Estimated changes

Modified src/data/real/hyperreal.lean

Modified src/order/filter/at_top_bot.lean

modified theorem filter.tendsto_at_bot'

modified theorem filter.tendsto_at_bot

modified theorem filter.tendsto_at_bot_at_bot

modified theorem filter.tendsto_at_bot_at_top

modified theorem filter.tendsto_at_top'

modified theorem filter.tendsto_at_top

modified theorem filter.tendsto_at_top_at_bot

modified theorem filter.tendsto_at_top_at_top

added theorem filter.tendsto_at_top_mul_at_top

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/algebra/ordered.lean

Modified src/topology/metric_space/closeds.lean

Modified src/topology/metric_space/emetric_space.lean

modified theorem emetric.tendsto_at_top

Modified src/topology/sequences.lean

Modified src/topology/uniform_space/cauchy.lean