English
For x,y: ∀ i, α i and i0 ∈ ι, m ∈ α i0 with m ≤ y i0, the pi-univ image of Ioc(x i, update y i0 m i) equals the intersection of {z | z i0 ≤ m} with the pi-univ image of Ioc(x i, y i).
Русский
Для x,y: ∀ i α i и i0, m ∈ α i0 с m ≤ y i0, образ Ioc(x i, update y i0 m i) равен пересечению множества {z | z_{i0} ≤ m} с образом Ioc(x i, y i).
LaTeX
$$$$ (\pi univ\; (\lambda i. Ioc(x i, update y i0 m i))) = \{ z \mid z_{i0} \le m \} \cap (\pi univ\; (\lambda i. Ioc(x i, y i))) $$$$
Lean4
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} ∩ pi univ fun i ↦ Ioc (x i) (y i) :=
by
have : Ioc (x i₀) m = Iic 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
