English
Updating at i over the universal index set gives an intersection with the Pi-set over the complement of {i}.
Русский
Обновление по i над вселенским множеством приводит к пересечению с Pi-множество над сопряжением {i}.
LaTeX
$$$ \pi \mathrm{univ} (\lambda j, t j (\mathrm{update} f i a j)) = \{ x \mid x_i \in t_i a \} \cap \pi \{ i \}^{c} (\lambda j, t j (f j)) $$$
Lean4
theorem univ_pi_update [DecidableEq ι] {β : ι → Type*} (i : ι) (f : ∀ j, α j) (a : α i) (t : ∀ j, α j → Set (β j)) :
(pi univ fun j => t j (update f i a j)) = {x | x i ∈ t i a} ∩ pi { i }ᶜ fun j => t j (f j) := by
rw [compl_eq_univ_diff, ← pi_update_of_mem (mem_univ _)]
