Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-27 09:41 c1a993d9

View on Github →

feat(data/set/intervals): unions of adjacent intervals (#1827)

Estimated changes

Modified src/data/set/intervals/basic.lean

added theorem set.Icc_union_Icc_eq_Icc

added theorem set.Icc_union_Ici_eq_Ioi

added theorem set.Icc_union_Ico_eq_Ico

added theorem set.Icc_union_Ioc_eq_Icc

added theorem set.Icc_union_Ioi_eq_Ioi

added theorem set.Icc_union_Ioo_eq_Ico

added theorem set.Ico_union_Icc_eq_Icc

added theorem set.Ico_union_Ici_eq_Ioi

added theorem set.Ico_union_Ico_eq_Ico

added theorem set.Iic_union_Icc_eq_Iic

modified theorem set.Iic_union_Ici

added theorem set.Iic_union_Ico_eq_Iio

added theorem set.Iic_union_Ioc_eq_Iic

modified theorem set.Iic_union_Ioi

added theorem set.Iic_union_Ioo_eq_Iio

added theorem set.Iio_union_Icc_eq_Iic

modified theorem set.Iio_union_Ici

added theorem set.Iio_union_Ico_eq_Iio

added theorem set.Ioc_union_Icc_eq_Ioc

added theorem set.Ioc_union_Ici_eq_Ioi

added theorem set.Ioc_union_Ico_eq_Ioo

added theorem set.Ioc_union_Ioc_eq_Ioc

added theorem set.Ioc_union_Ioi_eq_Ioi

added theorem set.Ioc_union_Ioo_eq_Ioo

added theorem set.Ioo_union_Icc_eq_Ioc

added theorem set.Ioo_union_Ici_eq_Ioi

added theorem set.Ioo_union_Ico_eq_Ioo

modified theorem set.nonempty_Ici

modified theorem set.nonempty_Iic

added theorem set.nonempty_Ioo