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.
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) :
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₀) :
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) (function.update y i₀ m i))) (set.univ.pi (λ (i : ι), set.Ioc (function.update x 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) :
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}
[decidable_eq ι]
[Π (i : ι), partial_order (α i)]
(f : Π (i : ι), α i)
(i : ι)
(a 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}
[decidable_eq ι]
[Π (i : ι), partial_order (α i)]
(f : Π (i : ι), α i)
(i : ι)
(a 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}
[decidable_eq ι]
[Π (i : ι), partial_order (α i)]
(f : Π (i : ι), α i)
(i : ι)
(a 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}
[decidable_eq ι]
[Π (i : ι), partial_order (α 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}
[decidable_eq ι]
[Π (i : ι), partial_order (α 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}
[decidable_eq ι]
[Π (i : ι), partial_order (α 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}
[decidable_eq ι]
[Π (i : ι), partial_order (α 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}
[decidable_eq ι]
[Π (i : ι), partial_order (α 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}
[decidable_eq ι]
[Π (i : ι), partial_order (α 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}
[decidable_eq ι]
[Π (i : ι), partial_order (α 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}
[decidable_eq ι]
[Π (i : ι), partial_order (α 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_mul_single_Icc
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), partial_order (α i)]
[Π (i : ι), has_one (α i)]
(i : ι)
(a b : α i) :
pi.mul_single i '' set.Icc a b = set.Icc (pi.mul_single i a) (pi.mul_single i 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) :
pi.mul_single i '' set.Ico a b = set.Ico (pi.mul_single i a) (pi.mul_single i 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) :
pi.mul_single i '' set.Ioc a b = set.Ioc (pi.mul_single i a) (pi.mul_single i 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) :
pi.mul_single i '' set.Ioo a b = set.Ioo (pi.mul_single i a) (pi.mul_single i b)
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) :
pi.mul_single i '' set.Icc a 1 = set.Icc (pi.mul_single i a) 1
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) :
pi.mul_single i '' set.Ico a 1 = set.Ico (pi.mul_single i 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) :
pi.mul_single i '' set.Ioc a 1 = set.Ioc (pi.mul_single i a) 1
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) :
pi.mul_single i '' set.Ioo a 1 = set.Ioo (pi.mul_single i a) 1
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) :
pi.mul_single i '' set.Icc 1 b = set.Icc 1 (pi.mul_single i 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) :
pi.mul_single i '' set.Ico 1 b = set.Ico 1 (pi.mul_single i 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) :
pi.mul_single i '' set.Ioc 1 b = set.Ioc 1 (pi.mul_single i 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) :
pi.mul_single i '' set.Ioo 1 b = set.Ioo 1 (pi.mul_single 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) :
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)]
[decidable_eq ι]
(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)]
[decidable_eq ι]
(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_mul_single_uIcc
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), lattice (α i)]
[decidable_eq ι]
[Π (i : ι), has_one (α i)]
(i : ι)
(a b : α i) :
pi.mul_single i '' set.uIcc a b = set.uIcc (pi.mul_single i a) (pi.mul_single i b)
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) :
pi.mul_single i '' set.uIcc a 1 = set.uIcc (pi.mul_single i a) 1
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) :
pi.mul_single i '' set.uIcc 1 b = set.uIcc 1 (pi.mul_single i 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₀)) :
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) :
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) :
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.