English
The difference between the closed box [x,z] and the product of half-open intervals (y_i, z_i] is contained in the union of the boxes [x, update z_i(y_i)].
Русский
Разность между замкнутым коробом [x,z] и произведением полузакрытых интервалов (y_i, z_i] содержится в объединении коробок [x, обновление z_i(y_i)].
LaTeX
$$(Icc x z) \ (pi univ i \mapsto Ioc(y_i, z_i)) ⊆ ∪_{i} Icc x (update z i (y i)).$$
Lean4
/-- 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
