Commit 2026-06-06 17:04 0ed37c92

View on Github →

chore(Order/Filter/AtTopBot/Basic): use to_dual (#37747) This PR uses to_dual for atTop/atBot. A lot of theorems that have been tagged contain the expression ∀ a ≥ b, ..., which means that their dual will be ∀ a, b ≥ a → ..., which is obviourly undesirable. Hence, I would like to ask the reviewers to reconsider the possibility of merging #32985.

Estimated changes

deleted theorem Filter.atBot_Iic_eq
deleted theorem Filter.atBot_Iio_eq
deleted theorem Filter.atBot_basis'
modified theorem Filter.atBot_basis
deleted theorem Filter.atBot_basis_Iio'
deleted theorem Filter.atBot_basis_Iio
deleted theorem Filter.atBot_neBot
deleted theorem Filter.atBot_neBot_iff
deleted theorem Filter.atTop_neBot
deleted theorem Filter.eventually_atBot
modified theorem Filter.eventually_atTop
deleted theorem Filter.frequently_atBot'
deleted theorem Filter.frequently_atBot
modified theorem Filter.frequently_atTop
deleted theorem Filter.map_atBot_eq
deleted theorem Filter.map_atBot_eq_of_gc
deleted theorem Filter.map_val_Iic_atBot
deleted theorem Filter.map_val_Iio_atBot
deleted theorem Filter.mem_atBot_sets
modified theorem Filter.mem_atTop_sets
deleted theorem Filter.tendsto_Iic_atBot
deleted theorem Filter.tendsto_Iio_atBot
deleted theorem Filter.tendsto_atBot'
modified theorem Filter.tendsto_atTop'