English
For a fixed i, the preimage of the i-th evaluation map on a set s equals the product pi univ with the i-th coordinate restricted to s via update.
Русский
Для фиксированного i предобраз отображения оценки в i-й координате на множество s равен произведению, где i-я координата ограничена до s через обновление.
LaTeX
$$$$ \\operatorname{preimage}(\\operatorname{eval}_i)(s) = \\pi\\mathrm{univ}\\, (\\operatorname{update}(\\lambda _,.\\, \\mathrm{univ}) i s). $$$$
Lean4
theorem eval_preimage [DecidableEq ι] {s : Set (α i)} : eval i ⁻¹' s = pi univ (update (fun _ => univ) i s) :=
by
ext x
simp [@forall_update_iff _ (fun i => Set (α i)) _ _ _ _ fun i' y => x i' ∈ y]
