Mathlib.Order.Interval.Set.Pi

Set.pi_univ_Ici theorem

: (pi univ fun i ↦ Ici (x i)) = Ici x

Full source

@[simp]
theorem pi_univ_Ici : (pi univ fun i ↦ Ici (x i)) = Ici x :=
  ext fun y ↦ by simp [Pi.le_def]

Product of Intervals Equals Interval in Product Space

Informal description

For a family of types $\alpha_i$ indexed by $i \in I$ and a function $x \in \Pi_{i \in I} \alpha_i$, the product of the left-closed right-infinite intervals $[x_i, \infty)$ over all $i \in I$ is equal to the left-closed right-infinite interval $[x, \infty)$ in the product space $\Pi_{i \in I} \alpha_i$. In other words, $$\prod_{i \in I} [x_i, \infty) = [x, \infty).$$

Set.pi_univ_Iic theorem

: (pi univ fun i ↦ Iic (x i)) = Iic x

Full source

@[simp]
theorem pi_univ_Iic : (pi univ fun i ↦ Iic (x i)) = Iic x :=
  ext fun y ↦ by simp [Pi.le_def]

Product of Left-Infinite Right-Closed Intervals in Product Space

Informal description

For a family of preordered types $\alpha_i$ indexed by $i \in \iota$, and an element $x \in \Pi_{i \in \iota} \alpha_i$, the product of the left-infinite right-closed intervals $(-\infty, x_i]$ over all $i \in \iota$ is equal to the left-infinite right-closed interval $(-\infty, x]$ in the product space $\Pi_{i \in \iota} \alpha_i$. In other words, \[ \prod_{i \in \iota} (-\infty, x_i] = (-\infty, x]. \]

Set.pi_univ_Icc theorem

: (pi univ fun i ↦ Icc (x i) (y i)) = Icc x y

Full source

@[simp]
theorem pi_univ_Icc : (pi univ fun i ↦ Icc (x i) (y i)) = Icc x y :=
  ext fun y ↦ by simp [Pi.le_def, forall_and]

Product of Closed Intervals Equals Closed Interval in Product Space

Informal description

For a family of types $\alpha_i$ indexed by $i \in \iota$ and elements $x, y \in \prod_{i} \alpha_i$, the product over all indices $i$ of the closed intervals $[x_i, y_i]$ is equal to the closed interval $[x, y]$ in the product space. That is, \[ \prod_{i \in \iota} [x_i, y_i] = [x, y]. \]

