Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-17 12:07 0736c95c

View on Github →

chore(order/filter/basic): move some parts to new files (#3087) Move at_top/at_bot, cofinite, and ultrafilter to new files.

Estimated changes

added theorem filter.Iio_mem_at_bot
added theorem filter.Ioi_mem_at_top
added def filter.at_bot
added def filter.at_top
added theorem filter.at_top_ne_bot
added theorem filter.high_scores
added theorem filter.map_at_top_eq
added theorem filter.mem_at_bot
added theorem filter.mem_at_top
added theorem filter.mem_at_top_sets
added theorem filter.tendsto_at_top'
added theorem filter.tendsto_at_top
deleted theorem filter.Iio_mem_at_bot
deleted theorem filter.Ioi_mem_at_top
deleted def filter.at_bot
deleted def filter.at_top
deleted theorem filter.at_top_ne_bot
deleted def filter.cofinite
deleted theorem filter.cofinite_ne_bot
deleted theorem filter.eventually_at_top
deleted theorem filter.exists_ultrafilter
deleted theorem filter.frequently_at_top'
deleted theorem filter.frequently_at_top
deleted theorem filter.high_scores
deleted theorem filter.le_of_ultrafilter
deleted theorem filter.map_at_top_eq
deleted theorem filter.mem_at_bot
deleted theorem filter.mem_at_top
deleted theorem filter.mem_at_top_sets
deleted theorem filter.mem_cofinite
deleted theorem filter.prod_map_at_top_eq
deleted theorem filter.tendsto_at_top'
deleted theorem filter.tendsto_at_top
deleted def filter.ultrafilter
deleted theorem filter.ultrafilter_bind
deleted theorem filter.ultrafilter_map
deleted theorem filter.ultrafilter_of_le
deleted theorem filter.ultrafilter_pure
deleted theorem filter.ultrafilter_unique
added def filter.cofinite
added theorem filter.cofinite_ne_bot
added theorem filter.mem_cofinite
added theorem nat.cofinite_eq_at_top
added theorem filter.ultrafilter_map