Lemmas about arithmetic operations and intervals

inv_mem_Ixx_iff, sub_mem_Ixx_iff

theorem Set.inv_mem_Icc_iff {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a c d : α} : a⁻¹ ∈ Icc c d ↔ a ∈ Icc d⁻¹ c⁻¹

theorem Set.neg_mem_Icc_iff {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a c d : α} : -a ∈ Icc c d ↔ a ∈ Icc (-d) (-c)

theorem Set.inv_mem_Ico_iff {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a c d : α} : a⁻¹ ∈ Ico c d ↔ a ∈ Ioc d⁻¹ c⁻¹

theorem Set.neg_mem_Ico_iff {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a c d : α} : -a ∈ Ico c d ↔ a ∈ Ioc (-d) (-c)

theorem Set.inv_mem_Ioc_iff {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a c d : α} : a⁻¹ ∈ Ioc c d ↔ a ∈ Ico d⁻¹ c⁻¹

theorem Set.neg_mem_Ioc_iff {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a c d : α} : -a ∈ Ioc c d ↔ a ∈ Ico (-d) (-c)

theorem Set.inv_mem_Ioo_iff {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a c d : α} : a⁻¹ ∈ Ioo c d ↔ a ∈ Ioo d⁻¹ c⁻¹

theorem Set.neg_mem_Ioo_iff {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a c d : α} : -a ∈ Ioo c d ↔ a ∈ Ioo (-d) (-c)

add_mem_Ixx_iff_left

theorem Set.add_mem_Icc_iff_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a + b ∈ Icc c d ↔ a ∈ Icc (c - b) (d - b)

theorem Set.add_mem_Ico_iff_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a + b ∈ Ico c d ↔ a ∈ Ico (c - b) (d - b)

theorem Set.add_mem_Ioc_iff_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a + b ∈ Ioc c d ↔ a ∈ Ioc (c - b) (d - b)

theorem Set.add_mem_Ioo_iff_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a + b ∈ Ioo c d ↔ a ∈ Ioo (c - b) (d - b)

add_mem_Ixx_iff_right

theorem Set.add_mem_Icc_iff_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a + b ∈ Icc c d ↔ b ∈ Icc (c - a) (d - a)

theorem Set.add_mem_Ico_iff_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a + b ∈ Ico c d ↔ b ∈ Ico (c - a) (d - a)

theorem Set.add_mem_Ioc_iff_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a + b ∈ Ioc c d ↔ b ∈ Ioc (c - a) (d - a)

theorem Set.add_mem_Ioo_iff_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a + b ∈ Ioo c d ↔ b ∈ Ioo (c - a) (d - a)

sub_mem_Ixx_iff_left

theorem Set.sub_mem_Icc_iff_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a - b ∈ Icc c d ↔ a ∈ Icc (c + b) (d + b)

theorem Set.sub_mem_Ico_iff_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a - b ∈ Ico c d ↔ a ∈ Ico (c + b) (d + b)

theorem Set.sub_mem_Ioc_iff_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a - b ∈ Ioc c d ↔ a ∈ Ioc (c + b) (d + b)

theorem Set.sub_mem_Ioo_iff_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a - b ∈ Ioo c d ↔ a ∈ Ioo (c + b) (d + b)

sub_mem_Ixx_iff_right

theorem Set.sub_mem_Icc_iff_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a - b ∈ Icc c d ↔ b ∈ Icc (a - d) (a - c)

theorem Set.sub_mem_Ico_iff_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a - b ∈ Ico c d ↔ b ∈ Ioc (a - d) (a - c)

theorem Set.sub_mem_Ioc_iff_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a - b ∈ Ioc c d ↔ b ∈ Ico (a - d) (a - c)

theorem Set.sub_mem_Ioo_iff_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α} : a - b ∈ Ioo c d ↔ b ∈ Ioo (a - d) (a - c)

