Commit 2022-12-26 20:05 74306d81

View on Github →

feat: port Data.Set.Intervals.Disjoint (#1198)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Intervals/Disjoint.lean

added theorem IsGLB.bunionᵢ_Ici_eq_Ici

added theorem IsGLB.bunionᵢ_Ici_eq_Ioi

added theorem IsGLB.bunionᵢ_Ioi_eq

added theorem IsGLB.unionᵢ_Ioi_eq

added theorem IsLUB.bunionᵢ_Iic_eq_Iic

added theorem IsLUB.bunionᵢ_Iic_eq_Iio

added theorem IsLUB.bunionᵢ_Iio_eq

added theorem IsLUB.unionᵢ_Iio_eq

added theorem Set.Ici_disjoint_Iic

added theorem Set.Ico_disjoint_Ico

added theorem Set.Ico_disjoint_Ico_same

added theorem Set.Iic_disjoint_Ici

added theorem Set.Iic_disjoint_Ioc

added theorem Set.Iic_disjoint_Ioi

added theorem Set.Ioc_disjoint_Ioc

added theorem Set.Ioc_disjoint_Ioc_same

added theorem Set.bunionᵢ_Ico_eq_Iio_self_iff

added theorem Set.bunionᵢ_Ioc_eq_Ioi_self_iff

added theorem Set.eq_of_Ico_disjoint

added theorem Set.unionᵢ_Icc_left

added theorem Set.unionᵢ_Icc_right

added theorem Set.unionᵢ_Ici

added theorem Set.unionᵢ_Ico_eq_Iio_self_iff

added theorem Set.unionᵢ_Ico_left

added theorem Set.unionᵢ_Ico_right

added theorem Set.unionᵢ_Iic

added theorem Set.unionᵢ_Iio

added theorem Set.unionᵢ_Ioc_eq_Ioi_self_iff

added theorem Set.unionᵢ_Ioc_left

added theorem Set.unionᵢ_Ioc_right

added theorem Set.unionᵢ_Ioi

added theorem Set.unionᵢ_Ioo_left

added theorem Set.unionᵢ_Ioo_right

added theorem unionᵢ_Ici_eq_Ici_infᵢ

added theorem unionᵢ_Ici_eq_Ioi_infᵢ

added theorem unionᵢ_Iic_eq_Iic_supᵢ

added theorem unionᵢ_Iic_eq_Iio_supᵢ