English
The image of an updated function under a single coordinate equals the universal product of single-coordinate images.
Русский
Образ обновления функции по одной координате равен универсльному произведению образов по координатам.
LaTeX
$$$$ \\mathrm{image}(\\mathrm{update} \\ x \\ i)(s) = \\mathrm{univ} \\pi (\\mathrm{update}(\\lambda j. \\{x_j\\}) i s). $$$$
Lean4
theorem update_image [DecidableEq ι] (x : (i : ι) → β i) (i : ι) (s : Set (β i)) :
update x i '' s = Set.univ.pi (update (fun j ↦ {x j}) i s) :=
by
ext y
simp only [mem_image, update_eq_iff, ne_eq, and_left_comm (a := _ ∈ s), exists_eq_left, mem_pi, mem_univ,
true_implies]
rw [forall_update_iff (p := fun x s => y x ∈ s)]
simp [eq_comm]
