Commit 2026-04-07 22:06 0c420cd7

View on Github →

chore(Topology/Order/OrderClosed): use to_dual (#35638)

Estimated changes

deleted theorem Dense.Iio_eq_biUnion
deleted theorem Dense.exists_le'
deleted theorem Filter.Tendsto.min_left
deleted theorem Filter.Tendsto.min_right
deleted theorem Icc_mem_nhdsGE
deleted theorem Icc_mem_nhdsGE_of_mem
deleted theorem Icc_mem_nhdsGT
deleted theorem Icc_mem_nhdsGT_of_mem
deleted theorem Ico_mem_nhds
deleted theorem Ico_mem_nhdsGE
deleted theorem Ico_mem_nhdsGE_of_mem
deleted theorem Ico_mem_nhdsGT
deleted theorem Ico_mem_nhdsGT_of_mem
deleted theorem Iic_mem_nhds
deleted theorem Iio_mem_nhds
deleted theorem Ioc_mem_nhdsGE_of_mem
deleted theorem Ioc_mem_nhdsGT
deleted theorem Ioc_mem_nhdsGT_of_mem
deleted theorem Ioo_mem_nhdsGE_of_mem
deleted theorem Ioo_mem_nhdsGT
deleted theorem Ioo_mem_nhdsGT_of_mem
deleted theorem IsClosed.hypograph
deleted theorem IsGLB.range_of_tendsto
deleted theorem SuccOrder.nhdsLE_eq_nhds
modified theorem bddAbove_closure
deleted theorem bddBelow_closure
deleted theorem closure_Ici
deleted theorem continuous_min
deleted theorem disjoint_nhds_atTop
deleted theorem disjoint_nhds_atTop_iff
deleted theorem eventually_le_nhds
deleted theorem eventually_lt_nhds
deleted theorem frontier_Ici_subset
deleted theorem ge_of_tendsto'
deleted theorem ge_of_tendsto
deleted theorem inf_nhds_atBot
deleted theorem inf_nhds_atTop
deleted theorem interior_Iio
deleted theorem isClosed_Ici
added theorem isClosed_le_prod'
deleted theorem isOpen_Iio
deleted theorem lowerBounds_closure
deleted theorem nhdsWithin_Icc_eq_nhdsGE
deleted theorem nhdsWithin_Ico_eq_nhdsGE
deleted theorem nhdsWithin_Ioc_eq_nhdsGT
deleted theorem nhdsWithin_Ioo_eq_nhdsGT
added theorem nhds_inf_atBot
modified theorem upperBounds_closure