Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-16 09:28 7b001c9c

View on Github →

feat(data/set/intervals): add missing intervals + some lemmas (#805) The lemmas about Icc ⊆ I** are important for convexity

Estimated changes

added theorem set.Icc_subset_Icc_iff
added theorem set.Icc_subset_Ici_iff
added theorem set.Icc_subset_Ico_iff
added theorem set.Icc_subset_Iic_iff
added theorem set.Icc_subset_Iio_iff
added theorem set.Icc_subset_Ioc_iff
added theorem set.Icc_subset_Ioi_iff
added theorem set.Icc_subset_Ioo_iff
added def set.Ici
added theorem set.Ici_ne_empty
added def set.Iic
added theorem set.Iic_ne_empty
added def set.Ioc
added theorem set.Ioc_eq_empty
added def set.Ioi
added theorem set.Ioi_ne_empty
added theorem set.mem_Ici
added theorem set.mem_Iic
added theorem set.mem_Ioc
added theorem set.mem_Ioi