Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-03 17:57 aef7ade7

View on Github →

feat(data/set/intervals): a few lemmas needed by FTC-1 (#3653)

Estimated changes

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

modified theorem set.Ico_diff_Iio

modified theorem set.Ico_inter_Iio

added theorem set.Ioc_union_Ioc

added theorem set.Ioc_union_Ioc_left

added theorem set.Ioc_union_Ioc_right

added theorem set.Ioc_union_Ioc_symm

added theorem set.Ioc_union_Ioc_union_Ioc_cycle

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

added theorem set.Ico_disjoint_Ico_same

added theorem set.Ioc_disjoint_Ioc

added theorem set.Ioc_disjoint_Ioc_same