Commit 2025-04-02 09:50 9b4fe96d

View on Github →

chore: split Order.Interval.Set.Basic (#23556) Declarations requiring LinearOrder have been moved to Order.Interval.Set.LinearOrder.

Estimated changes

deleted theorem Set.Icc_union_Icc'
deleted theorem Set.Icc_union_Icc
deleted theorem Set.Icc_union_Icc_eq_Icc
deleted theorem Set.Icc_union_Ici'
deleted theorem Set.Icc_union_Ici
deleted theorem Set.Icc_union_Ici_eq_Ici
deleted theorem Set.Icc_union_Ico_eq_Ico
deleted theorem Set.Icc_union_Ioc_eq_Icc
deleted theorem Set.Icc_union_Ioi_eq_Ici
deleted theorem Set.Icc_union_Ioo_eq_Ico
deleted theorem Set.Ici_diff_Ici
deleted theorem Set.Ici_diff_Ioi
deleted theorem Set.Ico_diff_Iio
deleted theorem Set.Ico_eq_Ico_iff
deleted theorem Set.Ico_inter_Ico
deleted theorem Set.Ico_inter_Iio
deleted theorem Set.Ico_subset_Ico_iff
deleted theorem Set.Ico_union_Icc_eq_Icc
deleted theorem Set.Ico_union_Ici'
deleted theorem Set.Ico_union_Ici
deleted theorem Set.Ico_union_Ici_eq_Ici
deleted theorem Set.Ico_union_Ico'
deleted theorem Set.Ico_union_Ico
deleted theorem Set.Ico_union_Ico_eq_Ico
deleted theorem Set.Iic_diff_Iic
deleted theorem Set.Iic_diff_Iio
deleted theorem Set.Iic_diff_Ioc
deleted theorem Set.Iic_union_Icc'
deleted theorem Set.Iic_union_Icc
deleted theorem Set.Iic_union_Icc_eq_Iic
deleted theorem Set.Iic_union_Ici
deleted theorem Set.Iic_union_Ici_of_le
deleted theorem Set.Iic_union_Ico_eq_Iio
deleted theorem Set.Iic_union_Ioc'
deleted theorem Set.Iic_union_Ioc
deleted theorem Set.Iic_union_Ioc_eq_Iic
deleted theorem Set.Iic_union_Ioi
deleted theorem Set.Iic_union_Ioi_of_le
deleted theorem Set.Iic_union_Ioo_eq_Iio
deleted theorem Set.Iio_diff_Iic
deleted theorem Set.Iio_diff_Iio
deleted theorem Set.Iio_inj
deleted theorem Set.Iio_injective
deleted theorem Set.Iio_inter_Iio
deleted theorem Set.Iio_inter_Ioo
deleted theorem Set.Iio_subset_Iic_iff
deleted theorem Set.Iio_subset_Iio_iff
deleted theorem Set.Iio_union_Icc_eq_Iic
deleted theorem Set.Iio_union_Ici
deleted theorem Set.Iio_union_Ici_of_le
deleted theorem Set.Iio_union_Ico'
deleted theorem Set.Iio_union_Ico
deleted theorem Set.Iio_union_Ico_eq_Iio
deleted theorem Set.Iio_union_Ioi
deleted theorem Set.Iio_union_Ioi_of_lt
deleted theorem Set.Iio_union_Ioo'
deleted theorem Set.Iio_union_Ioo
deleted theorem Set.Ioc_diff_Iic
deleted theorem Set.Ioc_diff_Ioi
deleted theorem Set.Ioc_inter_Ioc
deleted theorem Set.Ioc_inter_Ioi
deleted theorem Set.Ioc_subset_Ioc_iff
deleted theorem Set.Ioc_union_Icc_eq_Ioc
deleted theorem Set.Ioc_union_Ici_eq_Ioi
deleted theorem Set.Ioc_union_Ico_eq_Ioo
deleted theorem Set.Ioc_union_Ioc'
deleted theorem Set.Ioc_union_Ioc
deleted theorem Set.Ioc_union_Ioc_eq_Ioc
deleted theorem Set.Ioc_union_Ioc_left
deleted theorem Set.Ioc_union_Ioc_right
deleted theorem Set.Ioc_union_Ioc_symm
deleted theorem Set.Ioc_union_Ioi'
deleted theorem Set.Ioc_union_Ioi
deleted theorem Set.Ioc_union_Ioi_eq_Ioi
deleted theorem Set.Ioc_union_Ioo_eq_Ioo
deleted theorem Set.Ioi_diff_Ici
deleted theorem Set.Ioi_diff_Ioi
deleted theorem Set.Ioi_inj
deleted theorem Set.Ioi_injective
deleted theorem Set.Ioi_inter_Ioi
deleted theorem Set.Ioi_inter_Ioo
deleted theorem Set.Ioi_subset_Ici_iff
deleted theorem Set.Ioi_subset_Ioi_iff
deleted theorem Set.Ioo_inter_Iio
deleted theorem Set.Ioo_inter_Ioi
deleted theorem Set.Ioo_inter_Ioo
deleted theorem Set.Ioo_subset_Ioo_iff
deleted theorem Set.Ioo_union_Icc_eq_Ioc
deleted theorem Set.Ioo_union_Ici_eq_Ioi
deleted theorem Set.Ioo_union_Ico_eq_Ioo
deleted theorem Set.Ioo_union_Ioi'
deleted theorem Set.Ioo_union_Ioi
deleted theorem Set.Ioo_union_Ioo'
deleted theorem Set.Ioo_union_Ioo
deleted theorem Set.compl_Ici
deleted theorem Set.compl_Iic
deleted theorem Set.compl_Iio
deleted theorem Set.compl_Ioc
deleted theorem Set.compl_Ioi
deleted theorem Set.not_mem_Ici
deleted theorem Set.not_mem_Iic
deleted theorem Set.not_mem_Iio
deleted theorem Set.not_mem_Ioi
added theorem Set.Icc_union_Icc'
added theorem Set.Icc_union_Icc
added theorem Set.Icc_union_Ici'
added theorem Set.Icc_union_Ici
added theorem Set.Ici_diff_Ici
added theorem Set.Ici_diff_Ioi
added theorem Set.Ico_diff_Iio
added theorem Set.Ico_eq_Ico_iff
added theorem Set.Ico_inter_Ico
added theorem Set.Ico_inter_Iio
added theorem Set.Ico_subset_Ico_iff
added theorem Set.Ico_union_Ici'
added theorem Set.Ico_union_Ici
added theorem Set.Ico_union_Ico'
added theorem Set.Ico_union_Ico
added theorem Set.Iic_diff_Iic
added theorem Set.Iic_diff_Iio
added theorem Set.Iic_diff_Ioc
added theorem Set.Iic_union_Icc'
added theorem Set.Iic_union_Icc
added theorem Set.Iic_union_Ici
added theorem Set.Iic_union_Ioc'
added theorem Set.Iic_union_Ioc
added theorem Set.Iic_union_Ioi
added theorem Set.Iio_diff_Iic
added theorem Set.Iio_diff_Iio
added theorem Set.Iio_inj
added theorem Set.Iio_injective
added theorem Set.Iio_inter_Iio
added theorem Set.Iio_inter_Ioo
added theorem Set.Iio_subset_Iic_iff
added theorem Set.Iio_subset_Iio_iff
added theorem Set.Iio_union_Ici
added theorem Set.Iio_union_Ico'
added theorem Set.Iio_union_Ico
added theorem Set.Iio_union_Ioi
added theorem Set.Iio_union_Ioo'
added theorem Set.Iio_union_Ioo
added theorem Set.Ioc_diff_Iic
added theorem Set.Ioc_diff_Ioi
added theorem Set.Ioc_inter_Ioc
added theorem Set.Ioc_inter_Ioi
added theorem Set.Ioc_subset_Ioc_iff
added theorem Set.Ioc_union_Ioc'
added theorem Set.Ioc_union_Ioc
added theorem Set.Ioc_union_Ioc_left
added theorem Set.Ioc_union_Ioc_symm
added theorem Set.Ioc_union_Ioi'
added theorem Set.Ioc_union_Ioi
added theorem Set.Ioi_diff_Ici
added theorem Set.Ioi_diff_Ioi
added theorem Set.Ioi_inj
added theorem Set.Ioi_injective
added theorem Set.Ioi_inter_Ioi
added theorem Set.Ioi_inter_Ioo
added theorem Set.Ioi_subset_Ici_iff
added theorem Set.Ioi_subset_Ioi_iff
added theorem Set.Ioo_inter_Iio
added theorem Set.Ioo_inter_Ioi
added theorem Set.Ioo_inter_Ioo
added theorem Set.Ioo_subset_Ioo_iff
added theorem Set.Ioo_union_Ioi'
added theorem Set.Ioo_union_Ioi
added theorem Set.Ioo_union_Ioo'
added theorem Set.Ioo_union_Ioo
added theorem Set.compl_Ici
added theorem Set.compl_Iic
added theorem Set.compl_Iio
added theorem Set.compl_Ioc
added theorem Set.compl_Ioi
added theorem Set.not_mem_Ici
added theorem Set.not_mem_Iic
added theorem Set.not_mem_Iio
added theorem Set.not_mem_Ioi