Commit 2024-04-08 07:22 b8145add

View on Github →

refactor(Topology/Order/Basic): split up large file (#11992) This splits up the file Mathlib/Topology/Order/Basic.lean (currently > 2000 lines) into several smaller files.

Estimated changes

deleted theorem Filter.Tendsto.add_atBot
deleted theorem Filter.Tendsto.add_atTop
deleted theorem Filter.Tendsto.atBot_add
deleted theorem Filter.Tendsto.atTop_add
deleted theorem Icc_mem_nhds_iff
deleted theorem Ico_mem_nhds_iff
deleted theorem Ioc_mem_nhds_iff
deleted theorem IsClosed.csInf_mem
deleted theorem IsClosed.csSup_mem
deleted theorem IsClosed.isGreatest_csSup
deleted theorem IsClosed.isLeast_csInf
deleted theorem IsClosed.sInf_mem
deleted theorem IsClosed.sSup_mem
deleted theorem IsGLB.frequently_mem
deleted theorem IsGLB.frequently_nhds_mem
deleted theorem IsGLB.isGLB_of_tendsto
deleted theorem IsGLB.isLUB_of_tendsto
deleted theorem IsGLB.mem_closure
deleted theorem IsGLB.mem_of_isClosed
deleted theorem IsGLB.nhdsWithin_neBot
deleted theorem IsLUB.frequently_mem
deleted theorem IsLUB.frequently_nhds_mem
deleted theorem IsLUB.isGLB_of_tendsto
deleted theorem IsLUB.isLUB_of_tendsto
deleted theorem IsLUB.mem_closure
deleted theorem IsLUB.mem_of_isClosed
deleted theorem IsLUB.nhdsWithin_neBot
deleted theorem TFAE_mem_nhdsWithin_Ici
deleted theorem TFAE_mem_nhdsWithin_Iic
deleted theorem TFAE_mem_nhdsWithin_Iio
deleted theorem TFAE_mem_nhdsWithin_Ioi
deleted theorem closure_Ico
deleted theorem closure_Iio'
deleted theorem closure_Iio
deleted theorem closure_Ioc
deleted theorem closure_Ioi'
deleted theorem closure_Ioi
deleted theorem closure_Ioo
deleted theorem closure_interior_Icc
deleted theorem csInf_mem_closure
deleted theorem csSup_mem_closure
deleted theorem eventually_abs_sub_lt
deleted theorem exists_seq_tendsto_sInf
deleted theorem exists_seq_tendsto_sSup
deleted theorem frontier_Icc
deleted theorem frontier_Ici'
deleted theorem frontier_Ici
deleted theorem frontier_Ico
deleted theorem frontier_Iic'
deleted theorem frontier_Iic
deleted theorem frontier_Iio'
deleted theorem frontier_Iio
deleted theorem frontier_Ioc
deleted theorem frontier_Ioi'
deleted theorem frontier_Ioi
deleted theorem frontier_Ioo
deleted theorem interior_Icc
deleted theorem interior_Ici'
deleted theorem interior_Ici
deleted theorem interior_Ico
deleted theorem interior_Iic'
deleted theorem interior_Iic
deleted theorem interior_Ioc
deleted theorem isGLB_of_mem_closure
deleted theorem isGLB_of_mem_nhds
deleted theorem isLUB_of_mem_closure
deleted theorem isLUB_of_mem_nhds
deleted theorem left_nhdsWithin_Ioc_neBot
deleted theorem left_nhdsWithin_Ioo_neBot
deleted theorem map_coe_Iio_atTop
deleted theorem map_coe_Ioi_atBot
deleted theorem map_coe_Ioo_atBot
deleted theorem map_coe_Ioo_atTop
deleted theorem nhdsWithin_Ici_basis_Icc
deleted theorem nhdsWithin_Ici_basis_Ico
deleted theorem nhdsWithin_Iic_basis_Icc
deleted theorem nhdsWithin_Iio_basis'
deleted theorem nhdsWithin_Iio_eq_bot_iff
deleted theorem nhdsWithin_Iio_neBot'
deleted theorem nhdsWithin_Iio_neBot
deleted theorem nhdsWithin_Ioi_basis'
deleted theorem nhdsWithin_Ioi_basis
deleted theorem nhdsWithin_Ioi_eq_bot_iff
deleted theorem nhdsWithin_Ioi_neBot'
deleted theorem nhdsWithin_Ioi_neBot
deleted theorem nhds_basis_Icc_pos
deleted theorem nhds_basis_Ioo_pos
deleted theorem nhds_basis_Ioo_pos_of_pos
deleted theorem nhds_basis_abs_sub_lt
deleted theorem nhds_eq_iInf_abs_sub
deleted theorem orderTopology_of_nhds_abs
deleted theorem preimage_neg
deleted theorem sInf_mem_closure
deleted theorem sSup_mem_closure
deleted theorem tendsto_Iio_atTop
deleted theorem tendsto_Ioi_atBot
deleted theorem tendsto_Ioo_atBot
deleted theorem tendsto_Ioo_atTop
added theorem Icc_mem_nhds_iff
added theorem Ico_mem_nhds_iff
added theorem Ioc_mem_nhds_iff
added theorem closure_Ico
added theorem closure_Iio'
added theorem closure_Iio
added theorem closure_Ioc
added theorem closure_Ioi'
added theorem closure_Ioi
added theorem closure_Ioo
added theorem closure_interior_Icc
added theorem frontier_Icc
added theorem frontier_Ici'
added theorem frontier_Ici
added theorem frontier_Ico
added theorem frontier_Iic'
added theorem frontier_Iic
added theorem frontier_Iio'
added theorem frontier_Iio
added theorem frontier_Ioc
added theorem frontier_Ioi'
added theorem frontier_Ioi
added theorem frontier_Ioo
added theorem interior_Icc
added theorem interior_Ici'
added theorem interior_Ici
added theorem interior_Ico
added theorem interior_Iic'
added theorem interior_Iic
added theorem interior_Ioc
added theorem map_coe_Iio_atTop
added theorem map_coe_Ioi_atBot
added theorem map_coe_Ioo_atBot
added theorem map_coe_Ioo_atTop
added theorem nhdsWithin_Iio_neBot'
added theorem nhdsWithin_Iio_neBot
added theorem nhdsWithin_Ioi_neBot'
added theorem nhdsWithin_Ioi_neBot
added theorem tendsto_Iio_atTop
added theorem tendsto_Ioi_atBot
added theorem tendsto_Ioo_atBot
added theorem tendsto_Ioo_atTop
added theorem IsGLB.frequently_mem
added theorem IsGLB.isGLB_of_tendsto
added theorem IsGLB.isLUB_of_tendsto
added theorem IsGLB.mem_closure
added theorem IsGLB.mem_of_isClosed
added theorem IsGLB.nhdsWithin_neBot
added theorem IsLUB.frequently_mem
added theorem IsLUB.isGLB_of_tendsto
added theorem IsLUB.isLUB_of_tendsto
added theorem IsLUB.mem_closure
added theorem IsLUB.mem_of_isClosed
added theorem IsLUB.nhdsWithin_neBot
added theorem isGLB_of_mem_closure
added theorem isGLB_of_mem_nhds
added theorem isLUB_of_mem_closure
added theorem isLUB_of_mem_nhds
added theorem eventually_abs_sub_lt
added theorem nhdsWithin_Iio_basis'
added theorem nhdsWithin_Ioi_basis'
added theorem nhdsWithin_Ioi_basis
added theorem nhds_basis_Icc_pos
added theorem nhds_basis_Ioo_pos
added theorem nhds_basis_abs_sub_lt
added theorem nhds_eq_iInf_abs_sub
added theorem preimage_neg
added theorem IsClosed.csInf_mem
added theorem IsClosed.csSup_mem
added theorem IsClosed.isLeast_csInf
added theorem IsClosed.sInf_mem
added theorem IsClosed.sSup_mem
added theorem csInf_mem_closure
added theorem csSup_mem_closure
added theorem sInf_mem_closure
added theorem sSup_mem_closure