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