English
Let l be a nodup list of indices that contains every index i, and assign to each i a set t_i. Then the preimage under the elimination map of the universal product equals the product over the list l of the t_i.
Русский
Пусть l — список без повторов индексов, содержащий каждый индекс i, и для каждого i задано множество t_i. Тогда предобраз под изображением элиминации от универсального произведения равен произведению по списку l множеств t.
LaTeX
$$$$(\\mathrm{TProd.elim}'(h))^{-1}(\\pi_{\\mathrm{univ}}\\ t) = \\mathrm{tprod}_l\\ t.$$$$
Lean4
theorem elim_preimage_pi [DecidableEq ι] {l : List ι} (hnd : l.Nodup) (h : ∀ i, i ∈ l) (t : ∀ i, Set (α i)) :
TProd.elim' h ⁻¹' pi univ t = Set.tprod l t :=
by
have h2 : {i | i ∈ l} = univ := by
ext i
simp [h]
rw [← h2, ← mk_preimage_tprod, preimage_preimage]
simp only [TProd.mk_elim hnd h]
dsimp
