Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-30 05:20 d788d4b5

View on Github →

chore(data/set/intervals): split I??_union_I??_eq_I?? (#3237) For each lemma I??_union_I??_eq_I?? add a lemma I??_subset_I??_union_I?? with no assumptions.

Estimated changes

modified theorem set.Icc_union_Icc_eq_Icc
deleted theorem set.Icc_union_Ici_eq_Ioi
modified theorem set.Icc_union_Ico_eq_Ico
modified theorem set.Icc_union_Ioc_eq_Icc
deleted theorem set.Icc_union_Ioi_eq_Ioi
modified theorem set.Icc_union_Ioo_eq_Ico
modified theorem set.Ico_union_Icc_eq_Icc
deleted theorem set.Ico_union_Ici_eq_Ioi
modified theorem set.Ico_union_Ico_eq_Ico
modified theorem set.Ioc_union_Icc_eq_Ioc
modified theorem set.Ioc_union_Ico_eq_Ioo
modified theorem set.Ioc_union_Ioc_eq_Ioc
modified theorem set.Ioc_union_Ioo_eq_Ioo
modified theorem set.Ioo_union_Icc_eq_Ioc
modified theorem set.Ioo_union_Ico_eq_Ioo