Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-22 04:29 4d5ac734

View on Github →

feat(data/set/intervals): add lemmas (#15608) From sphere eversion project

Estimated changes

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

modified theorem set.Iic_union_Ici

added theorem set.Iic_union_Ici_of_le

modified theorem set.Iic_union_Ioi

added theorem set.Iic_union_Ioi_of_le

modified theorem set.Iio_union_Ici

added theorem set.Iio_union_Ici_of_le

added theorem set.Iio_union_Ioi

added theorem set.Iio_union_Ioi_of_lt

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

modified theorem set.ord_connected_interval

added theorem set.ord_connected_interval_oc

added theorem set.ord_interval.interval_oc_subset

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

added theorem set.Ioc_subset_interval_oc'

added theorem set.Ioc_subset_interval_oc