English
Let s(a) be a family of index sets and t(a, ·) a family of sets depending on a. Then the union over all choices of indices x with x(a) ∈ s(a) for every a, of the Cartesian products ∏_a t(a)(x(a)), equals the Cartesian product over a of the unions over j ∈ s(a) of t(a)(j).
Русский
Пусть s(a) задаёт для каждого a множество индексов, а t(a, j) задаёт множество, зависящее от a и индекса j. Тогда объединение по всем выборкам x с x(a) ∈ s(a) для каждого a от произведений по a из t(a)(x(a)) равно произведению по a от объединений по j ∈ s(a) из t(a)(j).
LaTeX
$$$$\\bigcup_{x \\in \\mathrm{univ}.\\pi s} \\prod_{a} t(a)(x(a)) = \\prod_{a} \\Big(\\bigcup_{j \\in s(a)} t(a)(j)\\Big).$$$$
Lean4
theorem biUnion_univ_pi {ι : α → Type*} (s : (a : α) → Set (ι a)) (t : (a : α) → ι a → Set (π a)) :
⋃ x ∈ univ.pi s, pi univ (fun a => t a (x a)) = pi univ fun a => ⋃ j ∈ s a, t a j :=
by
ext
simp [Classical.skolem, forall_and]
