data.set.intervals.group

source

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)

source

theorem set.inv_mem_Icc_iff {α : Type u_1} [ordered_comm_group α] {a c d : α} :

a⁻¹ ∈ set.Icc c d ↔ a ∈ set.Icc d⁻¹ c⁻¹

source

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)

source

theorem set.inv_mem_Ico_iff {α : Type u_1} [ordered_comm_group α] {a c d : α} :

a⁻¹ ∈ set.Ico c d ↔ a ∈ set.Ioc d⁻¹ c⁻¹

source

theorem set.inv_mem_Ioc_iff {α : Type u_1} [ordered_comm_group α] {a c d : α} :

a⁻¹ ∈ set.Ioc c d ↔ a ∈ set.Ico d⁻¹ c⁻¹

source

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)

source

theorem set.inv_mem_Ioo_iff {α : Type u_1} [ordered_comm_group α] {a c d : α} :

a⁻¹ ∈ set.Ioo c d ↔ a ∈ set.Ioo d⁻¹ c⁻¹

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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

source

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)))

source

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))

source

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)))

source

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))

source

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))

source

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)))

source

theorem set.pairwise_disjoint_Ioc_zpow {α : Type u_1} [ordered_comm_group α] (b : α) :

pairwise (disjoint on λ (n : ℤ), set.Ioc (b ^ n) (b ^ (n + 1)))

source

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))

source

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))

source

theorem set.pairwise_disjoint_Ico_zpow {α : Type u_1} [ordered_comm_group α] (b : α) :

pairwise (disjoint on λ (n : ℤ), set.Ico (b ^ n) (b ^ (n + 1)))

source

theorem set.pairwise_disjoint_Ioo_zpow {α : Type u_1} [ordered_comm_group α] (b : α) :

pairwise (disjoint on λ (n : ℤ), set.Ioo (b ^ n) (b ^ (n + 1)))

source

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))

source

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))

source

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))

source

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))

source

theorem set.pairwise_disjoint_Ico_int_cast (α : Type u_1) [ordered_ring α] :

pairwise (disjoint on λ (n : ℤ), set.Ico ↑n (↑n + 1))

source

theorem set.pairwise_disjoint_Ioo_int_cast (α : Type u_1) [ordered_ring α] :

pairwise (disjoint on λ (n : ℤ), set.Ioo ↑n (↑n + 1))

source

theorem set.pairwise_disjoint_Ioc_int_cast (α : Type u_1) [ordered_ring α] :

pairwise (disjoint on λ (n : ℤ), set.Ioc ↑n (↑n + 1))

mathlib3 documentation

Lemmas about arithmetic operations and intervals. #

Lemmas about disjointness of translates of intervals #