English
For a family a : ι → α_i, i ∈ ι, and b ∈ α_i, we have: update a i b ∈ pi s t iff a ∈ pi (s \\ {i}) t ∧ (i ∈ s → b ∈ t_i).
Русский
Для функции a и элемента b в координате i имеем: обновление a в координате i до b принадлежит π s t тогда и только тогда, когда исходная функция a принадлежит π (s \\ {i}) t и если i ∈ s, то b ∈ t_i.
LaTeX
$$$$ \\ update\\ a\\ i\\ b \\in \\pi s t \\iff a \\in \\pi (s \\setminus \\{i\\}) t \\wedge (i \\in s \\rightarrow b \\in t_i). $$$$
Lean4
theorem update_mem_pi_iff [DecidableEq ι] {a : ∀ i, α i} {i : ι} {b : α i} :
update a i b ∈ pi s t ↔ a ∈ pi (s \ { i }) t ∧ (i ∈ s → b ∈ t i) :=
by
constructor
· grind [update_self, update_of_ne]
· rintro h j
cases eq_or_ne i j <;> grind [update_self, update_of_ne]