theorem Set.mem_Icc_iff_abs_le {R : Type u_2} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] {x y z : R} : |x - y| ≤ z ↔ y ∈ Icc (x - z) (x + z)

sub_mem_Ixx_zero_right and sub_mem_Ixx_zero_iff_right; this specializes the previous lemmas to the case of reflecting the interval.

theorem Set.sub_mem_Icc_zero_iff_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} : b - a ∈ Icc 0 b ↔ a ∈ Icc 0 b

theorem Set.sub_mem_Ico_zero_iff_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} : b - a ∈ Ico 0 b ↔ a ∈ Ioc 0 b

theorem Set.sub_mem_Ioc_zero_iff_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} : b - a ∈ Ioc 0 b ↔ a ∈ Ico 0 b

theorem Set.sub_mem_Ioo_zero_iff_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} : b - a ∈ Ioo 0 b ↔ a ∈ Ioo 0 b

theorem Set.nonempty_Ico_sdiff {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {x dx y dy : α} (h : dy < dx) (hx : 0 < dx) : Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))

If we remove a smaller interval from a larger, the result is nonempty

Lemmas about disjointness of translates of intervals

theorem Set.pairwise_disjoint_Ioc_mul_zpow {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (a b : α) : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ioc (a * b ^ n) (a * b ^ (n + 1)))

theorem Set.pairwise_disjoint_Ioc_add_zsmul {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (a b : α) : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ioc (a + n • b) (a + (n + 1) • b))

theorem Set.pairwise_disjoint_Ico_mul_zpow {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (a b : α) : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ico (a * b ^ n) (a * b ^ (n + 1)))

theorem Set.pairwise_disjoint_Ico_add_zsmul {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (a b : α) : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ico (a + n • b) (a + (n + 1) • b))

theorem Set.pairwise_disjoint_Ioo_mul_zpow {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (a b : α) : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ioo (a * b ^ n) (a * b ^ (n + 1)))

theorem Set.pairwise_disjoint_Ioo_add_zsmul {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (a b : α) : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ioo (a + n • b) (a + (n + 1) • b))

theorem Set.pairwise_disjoint_Ioc_zpow {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (b : α) : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ioc (b ^ n) (b ^ (n + 1)))

theorem Set.pairwise_disjoint_Ioc_zsmul {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (b : α) : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ioc (n • b) ((n + 1) • b))

theorem Set.pairwise_disjoint_Ico_zpow {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (b : α) : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ico (b ^ n) (b ^ (n + 1)))

theorem Set.pairwise_disjoint_Ico_zsmul {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (b : α) : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ico (n • b) ((n + 1) • b))

theorem Set.pairwise_disjoint_Ioo_zpow {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (b : α) : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ioo (b ^ n) (b ^ (n + 1)))

theorem Set.pairwise_disjoint_Ioo_zsmul {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (b : α) : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ioo (n • b) ((n + 1) • b))

theorem Set.pairwise_disjoint_Ioc_add_intCast {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] (a : α) : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ioc (a + ↑n) (a + ↑n + 1))

theorem Set.pairwise_disjoint_Ico_add_intCast {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] (a : α) : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ico (a + ↑n) (a + ↑n + 1))

theorem Set.pairwise_disjoint_Ioo_add_intCast {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] (a : α) : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ioo (a + ↑n) (a + ↑n + 1))

theorem Set.pairwise_disjoint_Ico_intCast (α : Type u_1) [Ring α] [PartialOrder α] [IsOrderedRing α] : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ico (↑n) (↑n + 1))

theorem Set.pairwise_disjoint_Ioo_intCast (α : Type u_1) [Ring α] [PartialOrder α] [IsOrderedRing α] : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ioo (↑n) (↑n + 1))

theorem Set.pairwise_disjoint_Ioc_intCast (α : Type u_1) [Ring α] [PartialOrder α] [IsOrderedRing α] : Pairwise (Function.onFun Disjoint fun (n : ℤ) => Ioc (↑n) (↑n + 1))