# Intervals in `pi`-space #

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.

source
@[simp]
theorem Set.pi_univ_Ici {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] (x : (i : ι) → α i) :
(univ.pi fun (i : ι) => Ici (x i)) = Ici x
source
@[simp]
theorem Set.pi_univ_Iic {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] (x : (i : ι) → α i) :
(univ.pi fun (i : ι) => Iic (x i)) = Iic x
source
@[simp]
theorem Set.pi_univ_Icc {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] (x y : (i : ι) → α i) :
(univ.pi fun (i : ι) => Icc (x i) (y i)) = Icc x y
source
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 ∈ s, f₁ i ∈ Icc (g₁ i) (g₂ i)) (h₂ : ∀ i ∉ s, f₂ i ∈ Icc (g₁ i) (g₂ i)) :
s.piecewise f₁ f₂ ∈ Icc g₁ g₂
source
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₁ ∈ Icc g₁ g₂) (h₂ : f₂ ∈ Icc g₁ g₂) :
s.piecewise f₁ f₂ ∈ Icc g₁ g₂
source
theorem Set.pi_univ_Ioi_subset {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] (x : (i : ι) → α i) [Nonempty ι] :
(univ.pi fun (i : ι) => Ioi (x i)) ⊆ Ioi x
source
theorem Set.pi_univ_Iio_subset {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] (x : (i : ι) → α i) [Nonempty ι] :
(univ.pi fun (i : ι) => Iio (x i)) ⊆ Iio x
source
theorem Set.pi_univ_Ioo_subset {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] (x y : (i : ι) → α i) [Nonempty ι] :
(univ.pi fun (i : ι) => Ioo (x i) (y i)) ⊆ Ioo x y
source
theorem Set.pi_univ_Ioc_subset {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] (x y : (i : ι) → α i) [Nonempty ι] :
(univ.pi fun (i : ι) => Ioc (x i) (y i)) ⊆ Ioc x y
source
theorem Set.pi_univ_Ico_subset {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] (x y : (i : ι) → α i) [Nonempty ι] :
(univ.pi fun (i : ι) => Ico (x i) (y i)) ⊆ Ico x y
source
theorem Set.pi_univ_Ioc_update_left {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] [DecidableEq ι] {x y : (i : ι) → α i} {i₀ : ι} {m : α i₀} (hm : x i₀ ≤ m) :
(univ.pi fun (i : ι) => Ioc (Function.update x i₀ m i) (y i)) = {z : (i : ι) → α i | m < z i₀} ∩ univ.pi fun (i : ι) => Ioc (x i) (y i)
source
theorem Set.pi_univ_Ioc_update_right {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] [DecidableEq ι] {x y : (i : ι) → α i} {i₀ : ι} {m : α i₀} (hm : m ≤ y i₀) :
(univ.pi fun (i : ι) => Ioc (x i) (Function.update y i₀ m i)) = {z : (i : ι) → α i | z i₀ ≤ m} ∩ univ.pi fun (i : ι) => Ioc (x i) (y i)
source
theorem Set.disjoint_pi_univ_Ioc_update_left_right {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] [DecidableEq ι] {x y : (i : ι) → α i} {i₀ : ι} {m : α i₀} :
Disjoint (univ.pi fun (i : ι) => Ioc (x i) (Function.update y i₀ m i)) (univ.pi fun (i : ι) => Ioc (Function.update x i₀ m i) (y i))
source
theorem Set.image_update_Icc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] (f : (i : ι) → α i) (i : ι) (a b : α i) :
Function.update f i '' Icc a b = Icc (Function.update f i a) (Function.update f i b)
source
theorem Set.image_update_Ico {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] (f : (i : ι) → α i) (i : ι) (a b : α i) :
Function.update f i '' Ico a b = Ico (Function.update f i a) (Function.update f i b)
source
theorem Set.image_update_Ioc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] (f : (i : ι) → α i) (i : ι) (a b : α i) :
Function.update f i '' Ioc a b = Ioc (Function.update f i a) (Function.update f i b)
source
theorem Set.image_update_Ioo {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] (f : (i : ι) → α i) (i : ι) (a b : α i) :
Function.update f i '' Ioo a b = Ioo (Function.update f i a) (Function.update f i b)
source
theorem Set.image_update_Icc_left {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] (f : (i : ι) → α i) (i : ι) (a : α i) :
Function.update f i '' Icc a (f i) = Icc (Function.update f i a) f
source
theorem Set.image_update_Ico_left {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] (f : (i : ι) → α i) (i : ι) (a : α i) :
Function.update f i '' Ico a (f i) = Ico (Function.update f i a) f
source
theorem Set.image_update_Ioc_left {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] (f : (i : ι) → α i) (i : ι) (a : α i) :
Function.update f i '' Ioc a (f i) = Ioc (Function.update f i a) f
source
theorem Set.image_update_Ioo_left {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] (f : (i : ι) → α i) (i : ι) (a : α i) :
Function.update f i '' Ioo a (f i) = Ioo (Function.update f i a) f
source
theorem Set.image_update_Icc_right {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] (f : (i : ι) → α i) (i : ι) (b : α i) :
Function.update f i '' Icc (f i) b = Icc f (Function.update f i b)
source
theorem Set.image_update_Ico_right {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] (f : (i : ι) → α i) (i : ι) (b : α i) :
Function.update f i '' Ico (f i) b = Ico f (Function.update f i b)
source
theorem Set.image_update_Ioc_right {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] (f : (i : ι) → α i) (i : ι) (b : α i) :
Function.update f i '' Ioc (f i) b = Ioc f (Function.update f i b)
source
theorem Set.image_update_Ioo_right {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] (f : (i : ι) → α i) (i : ι) (b : α i) :
Function.update f i '' Ioo (f i) b = Ioo f (Function.update f i b)
source
theorem Set.image_mulSingle_Icc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → One (α i)] (i : ι) (a b : α i) :
Pi.mulSingle i '' Icc a b = Icc (Pi.mulSingle i a) (Pi.mulSingle i b)
source
theorem Set.image_single_Icc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] (i : ι) (a b : α i) :
Pi.single i '' Icc a b = Icc (Pi.single i a) (Pi.single i b)
source
theorem Set.image_mulSingle_Ico {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → One (α i)] (i : ι) (a b : α i) :
Pi.mulSingle i '' Ico a b = Ico (Pi.mulSingle i a) (Pi.mulSingle i b)
source
theorem Set.image_single_Ico {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] (i : ι) (a b : α i) :
Pi.single i '' Ico a b = Ico (Pi.single i a) (Pi.single i b)
source
theorem Set.image_mulSingle_Ioc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → One (α i)] (i : ι) (a b : α i) :
Pi.mulSingle i '' Ioc a b = Ioc (Pi.mulSingle i a) (Pi.mulSingle i b)
source
theorem Set.image_single_Ioc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] (i : ι) (a b : α i) :
Pi.single i '' Ioc a b = Ioc (Pi.single i a) (Pi.single i b)
source
theorem Set.image_mulSingle_Ioo {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → One (α i)] (i : ι) (a b : α i) :
Pi.mulSingle i '' Ioo a b = Ioo (Pi.mulSingle i a) (Pi.mulSingle i b)
source
theorem Set.image_single_Ioo {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] (i : ι) (a b : α i) :
Pi.single i '' Ioo a b = Ioo (Pi.single i a) (Pi.single i b)
source
theorem Set.image_mulSingle_Icc_left {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → One (α i)] (i : ι) (a : α i) :
Pi.mulSingle i '' Icc a 1 = Icc (Pi.mulSingle i a) 1
source
theorem Set.image_single_Icc_left {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] (i : ι) (a : α i) :
Pi.single i '' Icc a 0 = Icc (Pi.single i a) 0
source
theorem Set.image_mulSingle_Ico_left {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → One (α i)] (i : ι) (a : α i) :
Pi.mulSingle i '' Ico a 1 = Ico (Pi.mulSingle i a) 1
source
theorem Set.image_single_Ico_left {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] (i : ι) (a : α i) :
Pi.single i '' Ico a 0 = Ico (Pi.single i a) 0
source
theorem Set.image_mulSingle_Ioc_left {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → One (α i)] (i : ι) (a : α i) :
Pi.mulSingle i '' Ioc a 1 = Ioc (Pi.mulSingle i a) 1
source
theorem Set.image_single_Ioc_left {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] (i : ι) (a : α i) :
Pi.single i '' Ioc a 0 = Ioc (Pi.single i a) 0
source
theorem Set.image_mulSingle_Ioo_left {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → One (α i)] (i : ι) (a : α i) :
Pi.mulSingle i '' Ioo a 1 = Ioo (Pi.mulSingle i a) 1
source
theorem Set.image_single_Ioo_left {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] (i : ι) (a : α i) :
Pi.single i '' Ioo a 0 = Ioo (Pi.single i a) 0
source
theorem Set.image_mulSingle_Icc_right {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → One (α i)] (i : ι) (b : α i) :
Pi.mulSingle i '' Icc 1 b = Icc 1 (Pi.mulSingle i b)
source
theorem Set.image_single_Icc_right {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] (i : ι) (b : α i) :
Pi.single i '' Icc 0 b = Icc 0 (Pi.single i b)
source
theorem Set.image_mulSingle_Ico_right {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → One (α i)] (i : ι) (b : α i) :
Pi.mulSingle i '' Ico 1 b = Ico 1 (Pi.mulSingle i b)
source
theorem Set.image_single_Ico_right {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] (i : ι) (b : α i) :
Pi.single i '' Ico 0 b = Ico 0 (Pi.single i b)
source
theorem Set.image_mulSingle_Ioc_right {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → One (α i)] (i : ι) (b : α i) :
Pi.mulSingle i '' Ioc 1 b = Ioc 1 (Pi.mulSingle i b)
source
theorem Set.image_single_Ioc_right {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] (i : ι) (b : α i) :
Pi.single i '' Ioc 0 b = Ioc 0 (Pi.single i b)
source
theorem Set.image_mulSingle_Ioo_right {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → One (α i)] (i : ι) (b : α i) :
Pi.mulSingle i '' Ioo 1 b = Ioo 1 (Pi.mulSingle i b)
source
theorem Set.image_single_Ioo_right {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] (i : ι) (b : α i) :
Pi.single i '' Ioo 0 b = Ioo 0 (Pi.single i b)
source
@[simp]
theorem Set.pi_univ_uIcc {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] (a b : (i : ι) → α i) :
(univ.pi fun (i : ι) => uIcc (a i) (b i)) = uIcc a b
source
theorem Set.image_update_uIcc {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] (f : (i : ι) → α i) (i : ι) (a b : α i) :
Function.update f i '' uIcc a b = uIcc (Function.update f i a) (Function.update f i b)
source
theorem Set.image_update_uIcc_left {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] (f : (i : ι) → α i) (i : ι) (a : α i) :
Function.update f i '' uIcc a (f i) = uIcc (Function.update f i a) f
source
theorem Set.image_update_uIcc_right {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] (f : (i : ι) → α i) (i : ι) (b : α i) :
Function.update f i '' uIcc (f i) b = uIcc f (Function.update f i b)
source
theorem Set.image_mulSingle_uIcc {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] [(i : ι) → One (α i)] (i : ι) (a b : α i) :
Pi.mulSingle i '' uIcc a b = uIcc (Pi.mulSingle i a) (Pi.mulSingle i b)
source
theorem Set.image_single_uIcc {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] [(i : ι) → Zero (α i)] (i : ι) (a b : α i) :
Pi.single i '' uIcc a b = uIcc (Pi.single i a) (Pi.single i b)
source
theorem Set.image_mulSingle_uIcc_left {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] [(i : ι) → One (α i)] (i : ι) (a : α i) :
Pi.mulSingle i '' uIcc a 1 = uIcc (Pi.mulSingle i a) 1
source
theorem Set.image_single_uIcc_left {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] [(i : ι) → Zero (α i)] (i : ι) (a : α i) :
Pi.single i '' uIcc a 0 = uIcc (Pi.single i a) 0
source
theorem Set.image_mulSingle_uIcc_right {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] [(i : ι) → One (α i)] (i : ι) (b : α i) :
Pi.mulSingle i '' uIcc 1 b = uIcc 1 (Pi.mulSingle i b)
source
theorem Set.image_single_uIcc_right {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] [(i : ι) → Zero (α i)] (i : ι) (b : α i) :
Pi.single i '' uIcc 0 b = uIcc 0 (Pi.single i b)
source
theorem Set.pi_univ_Ioc_update_union {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → LinearOrder (α i)] (x y : (i : ι) → α i) (i₀ : ι) (m : α i₀) (hm : m ∈ Icc (x i₀) (y i₀)) :
((univ.pi fun (i : ι) => Ioc (x i) (Function.update y i₀ m i)) ∪ univ.pi fun (i : ι) => Ioc (Function.update x i₀ m i) (y i)) = univ.pi fun (i : ι) => Ioc (x i) (y i)
source
theorem Set.Icc_diff_pi_univ_Ioo_subset {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → LinearOrder (α i)] (x y x' y' : (i : ι) → α i) :
(Icc x y \ univ.pi fun (i : ι) => Ioo (x' i) (y' i)) ⊆ (⋃ (i : ι), Icc x (Function.update y i (x' i))) ∪ ⋃ (i : ι), Icc (Function.update x 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]`.

source
theorem Set.Icc_diff_pi_univ_Ioc_subset {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → LinearOrder (α i)] (x y z : (i : ι) → α i) :
(Icc x z \ univ.pi fun (i : ι) => Ioc (y i) (z i)) ⊆ ⋃ (i : ι), Icc x (Function.update z 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`.