Documentation

Mathlib.Data.Set.Intervals.Group

Lemmas about arithmetic operations and intervals. #

inv_mem_Ixx_iff, sub_mem_Ixx_iff

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_Icc_iff {α : Type u_1} [OrderedCommGroup α] {a : α} {c : α} {d : α} :
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_Ico_iff {α : Type u_1} [OrderedCommGroup α] {a : α} {c : α} {d : α} :
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_Ioc_iff {α : Type u_1} [OrderedCommGroup α] {a : α} {c : α} {d : α} :
theorem Set.neg_mem_Ioo_iff {α : Type u_1} [OrderedAddCommGroup α] {a : α} {c : α} {d : α} :
-a Set.Ioo c d a Set.Ioo (-d) (-c)
theorem Set.inv_mem_Ioo_iff {α : Type u_1} [OrderedCommGroup α] {a : α} {c : α} {d : α} :

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)
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_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_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_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_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_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_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_Ioc_zsmul {α : Type u_1} [OrderedAddCommGroup α] (b : α) :
Pairwise (Disjoint on fun n => Set.Ioc (n b) ((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_Ico_zsmul {α : Type u_1} [OrderedAddCommGroup α] (b : α) :
Pairwise (Disjoint on fun n => Set.Ico (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_Ioo_zsmul {α : Type u_1} [OrderedAddCommGroup α] (b : α) :
Pairwise (Disjoint on fun n => Set.Ioo (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_Ioc_add_int_cast {α : Type u_1} [OrderedRing α] (a : α) :
Pairwise (Disjoint on fun n => Set.Ioc (a + n) (a + n + 1))
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))
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))
theorem Set.pairwise_disjoint_Ico_int_cast (α : Type u_1) [OrderedRing α] :
Pairwise (Disjoint on fun n => Set.Ico (n) (n + 1))
theorem Set.pairwise_disjoint_Ioo_int_cast (α : Type u_1) [OrderedRing α] :
Pairwise (Disjoint on fun n => Set.Ioo (n) (n + 1))
theorem Set.pairwise_disjoint_Ioc_int_cast (α : Type u_1) [OrderedRing α] :
Pairwise (Disjoint on fun n => Set.Ioc (n) (n + 1))