Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-08 21:30 aab5994e

View on Github →

feat(data/finset/intervals, data/set/intervals/basic): intersection of finset.Ico, union of intervals for sets and finsets (#5410)

Estimated changes

added theorem finset.Ico.coe_eq_Ico
added theorem finset.Ico.inter
added theorem finset.Ico.union'
added theorem finset.Ico.union
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.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_union_Icc'
added theorem set.Iic_union_Icc
added theorem set.Iic_union_Ioc'
added theorem set.Iic_union_Ioc
added theorem set.Iio_union_Ico'
added theorem set.Iio_union_Ico
added theorem set.Iio_union_Ioo'
added theorem set.Iio_union_Ioo
added theorem set.Ioc_union_Ioc'
added theorem set.Ioc_union_Ioi'
added theorem set.Ioc_union_Ioi
added theorem set.Ioo_union_Ioi'
added theorem set.Ioo_union_Ioi
added theorem set.Ioo_union_Ioo'
added theorem set.Ioo_union_Ioo