Commit 2023-02-19 17:41 e8671780

View on Github →

feat(algebra/order): unions of Ioc intervals (#2263) Forward-port lemmas in Data.Set.Intervals.Group about disjointness of intervals, from mathlib3 PR [#18427](https://github.com/leanprover-community/mathlib/pull/18427)

Estimated changes

Modified Mathlib/Data/Set/Intervals/Group.lean

added theorem Set.pairwise_disjoint_Ico_add_int_cast

added theorem Set.pairwise_disjoint_Ico_int_cast

added theorem Set.pairwise_disjoint_Ico_mul_zpow

added theorem Set.pairwise_disjoint_Ico_zpow

added theorem Set.pairwise_disjoint_Ioc_add_int_cast

added theorem Set.pairwise_disjoint_Ioc_int_cast

added theorem Set.pairwise_disjoint_Ioc_mul_zpow

added theorem Set.pairwise_disjoint_Ioc_zpow

added theorem Set.pairwise_disjoint_Ioo_add_int_cast

added theorem Set.pairwise_disjoint_Ioo_int_cast

added theorem Set.pairwise_disjoint_Ioo_mul_zpow

added theorem Set.pairwise_disjoint_Ioo_zpow