mathlib documentation

data.set.intervals.group

Lemmas about arithmetic operations and intervals. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

inv_mem_Ixx_iff, sub_mem_Ixx_iff

theorem set.neg_mem_Icc_iff {α : Type u_1} [ordered_add_comm_group α] {a c d : α} :
-a set.Icc c d a set.Icc (-d) (-c)
theorem set.inv_mem_Icc_iff {α : Type u_1} [ordered_comm_group α] {a c d : α} :
theorem set.neg_mem_Ico_iff {α : Type u_1} [ordered_add_comm_group α] {a c d : α} :
-a set.Ico c d a set.Ioc (-d) (-c)
theorem set.inv_mem_Ico_iff {α : Type u_1} [ordered_comm_group α] {a c d : α} :
theorem set.inv_mem_Ioc_iff {α : Type u_1} [ordered_comm_group α] {a c d : α} :
theorem set.neg_mem_Ioc_iff {α : Type u_1} [ordered_add_comm_group α] {a c d : α} :
-a set.Ioc c d a set.Ico (-d) (-c)
theorem set.inv_mem_Ioo_iff {α : Type u_1} [ordered_comm_group α] {a c d : α} :
theorem set.neg_mem_Ioo_iff {α : Type u_1} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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_1} [linear_ordered_add_comm_group R] {x y z : R} :
|x - y| z y set.Icc (x - z) (x + z)
theorem set.nonempty_Ico_sdiff {α : Type u_1} [linear_ordered_add_comm_group α] {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} [ordered_comm_group α] (a b : α) :
pairwise (disjoint on λ (n : ), set.Ioc (a * b ^ n) (a * b ^ (n + 1)))
theorem set.pairwise_disjoint_Ioc_add_zsmul {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
pairwise (disjoint on λ (n : ), set.Ioc (a + n b) (a + (n + 1) b))
theorem set.pairwise_disjoint_Ico_mul_zpow {α : Type u_1} [ordered_comm_group α] (a b : α) :
pairwise (disjoint on λ (n : ), set.Ico (a * b ^ n) (a * b ^ (n + 1)))
theorem set.pairwise_disjoint_Ico_add_zsmul {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
pairwise (disjoint on λ (n : ), set.Ico (a + n b) (a + (n + 1) b))
theorem set.pairwise_disjoint_Ioo_add_zsmul {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
pairwise (disjoint on λ (n : ), set.Ioo (a + n b) (a + (n + 1) b))
theorem set.pairwise_disjoint_Ioo_mul_zpow {α : Type u_1} [ordered_comm_group α] (a b : α) :
pairwise (disjoint on λ (n : ), set.Ioo (a * b ^ n) (a * b ^ (n + 1)))
theorem set.pairwise_disjoint_Ioc_zpow {α : Type u_1} [ordered_comm_group α] (b : α) :
pairwise (disjoint on λ (n : ), set.Ioc (b ^ n) (b ^ (n + 1)))
theorem set.pairwise_disjoint_Ioc_zsmul {α : Type u_1} [ordered_add_comm_group α] (b : α) :
pairwise (disjoint on λ (n : ), set.Ioc (n b) ((n + 1) b))
theorem set.pairwise_disjoint_Ico_zsmul {α : Type u_1} [ordered_add_comm_group α] (b : α) :
pairwise (disjoint on λ (n : ), set.Ico (n b) ((n + 1) b))
theorem set.pairwise_disjoint_Ico_zpow {α : Type u_1} [ordered_comm_group α] (b : α) :
pairwise (disjoint on λ (n : ), set.Ico (b ^ n) (b ^ (n + 1)))
theorem set.pairwise_disjoint_Ioo_zpow {α : Type u_1} [ordered_comm_group α] (b : α) :
pairwise (disjoint on λ (n : ), set.Ioo (b ^ n) (b ^ (n + 1)))
theorem set.pairwise_disjoint_Ioo_zsmul {α : Type u_1} [ordered_add_comm_group α] (b : α) :
pairwise (disjoint on λ (n : ), set.Ioo (n b) ((n + 1) b))
theorem set.pairwise_disjoint_Ioc_add_int_cast {α : Type u_1} [ordered_ring α] (a : α) :
pairwise (disjoint on λ (n : ), set.Ioc (a + n) (a + n + 1))
theorem set.pairwise_disjoint_Ico_add_int_cast {α : Type u_1} [ordered_ring α] (a : α) :
pairwise (disjoint on λ (n : ), set.Ico (a + n) (a + n + 1))
theorem set.pairwise_disjoint_Ioo_add_int_cast {α : Type u_1} [ordered_ring α] (a : α) :
pairwise (disjoint on λ (n : ), set.Ioo (a + n) (a + n + 1))