Set.piecewise_mem_Icc theorem

 {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₂

Full source

theorem piecewise_mem_Icc {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₂ :=
  ⟨le_piecewise (fun i hi ↦ (h₁ i hi).1) fun i hi ↦ (h₂ i hi).1,
    piecewise_le (fun i hi ↦ (h₁ i hi).2) fun i hi ↦ (h₂ i hi).2⟩

Piecewise Function Preserves Interval Membership in Product Space

Informal description

Let $ι$ be a type, $\{α_i\}_{i \in ι}$ a family of types with preorders, and $s \subseteq ι$ a decidable subset. Given functions $f_1, f_2, g_1, g_2 : \prod_{i \in ι} α_i$, if for every $i \in s$ we have $f_1(i) \in [g_1(i), g_2(i)]$ and for every $i \notin s$ we have $f_2(i) \in [g_1(i), g_2(i)]$, then the piecewise function $s.\text{piecewise}\,f_1\,f_2$ satisfies $s.\text{piecewise}\,f_1\,f_2 \in [g_1, g_2]$.

Set.piecewise_mem_Icc' theorem

 {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₂

Full source

theorem piecewise_mem_Icc' {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₂ :=
  piecewise_mem_Icc (fun _ _ ↦ ⟨h₁.1 _, h₁.2 _⟩) fun _ _ ↦ ⟨h₂.1 _, h₂.2 _⟩

Piecewise Function Preserves Closed Interval Membership in Product Space

Informal description

Let $ι$ be a type with a decidable subset $s \subseteq ι$, and let $\{α_i\}_{i \in ι}$ be a family of types with preorders. Given functions $f_1, f_2, g_1, g_2 \in \prod_{i \in ι} α_i$ such that $f_1 \in [g_1, g_2]$ and $f_2 \in [g_1, g_2]$, the piecewise function $s.\text{piecewise}\,f_1\,f_2$ satisfies $s.\text{piecewise}\,f_1\,f_2 \in [g_1, g_2]$.

Set.pi_univ_Ioi_subset theorem

[Nonempty ι] : (pi univ fun i ↦ Ioi (x i)) ⊆ Ioi x

Full source

theorem pi_univ_Ioi_subset [Nonempty ι]: (pi univ fun i ↦ Ioi (x i)) ⊆ Ioi x := fun _ hz ↦
  ⟨fun i ↦ le_of_lt <| hz i trivial, fun h ↦
    (‹Nonempty ι›.elim) fun i ↦ not_lt_of_le (h i) (hz i trivial)⟩

Product of Right-Infinite Intervals is Contained in Product Space Right-Infinite Interval

Informal description

For a nonempty index set $\iota$ and a family of preorders $\{\alpha_i\}_{i \in \iota}$, the product of left-open right-infinite intervals $\prod_{i \in \iota} (x_i, \infty)$ is contained in the left-open right-infinite interval $(x, \infty)$ of the product space $\prod_{i \in \iota} \alpha_i$, where $x = (x_i)_{i \in \iota}$.

Set.pi_univ_Iio_subset theorem

[Nonempty ι] : (pi univ fun i ↦ Iio (x i)) ⊆ Iio x

Full source

theorem pi_univ_Iio_subset [Nonempty ι]: (pi univ fun i ↦ Iio (x i)) ⊆ Iio x :=
  pi_univ_Ioi_subset (α := fun i ↦ (α i)ᵒᵈ) x

Product of Left-Infinite Intervals is Contained in Product Space Left-Infinite Interval

Informal description

For a nonempty index set $\iota$ and a family of preorders $\{\alpha_i\}_{i \in \iota}$, the product of left-infinite right-open intervals $\prod_{i \in \iota} (-\infty, x_i)$ is contained in the left-infinite right-open interval $(-\infty, x)$ of the product space $\prod_{i \in \iota} \alpha_i$, where $x = (x_i)_{i \in \iota}$.

Set.pi_univ_Ioo_subset theorem

[Nonempty ι] : (pi univ fun i ↦ Ioo (x i) (y i)) ⊆ Ioo x y

Full source

theorem pi_univ_Ioo_subset [Nonempty ι]: (pi univ fun i ↦ Ioo (x i) (y i)) ⊆ Ioo x y := fun _ hx ↦
  ⟨(pi_univ_Ioi_subset _) fun i hi ↦ (hx i hi).1, (pi_univ_Iio_subset _) fun i hi ↦ (hx i hi).2⟩

Product of Open Intervals is Contained in Product Space Open Interval

Informal description

For a nonempty index set $\iota$ and a family of preorders $\{\alpha_i\}_{i \in \iota}$, the product of open intervals $\prod_{i \in \iota} (x_i, y_i)$ is contained in the open interval $(x, y)$ of the product space $\prod_{i \in \iota} \alpha_i$, where $x = (x_i)_{i \in \iota}$ and $y = (y_i)_{i \in \iota}$.

Set.pi_univ_Ioc_subset theorem

[Nonempty ι] : (pi univ fun i ↦ Ioc (x i) (y i)) ⊆ Ioc x y

Full source

theorem pi_univ_Ioc_subset [Nonempty ι]: (pi univ fun i ↦ Ioc (x i) (y i)) ⊆ Ioc x y := fun _ hx ↦
  ⟨(pi_univ_Ioi_subset _) fun i hi ↦ (hx i hi).1, fun i ↦ (hx i trivial).2⟩

Product of Left-Open Right-Closed Intervals is Contained in Product Space Left-Open Right-Closed Interval

Informal description

For a nonempty index set $\iota$ and a family of preorders $\{\alpha_i\}_{i \in \iota}$, the product of left-open right-closed intervals $\prod_{i \in \iota} (x_i, y_i]$ is contained in the left-open right-closed interval $(x, y]$ of the product space $\prod_{i \in \iota} \alpha_i$, where $x = (x_i)_{i \in \iota}$ and $y = (y_i)_{i \in \iota}$.

Set.pi_univ_Ico_subset theorem

[Nonempty ι] : (pi univ fun i ↦ Ico (x i) (y i)) ⊆ Ico x y

Full source

theorem pi_univ_Ico_subset [Nonempty ι]: (pi univ fun i ↦ Ico (x i) (y i)) ⊆ Ico x y := fun _ hx ↦
  ⟨fun i ↦ (hx i trivial).1, (pi_univ_Iio_subset _) fun i hi ↦ (hx i hi).2⟩

Product of Left-Closed Right-Open Intervals is Contained in Product Space Left-Closed Right-Open Interval

Informal description

For a nonempty index set $\iota$ and a family of preorders $\{\alpha_i\}_{i \in \iota}$, the product of left-closed right-open intervals $\prod_{i \in \iota} [x_i, y_i)$ is contained in the left-closed right-open interval $[x, y)$ of the product space $\prod_{i \in \iota} \alpha_i$, where $x = (x_i)_{i \in \iota}$ and $y = (y_i)_{i \in \iota}$.

Set.pi_univ_Ioc_update_left theorem

 {x y : ∀ i, α i} {i₀ : ι} {m : α i₀} (hm : x i₀ ≤ m) :
  (pi univ fun i ↦ Ioc (update x i₀ m i) (y i)) = {z | m < z i₀} ∩ pi univ fun i ↦ Ioc (x i) (y i)

Full source

theorem pi_univ_Ioc_update_left {x y : ∀ i, α i} {i₀ : ι} {m : α i₀} (hm : x i₀ ≤ m) :
    (pi univ fun i ↦ Ioc (update x i₀ m i) (y i)) =
      { z | m < z i₀ }{ z | m < z i₀ } ∩ pi univ fun i ↦ Ioc (x i) (y i) := by
  have : Ioc m (y i₀) = IoiIoi m ∩ Ioc (x i₀) (y i₀) := by
    rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc,
      inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)]
  simp_rw [univ_pi_update i₀ _ _ fun i z ↦ Ioc z (y i), ← pi_inter_compl ({i₀} : Set ι),
    singleton_pi', ← inter_assoc, this]
  rfl

Product of Intervals with Left Update Equals Intersection with Strict Inequality Condition

Informal description

Let $\{α_i\}_{i \in \iota}$ be a family of preorders, $x, y \in \prod_{i \in \iota} α_i$, $i_0 \in \iota$, and $m \in α_{i_0}$ such that $x_{i_0} \leq m$. Then the product of intervals $\prod_{i \in \iota} (x'_i, y_i]$, where $x'$ is the function $x$ updated at $i_0$ to have value $m$, is equal to the intersection of two sets: the set of functions $z$ satisfying $m < z_{i_0}$, and the product of intervals $\prod_{i \in \iota} (x_i, y_i]$. In symbols: $$ \prod_{i \in \iota} (x'_i, y_i] = \{z \mid m < z_{i_0}\} \cap \prod_{i \in \iota} (x_i, y_i] $$ where $x'_i = \begin{cases} m & \text{if } i = i_0 \\ x_i & \text{otherwise} \end{cases}$.

Set.pi_univ_Ioc_update_right theorem

 {x y : ∀ i, α i} {i₀ : ι} {m : α i₀} (hm : m ≤ y i₀) :
  (pi univ fun i ↦ Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ pi univ fun i ↦ Ioc (x i) (y i)

Full source

theorem pi_univ_Ioc_update_right {x y : ∀ i, α i} {i₀ : ι} {m : α i₀} (hm : m ≤ y i₀) :
    (pi univ fun i ↦ Ioc (x i) (update y i₀ m i)) =
      { z | z i₀ ≤ m }{ z | z i₀ ≤ m } ∩ pi univ fun i ↦ Ioc (x i) (y i) := by
  have : Ioc (x i₀) m = IicIic m ∩ Ioc (x i₀) (y i₀) := by
    rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
      inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]
  simp_rw [univ_pi_update i₀ y m fun i z ↦ Ioc (x i) z, ← pi_inter_compl ({i₀} : Set ι),
    singleton_pi', ← inter_assoc, this]
  rfl

Product of Right-Modified Intervals Equals Intersection with Coordinate Constraint

Informal description

Let $\{α_i\}_{i \in \iota}$ be a family of preorders, $x, y \in \prod_{i \in \iota} α_i$, $i_0 \in \iota$, and $m \in α_{i_0}$ such that $m \leq y_{i_0}$. Then the product of intervals $\prod_{i \in \iota} (x_i, y'_i]$, where $y'$ is the function $y$ updated at $i_0$ to have value $m$, is equal to the intersection of two sets: the set of functions $z$ satisfying $z_{i_0} \leq m$, and the product of intervals $\prod_{i \in \iota} (x_i, y_i]$. In symbols: $$ \prod_{i \in \iota} (x_i, y'_i] = \{z \mid z_{i_0} \leq m\} \cap \prod_{i \in \iota} (x_i, y_i] $$ where $y'_i = \begin{cases} m & \text{if } i = i_0 \\ y_i & \text{otherwise} \end{cases}$.

Set.disjoint_pi_univ_Ioc_update_left_right theorem

 {x y : ∀ i, α i} {i₀ : ι} {m : α i₀} :
  Disjoint (pi univ fun i ↦ Ioc (x i) (update y i₀ m i)) (pi univ fun i ↦ Ioc (update x i₀ m i) (y i))

Full source

theorem disjoint_pi_univ_Ioc_update_left_right {x y : ∀ i, α i} {i₀ : ι} {m : α i₀} :
    Disjoint (pi univ fun i ↦ Ioc (x i) (update y i₀ m i))
    (pi univ fun i ↦ Ioc (update x i₀ m i) (y i)) := by
  rw [disjoint_left]
  rintro z h₁ h₂
  refine (h₁ i₀ (mem_univ _)).2.not_lt ?_
  simpa only [Function.update_self] using (h₂ i₀ (mem_univ _)).1

Disjointness of Modified Product Intervals in Function Space

Informal description

For any functions $x, y \in \prod_{i} \alpha_i$, index $i_0 \in \iota$, and element $m \in \alpha_{i_0}$, the following two sets are disjoint: 1. The product $\prod_{i \in \iota} (x_i, y_i]$ where $y_{i_0}$ is replaced with $m$ 2. The product $\prod_{i \in \iota} (x_i, y_i]$ where $x_{i_0}$ is replaced with $m$ In other words, the sets $\prod_{i \in \iota} (x_i, \text{update } y i_0 m i]$ and $\prod_{i \in \iota} (\text{update } x i_0 m i, y_i]$ are disjoint.

Set.image_update_Icc theorem

(f : ∀ i, α i) (i : ι) (a b : α i) : update f i '' Icc a b = Icc (update f i a) (update f i b)

Full source

theorem image_update_Icc (f : ∀ i, α i) (i : ι) (a b : α i) :
    updateupdate f i '' Icc a b = Icc (update f i a) (update f i b) := by
  ext x
  rw [← Set.pi_univ_Icc]
  refine ⟨?_, fun h => ⟨x i, ?_, ?_⟩⟩
  · rintro ⟨c, hc, rfl⟩
    simpa [update_le_update_iff]
  · simpa only [Function.update_self] using h i (mem_univ i)
  · ext j
    obtain rfl | hij := eq_or_ne i j
    · exact Function.update_self ..
    · simpa only [Function.update_of_ne hij.symm, le_antisymm_iff] using h j (mem_univ j)

Image of Closed Interval under Function Update Equals Closed Interval of Updated Functions

Informal description

For any function $f \in \prod_{i} \alpha_i$, index $i \in \iota$, and elements $a, b \in \alpha_i$, the image of the closed interval $[a, b]$ under the function update operation at index $i$ is equal to the closed interval between the updated functions. That is, \[ \text{update } f i \text{ } '' [a, b] = [\text{update } f i \text{ } a, \text{update } f i \text{ } b]. \]

Set.image_update_Ico theorem

(f : ∀ i, α i) (i : ι) (a b : α i) : update f i '' Ico a b = Ico (update f i a) (update f i b)

Full source

theorem image_update_Ico (f : ∀ i, α i) (i : ι) (a b : α i) :
    updateupdate f i '' Ico a b = Ico (update f i a) (update f i b) := by
  rw [← Icc_diff_right, ← Icc_diff_right, image_diff (update_injective _ _), image_singleton,
    image_update_Icc]

Image of Left-Closed Right-Open Interval under Function Update Equals Left-Closed Right-Open Interval of Updated Functions

Informal description

For any function $f \in \prod_{i} \alpha_i$, index $i \in \iota$, and elements $a, b \in \alpha_i$, the image of the left-closed right-open interval $[a, b)$ under the function update operation at index $i$ is equal to the left-closed right-open interval between the updated functions. That is, \[ \text{update } f i \text{ } '' [a, b) = [\text{update } f i \text{ } a, \text{update } f i \text{ } b). \]

Set.image_update_Ioc theorem

(f : ∀ i, α i) (i : ι) (a b : α i) : update f i '' Ioc a b = Ioc (update f i a) (update f i b)

Full source

theorem image_update_Ioc (f : ∀ i, α i) (i : ι) (a b : α i) :
    updateupdate f i '' Ioc a b = Ioc (update f i a) (update f i b) := by
  rw [← Icc_diff_left, ← Icc_diff_left, image_diff (update_injective _ _), image_singleton,
    image_update_Icc]

Image of Left-Open Right-Closed Interval under Function Update Equals Left-Open Right-Closed Interval of Updated Functions

Informal description

For any function $f \in \prod_{i} \alpha_i$, index $i \in \iota$, and elements $a, b \in \alpha_i$, the image of the left-open right-closed interval $(a, b]$ under the function update operation at index $i$ is equal to the left-open right-closed interval between the updated functions. That is, \[ \text{update } f i \text{ } '' (a, b] = (\text{update } f i \text{ } a, \text{update } f i \text{ } b]. \]

Set.image_update_Ioo theorem

(f : ∀ i, α i) (i : ι) (a b : α i) : update f i '' Ioo a b = Ioo (update f i a) (update f i b)

Full source

theorem image_update_Ioo (f : ∀ i, α i) (i : ι) (a b : α i) :
    updateupdate f i '' Ioo a b = Ioo (update f i a) (update f i b) := by
  rw [← Ico_diff_left, ← Ico_diff_left, image_diff (update_injective _ _), image_singleton,
    image_update_Ico]

Image of Open Interval under Function Update Equals Open Interval of Updated Functions

Informal description

For any function $f \in \prod_{i} \alpha_i$, index $i \in \iota$, and elements $a, b \in \alpha_i$, the image of the open interval $(a, b)$ under the function update operation at index $i$ is equal to the open interval between the updated functions. That is, \[ \text{update } f i \text{ } '' (a, b) = (\text{update } f i \text{ } a, \text{update } f i \text{ } b). \]

Set.image_update_Icc_left theorem

(f : ∀ i, α i) (i : ι) (a : α i) : update f i '' Icc a (f i) = Icc (update f i a) f

Full source

theorem image_update_Icc_left (f : ∀ i, α i) (i : ι) (a : α i) :
    updateupdate f i '' Icc a (f i) = Icc (update f i a) f := by simpa using image_update_Icc f i a (f i)

Image of Left-Closed Interval under Function Update Equals Closed Interval of Updated Function

Informal description

For any function $f \in \prod_{i} \alpha_i$, index $i \in \iota$, and element $a \in \alpha_i$, the image of the closed interval $[a, f(i)]$ under the function update operation at index $i$ is equal to the closed interval between the updated function $\text{update } f i \text{ } a$ and the original function $f$. That is, \[ \text{update } f i \text{ } '' [a, f(i)] = [\text{update } f i \text{ } a, f]. \]

Set.image_update_Ico_left theorem

(f : ∀ i, α i) (i : ι) (a : α i) : update f i '' Ico a (f i) = Ico (update f i a) f

Full source

theorem image_update_Ico_left (f : ∀ i, α i) (i : ι) (a : α i) :
    updateupdate f i '' Ico a (f i) = Ico (update f i a) f := by simpa using image_update_Ico f i a (f i)

Image of Left-Closed Right-Open Interval under Function Update Equals Left-Closed Right-Open Interval of Updated Function

Informal description

For any function $f \in \prod_{i} \alpha_i$, index $i \in \iota$, and element $a \in \alpha_i$, the image of the left-closed right-open interval $[a, f(i))$ under the function update operation at index $i$ is equal to the left-closed right-open interval between the updated function $\text{update } f i \text{ } a$ and the original function $f$. That is, \[ \text{update } f i \text{ } '' [a, f(i)) = [\text{update } f i \text{ } a, f). \]

Set.image_update_Ioc_left theorem

(f : ∀ i, α i) (i : ι) (a : α i) : update f i '' Ioc a (f i) = Ioc (update f i a) f

Full source

theorem image_update_Ioc_left (f : ∀ i, α i) (i : ι) (a : α i) :
    updateupdate f i '' Ioc a (f i) = Ioc (update f i a) f := by simpa using image_update_Ioc f i a (f i)

Image of Left-Open Right-Closed Interval under Function Update Equals Left-Open Right-Closed Interval of Updated Function

Informal description

For any function $f \in \prod_{i} \alpha_i$, index $i \in \iota$, and element $a \in \alpha_i$, the image of the left-open right-closed interval $(a, f(i)]$ under the function update operation at index $i$ is equal to the left-open right-closed interval between the updated function $\text{update } f i \text{ } a$ and the original function $f$. That is, \[ \text{update } f i \text{ } '' (a, f(i)] = (\text{update } f i \text{ } a, f]. \]

Set.image_update_Ioo_left theorem

(f : ∀ i, α i) (i : ι) (a : α i) : update f i '' Ioo a (f i) = Ioo (update f i a) f

Full source

theorem image_update_Ioo_left (f : ∀ i, α i) (i : ι) (a : α i) :
    updateupdate f i '' Ioo a (f i) = Ioo (update f i a) f := by simpa using image_update_Ioo f i a (f i)

Image of Open Interval under Left Function Update Equals Open Interval of Updated and Original Functions

Informal description

For any function $f \in \prod_{i} \alpha_i$, index $i \in \iota$, and element $a \in \alpha_i$, the image of the open interval $(a, f(i))$ under the function update operation at index $i$ is equal to the open interval between the updated function $\text{update } f i \text{ } a$ and the original function $f$. That is, \[ \text{update } f i \text{ } '' (a, f(i)) = (\text{update } f i \text{ } a, f). \]

Set.image_update_Icc_right theorem

(f : ∀ i, α i) (i : ι) (b : α i) : update f i '' Icc (f i) b = Icc f (update f i b)

Full source

theorem image_update_Icc_right (f : ∀ i, α i) (i : ι) (b : α i) :
    updateupdate f i '' Icc (f i) b = Icc f (update f i b) := by simpa using image_update_Icc f i (f i) b

Image of Right Closed Interval under Function Update Equals Closed Interval of Original and Updated Functions

Informal description

For any function $f \in \prod_{i} \alpha_i$, index $i \in \iota$, and element $b \in \alpha_i$, the image of the closed interval $[f(i), b]$ under the function update operation at index $i$ is equal to the closed interval between $f$ and the updated function. That is, \[ \text{update } f i \text{ } '' [f(i), b] = [f, \text{update } f i \text{ } b]. \]

Set.image_update_Ico_right theorem

(f : ∀ i, α i) (i : ι) (b : α i) : update f i '' Ico (f i) b = Ico f (update f i b)

Full source

theorem image_update_Ico_right (f : ∀ i, α i) (i : ι) (b : α i) :
    updateupdate f i '' Ico (f i) b = Ico f (update f i b) := by simpa using image_update_Ico f i (f i) b

Image of Left-Closed Right-Open Interval under Right Function Update Equals Left-Closed Right-Open Interval of Original and Updated Functions

Informal description

For any function $f \in \prod_{i} \alpha_i$, index $i \in \iota$, and element $b \in \alpha_i$, the image of the left-closed right-open interval $[f(i), b)$ under the function update operation at index $i$ is equal to the left-closed right-open interval between $f$ and the updated function. That is, \[ \text{update } f i \text{ } '' [f(i), b) = [f, \text{update } f i \text{ } b). \]

Set.image_update_Ioc_right theorem

(f : ∀ i, α i) (i : ι) (b : α i) : update f i '' Ioc (f i) b = Ioc f (update f i b)

Full source

theorem image_update_Ioc_right (f : ∀ i, α i) (i : ι) (b : α i) :
    updateupdate f i '' Ioc (f i) b = Ioc f (update f i b) := by simpa using image_update_Ioc f i (f i) b

Image of Left-Open Right-Closed Interval under Right Function Update Equals Left-Open Right-Closed Interval of Original and Updated Functions

Informal description

For any function $f \in \prod_{i} \alpha_i$, index $i \in \iota$, and element $b \in \alpha_i$, the image of the left-open right-closed interval $(f(i), b]$ under the function update operation at index $i$ is equal to the left-open right-closed interval between $f$ and the updated function. That is, \[ \text{update } f i \text{ } '' (f(i), b] = (f, \text{update } f i \text{ } b]. \]

Set.image_update_Ioo_right theorem

(f : ∀ i, α i) (i : ι) (b : α i) : update f i '' Ioo (f i) b = Ioo f (update f i b)

Full source

theorem image_update_Ioo_right (f : ∀ i, α i) (i : ι) (b : α i) :
    updateupdate f i '' Ioo (f i) b = Ioo f (update f i b) := by simpa using image_update_Ioo f i (f i) b

Image of Open Interval under Right Function Update Equals Open Interval of Original and Updated Functions

Informal description

For any function $f \in \prod_{i} \alpha_i$, index $i \in \iota$, and element $b \in \alpha_i$, the image of the open interval $(f(i), b)$ under the function update operation at index $i$ is equal to the open interval between $f$ and the updated function. That is, \[ \text{update } f i \text{ } '' (f(i), b) = (f, \text{update } f i \text{ } b). \]

Set.image_mulSingle_Icc theorem

(i : ι) (a b : α i) : Pi.mulSingle i '' Icc a b = Icc (Pi.mulSingle i a) (Pi.mulSingle i b)

Full source

@[to_additive]
theorem image_mulSingle_Icc (i : ι) (a b : α i) :
    Pi.mulSinglePi.mulSingle i '' Icc a b = Icc (Pi.mulSingle i a) (Pi.mulSingle i b) :=
  image_update_Icc _ _ _ _

Image of Closed Interval under Pointwise Multiplication Equals Closed Interval of Multiplied Functions

Informal description

For any index $i \in \iota$ and elements $a, b \in \alpha_i$, the image of the closed interval $[a, b]$ under the pointwise multiplication function $\text{mulSingle}_i$ (which sets the $i$-th coordinate and leaves others unchanged) is equal to the closed interval between the pointwise multiplication functions applied to $a$ and $b$ respectively. That is, \[ \text{mulSingle}_i([a, b]) = [\text{mulSingle}_i(a), \text{mulSingle}_i(b)]. \]

Set.image_mulSingle_Ico theorem

(i : ι) (a b : α i) : Pi.mulSingle i '' Ico a b = Ico (Pi.mulSingle i a) (Pi.mulSingle i b)

Full source

@[to_additive]
theorem image_mulSingle_Ico (i : ι) (a b : α i) :
    Pi.mulSinglePi.mulSingle i '' Ico a b = Ico (Pi.mulSingle i a) (Pi.mulSingle i b) :=
  image_update_Ico _ _ _ _

Image of $[a, b)$ under $\text{mulSingle}_i$ equals $[\text{mulSingle}_i(a), \text{mulSingle}_i(b))$

Informal description

For any index $i \in \iota$ and elements $a, b \in \alpha_i$, the image of the left-closed right-open interval $[a, b)$ under the pointwise multiplication function $\text{mulSingle}_i$ (which sets the $i$-th coordinate to a given value and leaves others unchanged) is equal to the left-closed right-open interval between the pointwise multiplication functions applied to $a$ and $b$ respectively. That is, \[ \text{mulSingle}_i([a, b)) = [\text{mulSingle}_i(a), \text{mulSingle}_i(b)). \]

Set.image_mulSingle_Ioc theorem

(i : ι) (a b : α i) : Pi.mulSingle i '' Ioc a b = Ioc (Pi.mulSingle i a) (Pi.mulSingle i b)

Full source

@[to_additive]
theorem image_mulSingle_Ioc (i : ι) (a b : α i) :
    Pi.mulSinglePi.mulSingle i '' Ioc a b = Ioc (Pi.mulSingle i a) (Pi.mulSingle i b) :=
  image_update_Ioc _ _ _ _

Image of Left-Open Right-Closed Interval under Pointwise Multiplication Equals Left-Open Right-Closed Interval of Multiplied Functions

Informal description

For any index $i \in \iota$ and elements $a, b \in \alpha_i$, the image of the left-open right-closed interval $(a, b]$ under the pointwise multiplication function $\text{mulSingle}_i$ is equal to the left-open right-closed interval between the pointwise multiplication functions applied to $a$ and $b$ respectively. That is, \[ \text{mulSingle}_i((a, b]) = (\text{mulSingle}_i(a), \text{mulSingle}_i(b)]. \]

Set.image_mulSingle_Ioo theorem

(i : ι) (a b : α i) : Pi.mulSingle i '' Ioo a b = Ioo (Pi.mulSingle i a) (Pi.mulSingle i b)

Full source

@[to_additive]
theorem image_mulSingle_Ioo (i : ι) (a b : α i) :
    Pi.mulSinglePi.mulSingle i '' Ioo a b = Ioo (Pi.mulSingle i a) (Pi.mulSingle i b) :=
  image_update_Ioo _ _ _ _

Image of Open Interval under Pointwise Multiplication Equals Open Interval of Multiplied Functions

Informal description

For any index $i \in \iota$ and elements $a, b \in \alpha_i$, the image of the open interval $(a, b)$ under the pointwise multiplication function $\text{mulSingle}_i$ is equal to the open interval between the pointwise multiplication functions applied to $a$ and $b$ respectively. That is, \[ \text{mulSingle}_i((a, b)) = (\text{mulSingle}_i(a), \text{mulSingle}_i(b)). \]

Set.image_mulSingle_Icc_left theorem

(i : ι) (a : α i) : Pi.mulSingle i '' Icc a 1 = Icc (Pi.mulSingle i a) 1

Full source

@[to_additive]
theorem image_mulSingle_Icc_left (i : ι) (a : α i) :
    Pi.mulSinglePi.mulSingle i '' Icc a 1 = Icc (Pi.mulSingle i a) 1 :=
  image_update_Icc_left _ _ _

Image of Closed Interval under Pointwise Multiplication Equals Closed Interval of Multiplied Elements

Informal description

For any index $i \in \iota$ and element $a \in \alpha_i$, the image of the closed interval $[a, 1]$ under the pointwise multiplication operation $\text{mulSingle}_i$ is equal to the closed interval between $\text{mulSingle}_i(a)$ and $1$. That is, \[ \text{mulSingle}_i '' [a, 1] = [\text{mulSingle}_i(a), 1]. \]

Set.image_mulSingle_Ico_left theorem

(i : ι) (a : α i) : Pi.mulSingle i '' Ico a 1 = Ico (Pi.mulSingle i a) 1

Full source

@[to_additive]
theorem image_mulSingle_Ico_left (i : ι) (a : α i) :
    Pi.mulSinglePi.mulSingle i '' Ico a 1 = Ico (Pi.mulSingle i a) 1 :=
  image_update_Ico_left _ _ _

Image of Left-Closed Right-Open Interval under Pointwise Multiplication Equals Left-Closed Right-Open Interval of Multiplied Elements

Informal description

For any index $i \in \iota$ and element $a \in \alpha_i$, the image of the left-closed right-open interval $[a, 1)$ under the pointwise multiplication operation $\text{mulSingle}_i$ is equal to the left-closed right-open interval between $\text{mulSingle}_i(a)$ and $1$. That is, \[ \text{mulSingle}_i '' [a, 1) = [\text{mulSingle}_i(a), 1). \]

Set.image_mulSingle_Ioc_left theorem

(i : ι) (a : α i) : Pi.mulSingle i '' Ioc a 1 = Ioc (Pi.mulSingle i a) 1

Full source

@[to_additive]
theorem image_mulSingle_Ioc_left (i : ι) (a : α i) :
    Pi.mulSinglePi.mulSingle i '' Ioc a 1 = Ioc (Pi.mulSingle i a) 1 :=
  image_update_Ioc_left _ _ _

Image of Left-Open Right-Closed Interval under Pointwise Multiplication Equals Left-Open Right-Closed Interval of Multiplied Elements

Informal description

For any index $i \in \iota$ and element $a \in \alpha_i$, the image of the left-open right-closed interval $(a, 1]$ under the pointwise multiplication operation $\text{mulSingle}_i$ is equal to the left-open right-closed interval between $\text{mulSingle}_i(a)$ and the constant function $1$. That is, \[ \text{mulSingle}_i \text{ }'' (a, 1] = (\text{mulSingle}_i(a), 1]. \]

Set.image_mulSingle_Ioo_left theorem

(i : ι) (a : α i) : Pi.mulSingle i '' Ioo a 1 = Ioo (Pi.mulSingle i a) 1

Full source

@[to_additive]
theorem image_mulSingle_Ioo_left (i : ι) (a : α i) :
    Pi.mulSinglePi.mulSingle i '' Ioo a 1 = Ioo (Pi.mulSingle i a) 1 :=
  image_update_Ioo_left _ _ _

Image of Open Interval under Pointwise Multiplication Equals Open Interval of Multiplied Elements

Informal description

For any index $i \in \iota$ and element $a \in \alpha_i$, the image of the open interval $(a, 1)$ under the pointwise multiplication operation $\text{mulSingle}_i$ is equal to the open interval between $\text{mulSingle}_i(a)$ and the constant function $1$. That is, \[ \text{mulSingle}_i \text{ }'' (a, 1) = (\text{mulSingle}_i(a), 1). \]

Set.image_mulSingle_Icc_right theorem

(i : ι) (b : α i) : Pi.mulSingle i '' Icc 1 b = Icc 1 (Pi.mulSingle i b)

Full source

@[to_additive]
theorem image_mulSingle_Icc_right (i : ι) (b : α i) :
    Pi.mulSinglePi.mulSingle i '' Icc 1 b = Icc 1 (Pi.mulSingle i b) :=
  image_update_Icc_right _ _ _

Image of Closed Interval under Pointwise Multiplication Equals Closed Interval of Updated Function

Informal description

For any index $i \in \iota$ and element $b \in \alpha_i$, the image of the closed interval $[1, b]$ under the pointwise multiplication function `Pi.mulSingle i` is equal to the closed interval between the constant function $1$ and the function updated at $i$ with $b$. That is, \[ \text{Pi.mulSingle } i \text{ } '' [1, b] = [1, \text{Pi.mulSingle } i \text{ } b]. \]

Set.image_mulSingle_Ico_right theorem

(i : ι) (b : α i) : Pi.mulSingle i '' Ico 1 b = Ico 1 (Pi.mulSingle i b)

Full source

@[to_additive]
theorem image_mulSingle_Ico_right (i : ι) (b : α i) :
    Pi.mulSinglePi.mulSingle i '' Ico 1 b = Ico 1 (Pi.mulSingle i b) :=
  image_update_Ico_right _ _ _

Image of Left-Closed Right-Open Interval under Pointwise Multiplication Equals Left-Closed Right-Open Interval of Updated Function

Informal description

For any index $i \in \iota$ and element $b \in \alpha_i$, the image of the left-closed right-open interval $[1, b)$ under the pointwise multiplication function $\text{Pi.mulSingle } i$ is equal to the left-closed right-open interval between the constant function $1$ and the function updated at $i$ with $b$. That is, \[ \text{Pi.mulSingle } i \text{ } '' [1, b) = [1, \text{Pi.mulSingle } i \text{ } b). \]

Set.image_mulSingle_Ioc_right theorem

(i : ι) (b : α i) : Pi.mulSingle i '' Ioc 1 b = Ioc 1 (Pi.mulSingle i b)

Full source

@[to_additive]
theorem image_mulSingle_Ioc_right (i : ι) (b : α i) :
    Pi.mulSinglePi.mulSingle i '' Ioc 1 b = Ioc 1 (Pi.mulSingle i b) :=
  image_update_Ioc_right _ _ _

Image of Left-Open Right-Closed Interval under Pointwise Multiplication Equals Left-Open Right-Closed Interval of Updated Function

Informal description

For any index $i$ in the index set $\iota$ and any element $b$ in $\alpha_i$, the image of the left-open right-closed interval $(1, b]$ under the pointwise multiplication function $\text{mulSingle}_i$ is equal to the left-open right-closed interval between the constant function $1$ and the function $\text{mulSingle}_i(b)$. That is, \[ \text{mulSingle}_i \text{ } '' (1, b] = (1, \text{mulSingle}_i(b)]. \]

Set.image_mulSingle_Ioo_right theorem

(i : ι) (b : α i) : Pi.mulSingle i '' Ioo 1 b = Ioo 1 (Pi.mulSingle i b)

Full source

@[to_additive]
theorem image_mulSingle_Ioo_right (i : ι) (b : α i) :
    Pi.mulSinglePi.mulSingle i '' Ioo 1 b = Ioo 1 (Pi.mulSingle i b) :=
  image_update_Ioo_right _ _ _

Image of Open Interval under Pointwise Multiplication Equals Open Interval of Updated Function

Informal description

For any index $i$ in the index set $\iota$ and any element $b$ in $\alpha_i$, the image of the open interval $(1, b)$ under the pointwise multiplication function $\text{mulSingle}_i$ is equal to the open interval between the constant function $1$ and the function $\text{mulSingle}_i(b)$. That is, \[ \text{mulSingle}_i \text{ } '' (1, b) = (1, \text{mulSingle}_i(b)). \]

Set.pi_univ_uIcc theorem

(a b : ∀ i, α i) : (pi univ fun i => uIcc (a i) (b i)) = uIcc a b

Full source

@[simp]
theorem pi_univ_uIcc (a b : ∀ i, α i) : (pi univ fun i => uIcc (a i) (b i)) = uIcc a b :=
  pi_univ_Icc _ _

Product of Closed Intervals Equals Closed Interval in Product Space for Unordered Intervals

Informal description

For a family of types $\alpha_i$ indexed by $i \in \iota$ and elements $a, b \in \prod_{i} \alpha_i$, the product over all indices $i$ of the closed intervals $[\min(a_i, b_i), \max(a_i, b_i)]$ is equal to the closed interval $[\min(a, b), \max(a, b)]$ in the product space. That is, \[ \prod_{i \in \iota} [\min(a_i, b_i), \max(a_i, b_i)] = [\min(a, b), \max(a, b)]. \]

Set.image_update_uIcc theorem

(f : ∀ i, α i) (i : ι) (a b : α i) : update f i '' uIcc a b = uIcc (update f i a) (update f i b)

Full source

theorem image_update_uIcc (f : ∀ i, α i) (i : ι) (a b : α i) :
    updateupdate f i '' uIcc a b = uIcc (update f i a) (update f i b) :=
  (image_update_Icc _ _ _ _).trans <| by simp_rw [uIcc, update_sup, update_inf]

Image of Unordered Closed Interval under Function Update Equals Unordered Closed Interval of Updated Functions

Informal description

For any function $f \in \prod_{i} \alpha_i$, index $i \in \iota$, and elements $a, b \in \alpha_i$, the image of the unordered closed interval $[\min(a, b), \max(a, b)]$ under the function update operation at index $i$ is equal to the unordered closed interval between the updated functions. That is, \[ \text{update } f i \text{ } '' [\min(a, b), \max(a, b)] = [\min(\text{update } f i \text{ } a, \text{update } f i \text{ } b), \max(\text{update } f i \text{ } a, \text{update } f i \text{ } b)]. \]

Set.image_update_uIcc_left theorem

(f : ∀ i, α i) (i : ι) (a : α i) : update f i '' uIcc a (f i) = uIcc (update f i a) f

Full source

theorem image_update_uIcc_left (f : ∀ i, α i) (i : ι) (a : α i) :
    updateupdate f i '' uIcc a (f i) = uIcc (update f i a) f := by
  simpa using image_update_uIcc f i a (f i)

Image of Left Unordered Closed Interval under Function Update Equals Unordered Closed Interval of Updated and Original Functions

Informal description

For any function $f \in \prod_{i} \alpha_i$, index $i \in \iota$, and element $a \in \alpha_i$, the image of the unordered closed interval $[\min(a, f_i), \max(a, f_i)]$ under the function update operation at index $i$ is equal to the unordered closed interval between the updated function $\text{update } f i \text{ } a$ and the original function $f$. That is, \[ \text{update } f i \text{ } '' [\min(a, f_i), \max(a, f_i)] = [\min(\text{update } f i \text{ } a, f), \max(\text{update } f i \text{ } a, f)]. \]

Set.image_update_uIcc_right theorem

(f : ∀ i, α i) (i : ι) (b : α i) : update f i '' uIcc (f i) b = uIcc f (update f i b)

Full source

theorem image_update_uIcc_right (f : ∀ i, α i) (i : ι) (b : α i) :
    updateupdate f i '' uIcc (f i) b = uIcc f (update f i b) := by
  simpa using image_update_uIcc f i (f i) b

Image of Right Unordered Closed Interval under Function Update Equals Unordered Closed Interval of Original and Updated Functions

Informal description

For any function $f \in \prod_{i} \alpha_i$, index $i \in \iota$, and element $b \in \alpha_i$, the image of the unordered closed interval $[\min(f_i, b), \max(f_i, b)]$ under the function update operation at index $i$ is equal to the unordered closed interval between the original function $f$ and the updated function $\text{update } f i \text{ } b$. That is, \[ \text{update } f i \text{ } '' [\min(f_i, b), \max(f_i, b)] = [\min(f, \text{update } f i \text{ } b), \max(f, \text{update } f i \text{ } b)]. \]

Set.image_mulSingle_uIcc theorem

(i : ι) (a b : α i) : Pi.mulSingle i '' uIcc a b = uIcc (Pi.mulSingle i a) (Pi.mulSingle i b)

Full source

@[to_additive]
theorem image_mulSingle_uIcc (i : ι) (a b : α i) :
    Pi.mulSinglePi.mulSingle i '' uIcc a b = uIcc (Pi.mulSingle i a) (Pi.mulSingle i b) :=
  image_update_uIcc _ _ _ _

Image of Unordered Closed Interval under Component-wise Function Equals Unordered Closed Interval of Component-wise Functions

Informal description

For any index $i \in \iota$ and elements $a, b \in \alpha_i$, the image of the unordered closed interval $[\min(a, b), \max(a, b)]$ under the function $\text{mulSingle}_i$ (which sets the $i$-th component to a given value and leaves other components unchanged) is equal to the unordered closed interval between the functions $\text{mulSingle}_i(a)$ and $\text{mulSingle}_i(b)$. That is, \[ \text{mulSingle}_i \text{ } '' [\min(a, b), \max(a, b)] = [\min(\text{mulSingle}_i(a), \text{mulSingle}_i(b)), \max(\text{mulSingle}_i(a), \text{mulSingle}_i(b))]. \]

Set.image_mulSingle_uIcc_left theorem

(i : ι) (a : α i) : Pi.mulSingle i '' uIcc a 1 = uIcc (Pi.mulSingle i a) 1

Full source

@[to_additive]
theorem image_mulSingle_uIcc_left (i : ι) (a : α i) :
    Pi.mulSinglePi.mulSingle i '' uIcc a 1 = uIcc (Pi.mulSingle i a) 1 :=
  image_update_uIcc_left _ _ _

Image of Left Unordered Closed Interval under Component-wise Function Equals Unordered Closed Interval of Component-wise Function and Constant One

Informal description

For any index $i$ in the index set $\iota$ and element $a$ in $\alpha_i$, the image of the unordered closed interval $[\min(a, 1), \max(a, 1)]$ under the component-wise function $\text{mulSingle}_i$ (which sets the $i$-th component to a given value and leaves other components unchanged) is equal to the unordered closed interval between the function $\text{mulSingle}_i(a)$ and the constant function $1$. That is, \[ \text{mulSingle}_i \text{ } '' [\min(a, 1), \max(a, 1)] = [\min(\text{mulSingle}_i(a), 1), \max(\text{mulSingle}_i(a), 1)]. \]

Set.image_mulSingle_uIcc_right theorem

(i : ι) (b : α i) : Pi.mulSingle i '' uIcc 1 b = uIcc 1 (Pi.mulSingle i b)

Full source

@[to_additive]
theorem image_mulSingle_uIcc_right (i : ι) (b : α i) :
    Pi.mulSinglePi.mulSingle i '' uIcc 1 b = uIcc 1 (Pi.mulSingle i b) :=
  image_update_uIcc_right _ _ _

Image of Right Unordered Interval under Component-wise Function Equals Unordered Interval of Constant and Component-wise Functions

Informal description

For any index $i \in \iota$ and element $b \in \alpha_i$, the image of the unordered closed interval $[\min(1, b), \max(1, b)]$ under the function $\text{mulSingle}_i$ (which sets the $i$-th component to a given value and leaves other components unchanged) is equal to the unordered closed interval between the constant function $1$ and the function $\text{mulSingle}_i(b)$. That is, \[ \text{mulSingle}_i \text{ } '' [\min(1, b), \max(1, b)] = [\min(1, \text{mulSingle}_i(b)), \max(1, \text{mulSingle}_i(b))]. \]

Set.pi_univ_Ioc_update_union theorem

 (x y : ∀ i, α i) (i₀ : ι) (m : α i₀) (hm : m ∈ Icc (x i₀) (y i₀)) :
  ((pi univ fun i ↦ Ioc (x i) (update y i₀ m i)) ∪ pi univ fun i ↦ Ioc (update x i₀ m i) (y i)) =
    pi univ fun i ↦ Ioc (x i) (y i)

Full source

theorem pi_univ_Ioc_update_union (x y : ∀ i, α i) (i₀ : ι) (m : α i₀) (hm : m ∈ Icc (x i₀) (y i₀)) :
    ((pi univ fun i ↦ Ioc (x i) (update y i₀ m i)) ∪
        pi univ fun i ↦ Ioc (update x i₀ m i) (y i)) =
      pi univ fun i ↦ Ioc (x i) (y i) := by
  simp_rw [pi_univ_Ioc_update_left hm.1, pi_univ_Ioc_update_right hm.2, ← union_inter_distrib_right,
    ← setOf_or, le_or_lt, setOf_true, univ_inter]

Decomposition of Product of Half-Open Intervals via Coordinate Update

Informal description

Let $\{α_i\}_{i \in \iota}$ be a family of preorders, and let $x, y \in \prod_{i \in \iota} α_i$. For any index $i_0 \in \iota$ and any element $m \in α_{i_0}$ such that $x_{i_0} \leq m \leq y_{i_0}$, the union of the following two product sets equals the product of intervals $\prod_{i \in \iota} (x_i, y_i]$: 1. The product $\prod_{i \in \iota} (x_i, y'_i]$, where $y'$ is $y$ with $y'_{i_0} = m$ 2. The product $\prod_{i \in \iota} (x'_i, y_i]$, where $x'$ is $x$ with $x'_{i_0} = m$ In symbols: $$ \left(\prod_{i \in \iota} (x_i, y'_i]\right) \cup \left(\prod_{i \in \iota} (x'_i, y_i]\right) = \prod_{i \in \iota} (x_i, y_i] $$ where $y' = \text{update } y i_0 m$ and $x' = \text{update } x i_0 m$.

Set.Icc_diff_pi_univ_Ioo_subset theorem

 (x y x' y' : ∀ i, α i) :
  (Icc x y \ pi univ fun i ↦ Ioo (x' i) (y' i)) ⊆
    (⋃ i : ι, Icc x (update y i (x' i))) ∪ ⋃ i : ι, Icc (update x i (y' i)) y

Full source

/-- 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 Icc_diff_pi_univ_Ioo_subset (x y x' y' : ∀ i, α i) :
    (Icc x y \ pi univ fun i ↦ Ioo (x' i) (y' i)) ⊆
    (⋃ i : ι, Icc x (update y i (x' i))) ∪ ⋃ i : ι, Icc (update x i (y' i)) y := by
  rintro a ⟨⟨hxa, hay⟩, ha'⟩
  simp only [mem_pi, mem_univ, mem_Ioo, true_implies, not_forall] at ha'
  simp only [le_update_iff, update_le_iff, mem_union, mem_iUnion, mem_Icc,
    hxa, hay _, hxa _, hay, ← exists_or]
  rcases ha' with ⟨w, hw⟩
  apply Exists.intro w
  cases lt_or_le (x' w) (a w) <;> simp_all

Covering of Closed Box Minus Open Box by Faces in Product Space

Informal description

Let $\{ \alpha_i \}_{i \in \iota}$ be a family of preordered types, and let $x, y, x', y' \in \prod_{i \in \iota} \alpha_i$ be functions. The set difference between the closed box $[x, y] = \{ z \mid \forall i, x_i \leq z_i \leq y_i \}$ and the product of open intervals $\prod_{i \in \iota} (x'_i, y'_i)$ is contained in the union of the following sets: for each $i \in \iota$, the closed boxes $[x, y']$ and $[x', y]$, where $y'$ is obtained by updating $y$ at $i$ to $x'_i$, and $x'$ is obtained by updating $x$ at $i$ to $y'_i$. In particular, if $x' = x$ and $y' = y$, this states that the difference between the closed box $[x, y]$ and the open box $\{ z \mid \forall i, x_i < z_i < y_i \}$ is covered by the union of the faces of $[x, y]$.

Set.Icc_diff_pi_univ_Ioc_subset theorem

(x y z : ∀ i, α i) : (Icc x z \ pi univ fun i ↦ Ioc (y i) (z i)) ⊆ ⋃ i : ι, Icc x (update z i (y i))

Full source

/-- 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`. -/
theorem Icc_diff_pi_univ_Ioc_subset (x y z : ∀ i, α i) :
    (Icc x z \ pi univ fun i ↦ Ioc (y i) (z i)) ⊆ ⋃ i : ι, Icc x (update z i (y i)) := by
  rintro a ⟨⟨hax, haz⟩, hay⟩
  simpa [not_and_or, hax, le_update_iff, haz _] using hay

Covering of the Difference Between a Closed Box and a Product of Half-Open Intervals

Informal description

Let $x, y, z$ be functions in $\Pi i : \iota, \alpha i$, where each $\alpha i$ is equipped with a preorder. The set difference between the closed box $[x, z]$ (defined as $\{w \mid \forall i, x i \leq w i \leq z i\}$) and the product of left-open right-closed intervals $\prod_{i} (y i, z i]$ is contained in the union of the closed boxes $[x, z']$, where $z'$ is obtained from $z$ by updating one coordinate at a time to $y i$ (i.e., $z' = \text{update } z i (y i)$ for some $i \in \iota$).