Commit 2024-02-13 23:17 2cc4dd05

View on Github →

chore(Topology/Order): move OrderClosedTopology to a new file (#10497)

Estimated changes

deleted theorem Continuous.if_le
deleted theorem CovBy.nhdsWithin_Iio
deleted theorem CovBy.nhdsWithin_Ioi
deleted theorem Dense.Iio_eq_biUnion
deleted theorem Dense.Ioi_eq_biUnion
deleted theorem Dense.exists_between
deleted theorem Dense.exists_ge'
deleted theorem Dense.exists_le'
deleted theorem Dense.orderDual
deleted theorem Filter.Tendsto.min_left
deleted theorem Filter.Tendsto.min_right
deleted theorem Icc_mem_nhds
deleted theorem Icc_mem_nhdsWithin_Ici'
deleted theorem Icc_mem_nhdsWithin_Ici
deleted theorem Icc_mem_nhdsWithin_Iic'
deleted theorem Icc_mem_nhdsWithin_Iic
deleted theorem Icc_mem_nhdsWithin_Iio'
deleted theorem Icc_mem_nhdsWithin_Iio
deleted theorem Icc_mem_nhdsWithin_Ioi'
deleted theorem Icc_mem_nhdsWithin_Ioi
deleted theorem Ici_mem_nhds
deleted theorem Ico_mem_nhds
deleted theorem Ico_mem_nhdsWithin_Ici'
deleted theorem Ico_mem_nhdsWithin_Ici
deleted theorem Ico_mem_nhdsWithin_Iic
deleted theorem Ico_mem_nhdsWithin_Iio'
deleted theorem Ico_mem_nhdsWithin_Iio
deleted theorem Ico_mem_nhdsWithin_Ioi'
deleted theorem Ico_mem_nhdsWithin_Ioi
deleted theorem Iic_mem_nhds
deleted theorem Iio_mem_nhds
deleted theorem Ioc_mem_nhds
deleted theorem Ioc_mem_nhdsWithin_Ici
deleted theorem Ioc_mem_nhdsWithin_Iic'
deleted theorem Ioc_mem_nhdsWithin_Iic
deleted theorem Ioc_mem_nhdsWithin_Iio'
deleted theorem Ioc_mem_nhdsWithin_Iio
deleted theorem Ioc_mem_nhdsWithin_Ioi'
deleted theorem Ioc_mem_nhdsWithin_Ioi
deleted theorem Ioi_mem_nhds
deleted theorem Ioo_mem_nhds
deleted theorem Ioo_mem_nhdsWithin_Ici
deleted theorem Ioo_mem_nhdsWithin_Iic
deleted theorem Ioo_mem_nhdsWithin_Iio'
deleted theorem Ioo_mem_nhdsWithin_Iio
deleted theorem Ioo_mem_nhdsWithin_Ioi'
deleted theorem Ioo_mem_nhdsWithin_Ioi
deleted theorem IsClosed.epigraph
deleted theorem IsClosed.hypograph
deleted theorem IsClosed.isClosed_le
deleted theorem closure_Icc
deleted theorem closure_Ici
deleted theorem closure_Iic
deleted theorem closure_le_eq
deleted theorem closure_lt_subset_le
deleted theorem continuous_if_le
deleted theorem continuous_max
deleted theorem continuous_min
deleted theorem eventually_ge_nhds
deleted theorem eventually_gt_nhds
deleted theorem eventually_le_nhds
deleted theorem eventually_lt_nhds
deleted theorem frontier_Ici_subset
deleted theorem frontier_Iic_subset
deleted theorem frontier_le_subset_eq
deleted theorem frontier_lt_subset_eq
deleted theorem ge_of_tendsto'
deleted theorem ge_of_tendsto
deleted theorem interior_Iio
deleted theorem interior_Ioi
deleted theorem interior_Ioo
deleted theorem isClosed_Icc
deleted theorem isClosed_Ici
deleted theorem isClosed_Iic
deleted theorem isClosed_le
deleted theorem isClosed_le_prod
deleted theorem isOpen_Iio
deleted theorem isOpen_Ioi
deleted theorem isOpen_Ioo
deleted theorem isOpen_lt
deleted theorem isOpen_lt_prod
deleted theorem le_of_tendsto'
deleted theorem le_of_tendsto
deleted theorem le_of_tendsto_of_tendsto'
deleted theorem le_of_tendsto_of_tendsto
deleted theorem le_on_closure
deleted theorem lt_subset_interior_le
added theorem Continuous.if_le
added theorem CovBy.nhdsWithin_Iio
added theorem CovBy.nhdsWithin_Ioi
added theorem Dense.Iio_eq_biUnion
added theorem Dense.Ioi_eq_biUnion
added theorem Dense.exists_between
added theorem Dense.exists_ge'
added theorem Dense.exists_le'
added theorem Dense.orderDual
added theorem Icc_mem_nhds
added theorem Icc_mem_nhdsWithin_Ici
added theorem Icc_mem_nhdsWithin_Iic
added theorem Icc_mem_nhdsWithin_Iio
added theorem Icc_mem_nhdsWithin_Ioi
added theorem Ici_mem_nhds
added theorem Ico_mem_nhds
added theorem Ico_mem_nhdsWithin_Ici
added theorem Ico_mem_nhdsWithin_Iic
added theorem Ico_mem_nhdsWithin_Iio
added theorem Ico_mem_nhdsWithin_Ioi
added theorem Iic_mem_nhds
added theorem Iio_mem_nhds
added theorem Ioc_mem_nhds
added theorem Ioc_mem_nhdsWithin_Ici
added theorem Ioc_mem_nhdsWithin_Iic
added theorem Ioc_mem_nhdsWithin_Iio
added theorem Ioc_mem_nhdsWithin_Ioi
added theorem Ioi_mem_nhds
added theorem Ioo_mem_nhds
added theorem Ioo_mem_nhdsWithin_Ici
added theorem Ioo_mem_nhdsWithin_Iic
added theorem Ioo_mem_nhdsWithin_Iio
added theorem Ioo_mem_nhdsWithin_Ioi
added theorem IsClosed.epigraph
added theorem IsClosed.hypograph
added theorem IsClosed.isClosed_le
added theorem closure_Icc
added theorem closure_Ici
added theorem closure_Iic
added theorem closure_le_eq
added theorem closure_lt_subset_le
added theorem continuous_if_le
added theorem continuous_max
added theorem continuous_min
added theorem eventually_ge_nhds
added theorem eventually_gt_nhds
added theorem eventually_le_nhds
added theorem eventually_lt_nhds
added theorem frontier_Ici_subset
added theorem frontier_Iic_subset
added theorem frontier_le_subset_eq
added theorem frontier_lt_subset_eq
added theorem ge_of_tendsto'
added theorem ge_of_tendsto
added theorem interior_Iio
added theorem interior_Ioi
added theorem interior_Ioo
added theorem isClosed_Icc
added theorem isClosed_Ici
added theorem isClosed_Iic
added theorem isClosed_le
added theorem isClosed_le_prod
added theorem isOpen_Iio
added theorem isOpen_Ioi
added theorem isOpen_Ioo
added theorem isOpen_lt
added theorem isOpen_lt_prod
added theorem le_of_tendsto'
added theorem le_of_tendsto
added theorem le_on_closure
added theorem lt_subset_interior_le