Commit 2024-08-06 23:04 c2f3c7e4

View on Github →

chore(Order/Filter/AtTopBot): Generalise from semilattices to directed orders (#15252) Many lemmas requiring [SemilatticeSup α] actually only need [Preorder α] [IsDirected α (· ≤ ·)].

Estimated changes

Modified Mathlib/Order/Filter/AtTopBot.lean

deleted theorem Filter.Eventually.exists_forall_of_atBot

deleted theorem Filter.Eventually.exists_forall_of_atTop

deleted theorem Filter.Frequently.forall_exists_of_atBot

deleted theorem Filter.Frequently.forall_exists_of_atTop

modified theorem Filter.HasAntitoneBasis.comp_mono

modified theorem Filter.Tendsto.prod_atBot

modified theorem Filter.Tendsto.prod_atTop

modified theorem Filter.Tendsto.prod_map_prod_atBot

modified theorem Filter.Tendsto.prod_map_prod_atTop

modified theorem Filter.atBot_basis'

modified theorem Filter.atBot_basis

added theorem Filter.atBot_basis_Iio'

added theorem Filter.atBot_basis_Iio

modified theorem Filter.atBot_countable_basis

modified theorem Filter.atBot_neBot

modified theorem Filter.atTop_basis'

modified theorem Filter.atTop_basis

modified theorem Filter.atTop_basis_Ioi'

modified theorem Filter.atTop_basis_Ioi

modified theorem Filter.atTop_countable_basis

modified theorem Filter.atTop_eq_generate_Ici

modified theorem Filter.atTop_neBot

modified theorem Filter.eventually_atBot

modified theorem Filter.eventually_atBot_curry

modified theorem Filter.eventually_atBot_prod_self'

modified theorem Filter.eventually_atBot_prod_self

modified theorem Filter.eventually_atTop

modified theorem Filter.eventually_atTop_curry

modified theorem Filter.eventually_atTop_prod_self'

modified theorem Filter.eventually_atTop_prod_self

modified theorem Filter.exists_eventually_atBot

modified theorem Filter.exists_eventually_atTop

modified theorem Filter.exists_le_of_tendsto_atBot

modified theorem Filter.exists_le_of_tendsto_atTop

modified theorem Filter.exists_lt_of_tendsto_atBot

modified theorem Filter.exists_lt_of_tendsto_atTop

modified theorem Filter.frequently_atBot'

modified theorem Filter.frequently_atBot

modified theorem Filter.frequently_atTop'

modified theorem Filter.frequently_atTop

modified theorem Filter.hasAntitoneBasis_atTop

modified theorem Filter.inf_map_atBot_neBot_iff

modified theorem Filter.inf_map_atTop_neBot_iff

modified theorem Filter.map_atBot_eq

modified theorem Filter.map_atTop_eq

modified theorem Filter.mem_atBot_sets

modified theorem Filter.mem_atTop_sets

modified theorem Filter.tendsto_atBot'

modified theorem Filter.tendsto_atBot_atBot

modified theorem Filter.tendsto_atBot_atBot_iff_of_monotone

modified theorem Filter.tendsto_atBot_atTop

modified theorem Filter.tendsto_atBot_atTop_iff_of_antitone

modified theorem Filter.tendsto_atBot_diagonal

modified theorem Filter.tendsto_atBot_principal

modified theorem Filter.tendsto_atTop'

modified theorem Filter.tendsto_atTop_atBot

modified theorem Filter.tendsto_atTop_atBot_iff_of_antitone

modified theorem Filter.tendsto_atTop_atTop

modified theorem Filter.tendsto_atTop_atTop_iff_of_monotone

modified theorem Filter.tendsto_atTop_diagonal

modified theorem Filter.tendsto_atTop_principal

modified theorem Filter.unbounded_of_tendsto_atBot'

modified theorem Filter.unbounded_of_tendsto_atBot

modified theorem Filter.unbounded_of_tendsto_atTop'

modified theorem Filter.unbounded_of_tendsto_atTop

Modified Mathlib/Topology/MetricSpace/Cauchy.lean