English
For functions x,y,x',y' indexed by i, the set difference between the closed box [x,y] and the product of open intervals (x'i, y'i) is contained in the union of two families of boxes, one obtained by updating the upper bounds y and the other by updating the lower bounds x.
Русский
Для функций x,y,x',y' разного индекса i разность между замкнутым коробом [x,y] и произведением открытых интервалов (x'i, y'i) содержится в объединении двух семейств коробок, полученных обновлением верхних и нижних границ.
LaTeX
$$$(Icc\;x\;y) \setminus (\pi univ i \mapsto Ioo(x'_i, y'_i)) \subset (\bigcup_i Icc\, x\,(update\ y\, i\, (x'_i))) \cup (\bigcup_i Icc\,(update\ x\, i\, (y'_i))\, y).$$$
Lean4
/-- 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_ge (x' w) (a w) <;> simp_all
