Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-16 12:05 0716fa44

View on Github →

feat(data/set/intervals/basic): not_mem of various intervals (#6238) c is not in a given open/closed/unordered interval if it is outside the bounds of that interval (or if it is not in a superset of that interval).

Estimated changes

added theorem set.not_mem_subset
modified theorem set.Icc_union_Ici'
modified theorem set.Icc_union_Ici
modified theorem set.Ico_union_Ici'
modified theorem set.Ico_union_Ici
modified theorem set.Iic_union_Icc'
modified theorem set.Iic_union_Icc
modified theorem set.Iic_union_Ioc'
modified theorem set.Iic_union_Ioc
modified theorem set.Iio_union_Ico'
modified theorem set.Iio_union_Ico
modified theorem set.Iio_union_Ioo'
modified theorem set.Iio_union_Ioo
modified theorem set.Ioc_union_Ioi'
modified theorem set.Ioc_union_Ioi
modified theorem set.Ioo_union_Ioi'
modified theorem set.Ioo_union_Ioi
added theorem set.not_mem_Icc_of_gt
added theorem set.not_mem_Icc_of_lt
added theorem set.not_mem_Ici
added theorem set.not_mem_Ico_of_ge
added theorem set.not_mem_Ico_of_lt
added theorem set.not_mem_Iic
added theorem set.not_mem_Iio
added theorem set.not_mem_Ioc_of_gt
added theorem set.not_mem_Ioc_of_le
added theorem set.not_mem_Ioi
added theorem set.not_mem_Ioo_of_ge
added theorem set.not_mem_Ioo_of_le