Commit 2025-12-05 15:16 e13273c9

View on Github →

chore: add variable [OrderTopology α] (#32452)

Estimated changes

Modified Mathlib/Topology/Order/Basic.lean

modified theorem Dense.topology_eq_generateFrom

modified theorem Filter.Eventually.exists_Ioo_subset

modified theorem IsLowerSet.isClosed

modified theorem IsLowerSet.isOpen

modified theorem IsOpen.exists_Ioo_subset

modified theorem IsUpperSet.isClosed

modified theorem IsUpperSet.isOpen

modified theorem PredOrder.hasBasis_nhds_Ioc

modified theorem PredOrder.hasBasis_nhds_Ioc_of_exists_gt

modified theorem SecondCountableTopology.of_separableSpace_orderTopology

modified theorem Set.PairwiseDisjoint.countable_of_Ioo

modified theorem SuccOrder.hasBasis_nhds_Ioc

modified theorem SuccOrder.hasBasis_nhds_Ioc_of_exists_lt

modified theorem countable_image_gt_image_Iio

modified theorem countable_image_gt_image_Ioi

modified theorem countable_image_lt_image_Iio

modified theorem countable_image_lt_image_Ioi

modified theorem countable_of_isolated_left'

modified theorem countable_setOf_covBy_left

modified theorem countable_setOf_covBy_right

modified theorem dense_iff_exists_between

modified theorem dense_of_exists_between

modified theorem exists_Icc_mem_subset_of_mem_nhds

modified theorem exists_Icc_mem_subset_of_mem_nhdsGE

modified theorem exists_Icc_mem_subset_of_mem_nhdsLE

modified theorem exists_Ico_subset_of_mem_nhds'

modified theorem exists_Ico_subset_of_mem_nhds

modified theorem exists_Ioc_subset_of_mem_nhds'

modified theorem exists_Ioc_subset_of_mem_nhds

modified theorem mem_nhds_iff_exists_Ioo_subset'

modified theorem mem_nhds_iff_exists_Ioo_subset

modified theorem nhds_basis_Ioo'

modified theorem nhds_basis_Ioo

modified theorem order_separated