Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-18 10:28 67549d93

View on Github →

feat(order/filter/at_top_bot): add at_bot versions for (almost) all at_top lemmas (#3845) There are a few lemmas I ignored, either because I thought a at_bot version wouldn't be useful (e.g subsequence lemmas), because there is no "order inversing" equivalent of monotone (I think ?), or because I just didn't understand the statement so I was unable to tell if it was useful or not.

Estimated changes

Modified src/order/filter/at_top_bot.lean

added theorem filter.at_bot_basis'

added theorem filter.at_bot_basis

added theorem filter.at_bot_countable_basis

added theorem filter.at_bot_ne_bot

added theorem filter.eventually.exists_forall_of_at_bot

added theorem filter.eventually_at_bot

added theorem filter.eventually_le_at_bot

added theorem filter.exists_le_of_tendsto_at_bot

added theorem filter.exists_lt_of_tendsto_at_bot

added theorem filter.frequently.forall_exists_of_at_bot

added theorem filter.frequently_at_bot'

added theorem filter.frequently_at_bot

added theorem filter.frequently_low_scores

added theorem filter.inf_map_at_bot_ne_bot_iff

added theorem filter.is_countably_generated_at_bot

added theorem filter.low_scores

added theorem filter.map_at_bot_eq

added theorem filter.map_at_bot_eq_of_gc

added theorem filter.mem_at_bot_sets

added theorem filter.order_bot.at_bot_eq

added theorem filter.prod_at_bot_at_bot_eq

added theorem filter.prod_map_at_bot_eq

added theorem filter.tendsto_at_bot_add_const_left

added theorem filter.tendsto_at_bot_add_const_right

added theorem filter.tendsto_at_bot_add_left_of_ge'

added theorem filter.tendsto_at_bot_add_left_of_ge

added theorem filter.tendsto_at_bot_add_nonpos_left'

added theorem filter.tendsto_at_bot_add_nonpos_left

added theorem filter.tendsto_at_bot_add_nonpos_right'

added theorem filter.tendsto_at_bot_add_nonpos_right

added theorem filter.tendsto_at_bot_add_right_of_ge'

added theorem filter.tendsto_at_bot_add_right_of_ge

added theorem filter.tendsto_at_bot_at_bot_iff_of_monotone

added theorem filter.tendsto_at_bot_at_bot_of_monotone'

added theorem filter.tendsto_at_bot_at_bot_of_monotone

added theorem filter.tendsto_at_bot_embedding

added theorem filter.tendsto_at_bot_mono'

added theorem filter.tendsto_at_bot_mono

added theorem filter.tendsto_at_bot_of_add_bdd_below_left'

added theorem filter.tendsto_at_bot_of_add_bdd_below_left

added theorem filter.tendsto_at_bot_of_add_bdd_below_right'

added theorem filter.tendsto_at_bot_of_add_bdd_below_right

added theorem filter.tendsto_at_bot_of_add_const_left

added theorem filter.tendsto_at_bot_of_add_const_right

added theorem filter.tendsto_at_bot_of_monotone_of_filter

added theorem filter.tendsto_at_bot_of_monotone_of_subseq

added theorem filter.tendsto_at_bot_principal

added theorem filter.tendsto_at_bot_pure

added theorem filter.unbounded_of_tendsto_at_bot'

added theorem filter.unbounded_of_tendsto_at_bot

added theorem filter.unbounded_of_tendsto_at_top'