English
If i ∈ s, then updating i changes the Pi-set to the intersection with { x | x_i ∈ t_i a } and the rest.
Русский
Если i ∈ s, обновление i изменяет Pi-множество на пересечение с { x | x_i ∈ t_i(a) } и оставшееся множество.
LaTeX
$$$ (s.\pi (\lambda j, t j (\mathrm{update} f i a j))) = \{ x \mid x_i \in t_i a \} \cap (s \setminus \{ i \}).\pi (\lambda j, t j (f j)) $$$
Lean4
theorem pi_update_of_mem [DecidableEq ι] (hi : i ∈ s) (f : ∀ j, α j) (a : α i) (t : ∀ j, α j → Set (β j)) :
(s.pi fun j => t j (update f i a j)) = {x | x i ∈ t i a} ∩ (s \ { i }).pi fun j => t j (f j) :=
calc
(s.pi fun j => t j (update f i a j)) = ({ i } ∪ s \ { i }).pi fun j => t j (update f i a j) := by
rw [union_diff_self, union_eq_self_of_subset_left (singleton_subset_iff.2 hi)]
_ = {x | x i ∈ t i a} ∩ (s \ { i }).pi fun j => t j (f j) := by
rw [union_pi, singleton_pi', update_self, pi_update_of_notMem]; simp
