# mathlib3documentation

data.set.intervals.pi

# Intervals in pi-space #

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

In this we prove various simple lemmas about intervals in Π i, α i. Closed intervals (Ici x, Iic x, Icc x y) are equal to products of their projections to α i, while (semi-)open intervals usually include the corresponding products as proper subsets.

@[simp]
theorem set.pi_univ_Ici {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] (x : Π (i : ι), α i) :
set.univ.pi (λ (i : ι), set.Ici (x i)) =
@[simp]
theorem set.pi_univ_Iic {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] (x : Π (i : ι), α i) :
set.univ.pi (λ (i : ι), set.Iic (x i)) =
@[simp]
theorem set.pi_univ_Icc {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] (x y : Π (i : ι), α i) :
set.univ.pi (λ (i : ι), set.Icc (x i) (y i)) = y
theorem set.piecewise_mem_Icc {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] {s : set ι} [Π (j : ι), decidable (j s)] {f₁ f₂ g₁ g₂ : Π (i : ι), α i} (h₁ : (i : ι), i s f₁ i set.Icc (g₁ i) (g₂ i)) (h₂ : (i : ι), i s f₂ i set.Icc (g₁ i) (g₂ i)) :
s.piecewise f₁ f₂ set.Icc g₁ g₂
theorem set.piecewise_mem_Icc' {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] {s : set ι} [Π (j : ι), decidable (j s)] {f₁ f₂ g₁ g₂ : Π (i : ι), α i} (h₁ : f₁ set.Icc g₁ g₂) (h₂ : f₂ set.Icc g₁ g₂) :
s.piecewise f₁ f₂ set.Icc g₁ g₂
theorem set.pi_univ_Ioi_subset {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] (x : Π (i : ι), α i) [nonempty ι] :
set.univ.pi (λ (i : ι), set.Ioi (x i))
theorem set.pi_univ_Iio_subset {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] (x : Π (i : ι), α i) [nonempty ι] :
set.univ.pi (λ (i : ι), set.Iio (x i))
theorem set.pi_univ_Ioo_subset {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] (x y : Π (i : ι), α i) [nonempty ι] :
set.univ.pi (λ (i : ι), set.Ioo (x i) (y i)) y
theorem set.pi_univ_Ioc_subset {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] (x y : Π (i : ι), α i) [nonempty ι] :
set.univ.pi (λ (i : ι), set.Ioc (x i) (y i)) y
theorem set.pi_univ_Ico_subset {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] (x y : Π (i : ι), α i) [nonempty ι] :
set.univ.pi (λ (i : ι), set.Ico (x i) (y i)) y
theorem set.pi_univ_Ioc_update_left {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] [decidable_eq ι] {x y : Π (i : ι), α i} {i₀ : ι} {m : α i₀} (hm : x i₀ m) :
set.univ.pi (λ (i : ι), set.Ioc i₀ m i) (y i)) = {z : Π (i : ι), α i | m < z i₀} set.univ.pi (λ (i : ι), set.Ioc (x i) (y i))
theorem set.pi_univ_Ioc_update_right {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] [decidable_eq ι] {x y : Π (i : ι), α i} {i₀ : ι} {m : α i₀} (hm : m y i₀) :
set.univ.pi (λ (i : ι), set.Ioc (x i) i₀ m i)) = {z : Π (i : ι), α i | z i₀ m} set.univ.pi (λ (i : ι), set.Ioc (x i) (y i))
theorem set.disjoint_pi_univ_Ioc_update_left_right {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] [decidable_eq ι] {x y : Π (i : ι), α i} {i₀ : ι} {m : α i₀} :
disjoint (set.univ.pi (λ (i : ι), set.Ioc (x i) i₀ m i))) (set.univ.pi (λ (i : ι), set.Ioc i₀ m i) (y i)))
theorem set.image_update_Icc {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] (f : Π (i : ι), α i) (i : ι) (a b : α i) :
'' b = set.Icc i a) i b)
theorem set.image_update_Ico {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] (f : Π (i : ι), α i) (i : ι) (a b : α i) :
'' b = set.Ico i a) i b)
theorem set.image_update_Ioc {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] (f : Π (i : ι), α i) (i : ι) (a b : α i) :
'' b = set.Ioc i a) i b)
theorem set.image_update_Ioo {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] (f : Π (i : ι), α i) (i : ι) (a b : α i) :
'' b = set.Ioo i a) i b)
theorem set.image_update_Icc_left {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] (f : Π (i : ι), α i) (i : ι) (a : α i) :
'' (f i) = set.Icc i a) f
theorem set.image_update_Ico_left {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] (f : Π (i : ι), α i) (i : ι) (a : α i) :
'' (f i) = set.Ico i a) f
theorem set.image_update_Ioc_left {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] (f : Π (i : ι), α i) (i : ι) (a : α i) :
'' (f i) = set.Ioc i a) f
theorem set.image_update_Ioo_left {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] (f : Π (i : ι), α i) (i : ι) (a : α i) :
'' (f i) = set.Ioo i a) f
theorem set.image_update_Icc_right {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] (f : Π (i : ι), α i) (i : ι) (b : α i) :
'' set.Icc (f i) b = i b)
theorem set.image_update_Ico_right {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] (f : Π (i : ι), α i) (i : ι) (b : α i) :
'' set.Ico (f i) b = i b)
theorem set.image_update_Ioc_right {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] (f : Π (i : ι), α i) (i : ι) (b : α i) :
'' set.Ioc (f i) b = i b)
theorem set.image_update_Ioo_right {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] (f : Π (i : ι), α i) (i : ι) (b : α i) :
'' set.Ioo (f i) b = i b)
theorem set.image_mul_single_Icc {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_one (α i)] (i : ι) (a b : α i) :
'' b = set.Icc a) b)
theorem set.image_single_Icc {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] (i : ι) (a b : α i) :
'' b = set.Icc a) b)
theorem set.image_single_Ico {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] (i : ι) (a b : α i) :
'' b = set.Ico a) b)
theorem set.image_mul_single_Ico {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_one (α i)] (i : ι) (a b : α i) :
'' b = set.Ico a) b)
theorem set.image_single_Ioc {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] (i : ι) (a b : α i) :
'' b = set.Ioc a) b)
theorem set.image_mul_single_Ioc {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_one (α i)] (i : ι) (a b : α i) :
'' b = set.Ioc a) b)
theorem set.image_mul_single_Ioo {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_one (α i)] (i : ι) (a b : α i) :
'' b = set.Ioo a) b)
theorem set.image_single_Ioo {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] (i : ι) (a b : α i) :
'' b = set.Ioo a) b)
theorem set.image_single_Icc_left {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] (i : ι) (a : α i) :
'' 0 = set.Icc a) 0
theorem set.image_mul_single_Icc_left {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_one (α i)] (i : ι) (a : α i) :
'' 1 = set.Icc a) 1
theorem set.image_single_Ico_left {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] (i : ι) (a : α i) :
'' 0 = set.Ico a) 0
theorem set.image_mul_single_Ico_left {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_one (α i)] (i : ι) (a : α i) :
'' 1 = set.Ico a) 1
theorem set.image_mul_single_Ioc_left {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_one (α i)] (i : ι) (a : α i) :
'' 1 = set.Ioc a) 1
theorem set.image_single_Ioc_left {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] (i : ι) (a : α i) :
'' 0 = set.Ioc a) 0
theorem set.image_single_Ioo_left {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] (i : ι) (a : α i) :
'' 0 = set.Ioo a) 0
theorem set.image_mul_single_Ioo_left {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_one (α i)] (i : ι) (a : α i) :
'' 1 = set.Ioo a) 1
theorem set.image_single_Icc_right {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] (i : ι) (b : α i) :
'' b = b)
theorem set.image_mul_single_Icc_right {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_one (α i)] (i : ι) (b : α i) :
'' b = b)
theorem set.image_single_Ico_right {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] (i : ι) (b : α i) :
'' b = b)
theorem set.image_mul_single_Ico_right {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_one (α i)] (i : ι) (b : α i) :
'' b = b)
theorem set.image_mul_single_Ioc_right {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_one (α i)] (i : ι) (b : α i) :
'' b = b)
theorem set.image_single_Ioc_right {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] (i : ι) (b : α i) :
'' b = b)
theorem set.image_mul_single_Ioo_right {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_one (α i)] (i : ι) (b : α i) :
'' b = b)
theorem set.image_single_Ioo_right {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] (i : ι) (b : α i) :
'' b = b)
@[simp]
theorem set.pi_univ_uIcc {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), lattice (α i)] (a b : Π (i : ι), α i) :
set.univ.pi (λ (i : ι), set.uIcc (a i) (b i)) = b
theorem set.image_update_uIcc {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), lattice (α i)] [decidable_eq ι] (f : Π (i : ι), α i) (i : ι) (a b : α i) :
'' b = set.uIcc i a) i b)
theorem set.image_update_uIcc_left {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), lattice (α i)] [decidable_eq ι] (f : Π (i : ι), α i) (i : ι) (a : α i) :
'' (f i) = set.uIcc i a) f
theorem set.image_update_uIcc_right {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), lattice (α i)] [decidable_eq ι] (f : Π (i : ι), α i) (i : ι) (b : α i) :
'' set.uIcc (f i) b = i b)
theorem set.image_single_uIcc {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), lattice (α i)] [decidable_eq ι] [Π (i : ι), has_zero (α i)] (i : ι) (a b : α i) :
'' b = set.uIcc a) b)
theorem set.image_mul_single_uIcc {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), lattice (α i)] [decidable_eq ι] [Π (i : ι), has_one (α i)] (i : ι) (a b : α i) :
'' b = set.uIcc a) b)
theorem set.image_single_uIcc_left {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), lattice (α i)] [decidable_eq ι] [Π (i : ι), has_zero (α i)] (i : ι) (a : α i) :
'' 0 = set.uIcc a) 0
theorem set.image_mul_single_uIcc_left {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), lattice (α i)] [decidable_eq ι] [Π (i : ι), has_one (α i)] (i : ι) (a : α i) :
'' 1 = set.uIcc a) 1
theorem set.image_single_uIcc_right {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), lattice (α i)] [decidable_eq ι] [Π (i : ι), has_zero (α i)] (i : ι) (b : α i) :
'' b = b)
theorem set.image_mul_single_uIcc_right {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), lattice (α i)] [decidable_eq ι] [Π (i : ι), has_one (α i)] (i : ι) (b : α i) :
'' b = b)
theorem set.pi_univ_Ioc_update_union {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), linear_order (α i)] (x y : Π (i : ι), α i) (i₀ : ι) (m : α i₀) (hm : m set.Icc (x i₀) (y i₀)) :
set.univ.pi (λ (i : ι), set.Ioc (x i) i₀ m i)) set.univ.pi (λ (i : ι), set.Ioc i₀ m i) (y i)) = set.univ.pi (λ (i : ι), set.Ioc (x i) (y i))
theorem set.Icc_diff_pi_univ_Ioo_subset {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), linear_order (α i)] (x y x' y' : Π (i : ι), α i) :
y \ set.univ.pi (λ (i : ι), set.Ioo (x' i) (y' i)) ( (i : ι), i (x' i))) (i : ι), set.Icc i (y' i)) y

If x, y, x', and y' are functions Π i : ι, α i, then the set difference between the box [x, y] and the product of the open intervals (x' i, y' i) is covered by the union of the following boxes: for each i : ι, we take [x, update y i (x' i)] and [update x i (y' i), y].

E.g., if x' = x and y' = y, then this lemma states that the difference between a closed box [x, y] and the corresponding open box {z | ∀ i, x i < z i < y i} is covered by the union of the faces of [x, y].

theorem set.Icc_diff_pi_univ_Ioc_subset {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), linear_order (α i)] (x y z : Π (i : ι), α i) :
z \ set.univ.pi (λ (i : ι), set.Ioc (y i) (z i)) (i : ι), i (y i))

If x, y, z are functions Π i : ι, α i, then the set difference between the box [x, z] and the product of the intervals (y i, z i] is covered by the union of the boxes [x, update z i (y i)].

E.g., if x = y, then this lemma states that the difference between a closed box [x, y] and the product of half-open intervals {z | ∀ i, x i < z i ≤ y i} is covered by the union of the faces of [x, y] adjacent to x.