English
Let x and y be functions indexed by i, with i0 ∈ ι and m ∈ Icc(x_i0, y_i0). Then the product set of Ioc slices over all i decomposes as the union of two families, one with the i0-th coordinate updated from y to m and the other with the i0-th coordinate updated from x to m; together these cover the whole product Ioc region between x and y.
Русский
Пусть x,y — функции, индексируемые по i; выберем i0 и m ∈ Icc(x_i0, y_i0). Тогда произведение множеств Ioc по всем i распадается на две семейства: одно с обновлением i0-й координаты в y до m, другое — с обновлением i0-й координаты в x до m; вместе они покрывают всю область Ioc между x и y.
LaTeX
$$$\big(\pi\operatorname{univ} i \mapsto \mathrm{Ioc}(x_i, \mathrm{update}\, y\, i_0\, m\, i)\big) \cup\big(\pi\operatorname{univ} i \mapsto \mathrm{Ioc}(\mathrm{update}\, x\, i_0\, m\, i, y_i)\big) = \pi\operatorname{univ} i \mapsto \mathrm{Ioc}(x_i, y_i).$$$
Lean4
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_gt, setOf_true, univ_inter]
