Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-24 23:51 bf509d78

View on Github →

feat(order/filter/basic): add more lemmas about tendsto _ _ at_top (#1713)

feat(order/filter/basic): add more lemmas about tendsto _ _ at_top
Use explicit arguments as suggested by @sgouezel
Add lemmas for an ordered_comm_group
Add a missing lemma

Estimated changes

Modified src/order/filter/basic.lean

added theorem filter.tendsto_at_top_add_const_left

added theorem filter.tendsto_at_top_add_const_right

added theorem filter.tendsto_at_top_add_left_of_le'

added theorem filter.tendsto_at_top_add_left_of_le

added theorem filter.tendsto_at_top_add_nonneg_left'

added theorem filter.tendsto_at_top_add_nonneg_left

added theorem filter.tendsto_at_top_add_nonneg_right'

added theorem filter.tendsto_at_top_add_nonneg_right

added theorem filter.tendsto_at_top_add_right_of_le'

added theorem filter.tendsto_at_top_add_right_of_le

added theorem filter.tendsto_at_top_at_top_of_monotone

added theorem filter.tendsto_at_top_mono'

added theorem filter.tendsto_at_top_mono

added theorem filter.tendsto_at_top_of_add_bdd_above_left'

added theorem filter.tendsto_at_top_of_add_bdd_above_left

added theorem filter.tendsto_at_top_of_add_bdd_above_right'

added theorem filter.tendsto_at_top_of_add_bdd_above_right

added theorem filter.tendsto_at_top_of_add_const_left

added theorem filter.tendsto_at_top_of_add_const_right