Commit 2026-04-21 17:27 a2d30da2

View on Github →

chore(Topology/Order/Basic): use to_dual (#37780)

Estimated changes

Modified Mathlib/Data/Set/Subsingleton.lean

deleted theorem Set.subsingleton_isBot

Modified Mathlib/Order/Basic.lean

Modified Mathlib/Order/Cover.lean

added theorem not_covBy_iff_exists_mem_Ioo

Modified Mathlib/Order/Filter/Ultrafilter/Basic.lean

deleted theorem Filter.atBot_eq_pure_of_isBot

Modified Mathlib/Order/Interval/Set/LinearOrder.lean

Modified Mathlib/Order/Interval/Set/Pi.lean

deleted theorem Set.pi_univ_Ico_subset

deleted theorem Set.pi_univ_Iic

deleted theorem Set.pi_univ_Iio_subset

Modified Mathlib/Topology/Order/Basic.lean

deleted theorem IsLowerSet.isClosed

deleted theorem IsUpperSet.isOpen

deleted theorem PredOrder.hasBasis_nhds_Ioc

deleted theorem PredOrder.hasBasis_nhds_Ioc_of_exists_gt

deleted theorem countable_image_gt_image_Iio

deleted theorem countable_image_gt_image_Iio_within

deleted theorem countable_image_lt_image_Iio

deleted theorem countable_image_lt_image_Iio_within

deleted theorem countable_setOf_covBy_left

deleted theorem exists_Icc_mem_subset_of_mem_nhdsLE

deleted theorem exists_Ico_subset_of_mem_nhds'

deleted theorem exists_Ico_subset_of_mem_nhds

deleted theorem ge_mem_nhds

deleted theorem gt_mem_nhds

modified theorem induced_orderTopology'

modified theorem induced_orderTopology

deleted theorem isOpen_Iio'

deleted theorem isOpen_gt'

deleted theorem nhdsLE_basis

deleted theorem nhdsLE_basis_of_exists_lt

deleted theorem nhdsLE_eq_iInf_inf_principal

deleted theorem nhdsLE_eq_iInf_principal

deleted theorem nhds_bot_basis

deleted theorem nhds_bot_basis_Iic

deleted theorem nhds_bot_order

deleted theorem pi_Ici_mem_nhds'

deleted theorem pi_Ici_mem_nhds

deleted theorem pi_Ico_mem_nhds'

deleted theorem pi_Ico_mem_nhds

deleted theorem pi_Ioi_mem_nhds'

deleted theorem pi_Ioi_mem_nhds

deleted theorem tendsto_nhds_bot_mono'

deleted theorem tendsto_nhds_bot_mono

Modified Mathlib/Topology/Order/SuccPred.lean