Lemmas about arithmetic operations and intervals.

inv_mem_Ixx_iff, sub_mem_Ixx_iff

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

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

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

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

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

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

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

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

add_mem_Ixx_iff_left

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

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

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

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

add_mem_Ixx_iff_right

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

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

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

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

sub_mem_Ixx_iff_left

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

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

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

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

sub_mem_Ixx_iff_right

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

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

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

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

theorem Set.mem_Icc_iff_abs_le {R : Type u_2} [LinearOrderedAddCommGroup R] {x : R} {y : R} {z : R} : |x - y| ≤ z ↔ y ∈ Set.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} [OrderedAddCommGroup α] {a : α} {b : α} : b - a ∈ Set.Icc 0 b ↔ a ∈ Set.Icc 0 b

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

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

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

theorem Set.nonempty_Ico_sdiff {α : Type u_1} [LinearOrderedAddCommGroup α] {x : α} {dx : α} {y : α} {dy : α} (h : dy < dx) (hx : 0 < dx) : Nonempty ↑(Set.Ico x (x + dx) \ Set.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} [OrderedCommGroup α] (a : α) (b : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ioc (a * b ^ n) (a * b ^ (n + 1)))

theorem Set.pairwise_disjoint_Ioc_add_zsmul {α : Type u_1} [OrderedAddCommGroup α] (a : α) (b : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ioc (a + n • b) (a + (n + 1) • b))

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

theorem Set.pairwise_disjoint_Ico_add_zsmul {α : Type u_1} [OrderedAddCommGroup α] (a : α) (b : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ico (a + n • b) (a + (n + 1) • b))

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

theorem Set.pairwise_disjoint_Ioo_add_zsmul {α : Type u_1} [OrderedAddCommGroup α] (a : α) (b : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ioo (a + n • b) (a + (n + 1) • b))

theorem Set.pairwise_disjoint_Ioc_zpow {α : Type u_1} [OrderedCommGroup α] (b : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ioc (b ^ n) (b ^ (n + 1)))

theorem Set.pairwise_disjoint_Ioc_zsmul {α : Type u_1} [OrderedAddCommGroup α] (b : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ioc (n • b) ((n + 1) • b))

theorem Set.pairwise_disjoint_Ico_zpow {α : Type u_1} [OrderedCommGroup α] (b : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ico (b ^ n) (b ^ (n + 1)))

theorem Set.pairwise_disjoint_Ico_zsmul {α : Type u_1} [OrderedAddCommGroup α] (b : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ico (n • b) ((n + 1) • b))

theorem Set.pairwise_disjoint_Ioo_zpow {α : Type u_1} [OrderedCommGroup α] (b : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ioo (b ^ n) (b ^ (n + 1)))

theorem Set.pairwise_disjoint_Ioo_zsmul {α : Type u_1} [OrderedAddCommGroup α] (b : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ioo (n • b) ((n + 1) • b))

theorem Set.pairwise_disjoint_Ioc_add_intCast {α : Type u_1} [OrderedRing α] (a : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ioc (a + ↑n) (a + ↑n + 1))

@[deprecated Set.pairwise_disjoint_Ioc_add_intCast]

theorem Set.pairwise_disjoint_Ioc_add_int_cast {α : Type u_1} [OrderedRing α] (a : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ioc (a + ↑n) (a + ↑n + 1))

Alias of Set.pairwise_disjoint_Ioc_add_intCast.

theorem Set.pairwise_disjoint_Ico_add_intCast {α : Type u_1} [OrderedRing α] (a : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ico (a + ↑n) (a + ↑n + 1))

@[deprecated Set.pairwise_disjoint_Ico_add_intCast]

theorem Set.pairwise_disjoint_Ico_add_int_cast {α : Type u_1} [OrderedRing α] (a : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ico (a + ↑n) (a + ↑n + 1))

Alias of Set.pairwise_disjoint_Ico_add_intCast.

theorem Set.pairwise_disjoint_Ioo_add_intCast {α : Type u_1} [OrderedRing α] (a : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ioo (a + ↑n) (a + ↑n + 1))

@[deprecated Set.pairwise_disjoint_Ioo_add_intCast]

theorem Set.pairwise_disjoint_Ioo_add_int_cast {α : Type u_1} [OrderedRing α] (a : α) : Pairwise (Disjoint on fun (n : ℤ) => Set.Ioo (a + ↑n) (a + ↑n + 1))

Alias of Set.pairwise_disjoint_Ioo_add_intCast.

theorem Set.pairwise_disjoint_Ico_intCast (α : Type u_1) [OrderedRing α] : Pairwise (Disjoint on fun (n : ℤ) => Set.Ico (↑n) (↑n + 1))

@[deprecated Set.pairwise_disjoint_Ico_intCast]

theorem Set.pairwise_disjoint_Ico_int_cast (α : Type u_1) [OrderedRing α] : Pairwise (Disjoint on fun (n : ℤ) => Set.Ico (↑n) (↑n + 1))

Alias of Set.pairwise_disjoint_Ico_intCast.

theorem Set.pairwise_disjoint_Ioo_intCast (α : Type u_1) [OrderedRing α] : Pairwise (Disjoint on fun (n : ℤ) => Set.Ioo (↑n) (↑n + 1))

@[deprecated Set.pairwise_disjoint_Ioo_intCast]

theorem Set.pairwise_disjoint_Ioo_int_cast (α : Type u_1) [OrderedRing α] : Pairwise (Disjoint on fun (n : ℤ) => Set.Ioo (↑n) (↑n + 1))

Alias of Set.pairwise_disjoint_Ioo_intCast.

theorem Set.pairwise_disjoint_Ioc_intCast (α : Type u_1) [OrderedRing α] : Pairwise (Disjoint on fun (n : ℤ) => Set.Ioc (↑n) (↑n + 1))

@[deprecated Set.pairwise_disjoint_Ioc_intCast]

theorem Set.pairwise_disjoint_Ioc_int_cast (α : Type u_1) [OrderedRing α] : Pairwise (Disjoint on fun (n : ℤ) => Set.Ioc (↑n) (↑n + 1))

Alias of Set.pairwise_disjoint_Ioc_intCast.