Commit 2026-09-03 12:01 7e283a73

View on Github →

chore(Order/Filter/AtTopBot): use to_dual more (#43385)

Estimated changes

Modified Mathlib/Data/Set/Finite/Lemmas.lean

deleted theorem Set.exists_max_image

deleted theorem Set.exists_upper_bound_image

Modified Mathlib/Order/Filter/AtTopBot/CompleteLattice.lean

deleted theorem Antitone.ciInf_comp_tendsto_atTop

deleted theorem Antitone.ciSup_comp_tendsto_atBot_of_linearOrder

deleted theorem Antitone.iInf_comp_tendsto_atTop

deleted theorem Filter.Subsingleton.atBot_eq

deleted theorem Monotone.ciInf_comp_tendsto_atBot

deleted theorem Monotone.ciInf_comp_tendsto_atBot_of_linearOrder

deleted theorem Monotone.iInf_comp_tendsto_atBot

Modified Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean

deleted theorem Filter.atBot_countable_basis

Modified Mathlib/Order/Filter/AtTopBot/Finite.lean

deleted theorem Filter.Tendsto.eventually_forall_le_atBot

deleted theorem Filter.eventually_forall_le_atBot

deleted theorem Filter.frequently_low_scores

deleted theorem Filter.low_scores

Modified Mathlib/Order/Filter/AtTopBot/Prod.lean

deleted theorem Filter.Tendsto.prod_atBot

deleted theorem Filter.Tendsto.prod_map_prod_atBot

deleted theorem Filter.eventually_atBot_curry

deleted theorem Filter.eventually_atBot_prod_self'

deleted theorem Filter.eventually_atBot_prod_self

deleted theorem Filter.prod_atBot_atBot_eq

deleted theorem Filter.prod_map_atBot_eq

deleted theorem Filter.tendsto_atBot_diagonal