# Documentation

Mathlib.Data.Set.Intervals.Pi

# 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.

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

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