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.
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₁ : ∀ i ∈ s, f₁ i ∈ Set.Icc (g₁ i) (g₂ i))
(h₂ : ∀ i ∉ s, 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_Ioc_update_left
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Preorder (α i)]
[DecidableEq ι]
{x : (i : ι) → α i}
{y : (i : ι) → α i}
{i₀ : ι}
{m : α i₀}
(hm : x i₀ ≤ m)
:
theorem
Set.pi_univ_Ioc_update_right
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Preorder (α i)]
[DecidableEq ι]
{x : (i : ι) → α i}
{y : (i : ι) → α i}
{i₀ : ι}
{m : α i₀}
(hm : m ≤ y i₀)
:
theorem
Set.disjoint_pi_univ_Ioc_update_left_right
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Preorder (α i)]
[DecidableEq ι]
{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}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
(f : (i : ι) → α i)
(i : ι)
(a : α i)
(b : α i)
:
Function.update f i '' Set.Icc a b = Set.Icc (Function.update f i a) (Function.update f i b)
theorem
Set.image_update_Ico
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
(f : (i : ι) → α i)
(i : ι)
(a : α i)
(b : α i)
:
Function.update f i '' Set.Ico a b = Set.Ico (Function.update f i a) (Function.update f i b)
theorem
Set.image_update_Ioc
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
(f : (i : ι) → α i)
(i : ι)
(a : α i)
(b : α i)
:
Function.update f i '' Set.Ioc a b = Set.Ioc (Function.update f i a) (Function.update f i b)
theorem
Set.image_update_Ioo
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
(f : (i : ι) → α i)
(i : ι)
(a : α i)
(b : α i)
:
Function.update f i '' Set.Ioo a b = Set.Ioo (Function.update f i a) (Function.update f i b)
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 '' Set.Icc a (f i) = Set.Icc (Function.update f i a) f
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 '' Set.Ico a (f i) = Set.Ico (Function.update f i a) f
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 '' Set.Ioc a (f i) = Set.Ioc (Function.update f i a) f
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 '' Set.Ioo a (f i) = Set.Ioo (Function.update f i a) f
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 '' Set.Icc (f i) b = Set.Icc f (Function.update f i b)
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 '' Set.Ico (f i) b = Set.Ico f (Function.update f i b)
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 '' Set.Ioc (f i) b = Set.Ioc f (Function.update f i b)
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 '' Set.Ioo (f i) b = Set.Ioo f (Function.update f i b)
theorem
Set.image_single_Icc
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → Zero (α i)]
(i : ι)
(a : α i)
(b : α i)
:
theorem
Set.image_mulSingle_Icc
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → One (α i)]
(i : ι)
(a : α i)
(b : α i)
:
Pi.mulSingle i '' Set.Icc a b = Set.Icc (Pi.mulSingle i a) (Pi.mulSingle i b)
theorem
Set.image_single_Ico
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → Zero (α i)]
(i : ι)
(a : α i)
(b : α i)
:
theorem
Set.image_mulSingle_Ico
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → One (α i)]
(i : ι)
(a : α i)
(b : α i)
:
Pi.mulSingle i '' Set.Ico a b = Set.Ico (Pi.mulSingle i a) (Pi.mulSingle i b)
theorem
Set.image_single_Ioc
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → Zero (α i)]
(i : ι)
(a : α i)
(b : α i)
:
theorem
Set.image_mulSingle_Ioc
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → One (α i)]
(i : ι)
(a : α i)
(b : α i)
:
Pi.mulSingle i '' Set.Ioc a b = Set.Ioc (Pi.mulSingle i a) (Pi.mulSingle i b)
theorem
Set.image_single_Ioo
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → Zero (α i)]
(i : ι)
(a : α i)
(b : α i)
:
theorem
Set.image_mulSingle_Ioo
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → One (α i)]
(i : ι)
(a : α i)
(b : α i)
:
Pi.mulSingle i '' Set.Ioo a b = Set.Ioo (Pi.mulSingle i a) (Pi.mulSingle i b)
theorem
Set.image_single_Icc_left
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → Zero (α i)]
(i : ι)
(a : α i)
:
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 '' Set.Icc a 1 = Set.Icc (Pi.mulSingle i a) 1
theorem
Set.image_single_Ico_left
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → Zero (α i)]
(i : ι)
(a : α i)
:
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 '' Set.Ico a 1 = Set.Ico (Pi.mulSingle i a) 1
theorem
Set.image_single_Ioc_left
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → Zero (α i)]
(i : ι)
(a : α i)
:
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 '' Set.Ioc a 1 = Set.Ioc (Pi.mulSingle i a) 1
theorem
Set.image_single_Ioo_left
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → Zero (α i)]
(i : ι)
(a : α i)
:
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 '' Set.Ioo a 1 = Set.Ioo (Pi.mulSingle i a) 1
theorem
Set.image_single_Icc_right
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → Zero (α i)]
(i : ι)
(b : α i)
:
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 '' Set.Icc 1 b = Set.Icc 1 (Pi.mulSingle i b)
theorem
Set.image_single_Ico_right
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → Zero (α i)]
(i : ι)
(b : α i)
:
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 '' Set.Ico 1 b = Set.Ico 1 (Pi.mulSingle i b)
theorem
Set.image_single_Ioc_right
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → Zero (α i)]
(i : ι)
(b : α i)
:
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 '' Set.Ioc 1 b = Set.Ioc 1 (Pi.mulSingle i b)
theorem
Set.image_single_Ioo_right
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(i : ι) → PartialOrder (α i)]
[(i : ι) → Zero (α i)]
(i : ι)
(b : α i)
:
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 '' Set.Ioo 1 b = Set.Ioo 1 (Pi.mulSingle i b)
theorem
Set.image_update_uIcc
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Lattice (α i)]
[DecidableEq ι]
(f : (i : ι) → α i)
(i : ι)
(a : α i)
(b : α i)
:
Function.update f i '' Set.uIcc a b = Set.uIcc (Function.update f i a) (Function.update f i b)
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 '' Set.uIcc a (f i) = Set.uIcc (Function.update f i a) f
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 '' Set.uIcc (f i) b = Set.uIcc f (Function.update f i b)
theorem
Set.image_mulSingle_uIcc
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Lattice (α i)]
[DecidableEq ι]
[(i : ι) → One (α i)]
(i : ι)
(a : α i)
(b : α i)
:
Pi.mulSingle i '' Set.uIcc a b = Set.uIcc (Pi.mulSingle i a) (Pi.mulSingle i b)
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 '' Set.uIcc a 1 = Set.uIcc (Pi.mulSingle i a) 1
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 '' Set.uIcc 1 b = Set.uIcc 1 (Pi.mulSingle i b)
theorem
Set.pi_univ_Ioc_update_union
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ι]
[(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}
[DecidableEq ι]
[(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}
[DecidableEq ι]
[(i : ι) → LinearOrder (α i)]
(x : (i : ι) → α i)
(y : (i : ι) → α i)
(z : (i : ι) → α 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.