prod_eq_biUnion_left — Mathlib

English

Let f be a binary function and s_i_j, t: a double-indexed collection. Then image of the product s with t over a two-parameter index equals the iterated union over i and j of the image over s i j with t.

Русский

Пусть f — бинарная функция, а {s_{i,j}} и t — двухпараметрическая коллекция. Тогда образ произведения s с t по двум индексам равен повторяющемуся объединению по i и j образов image2 f (s_{i,j}) t.

LaTeX

$$$$ \\operatorname{image}_2 f (\\bigcup_{i} \\bigcup_{j} s_{i,j}) t = \\bigcup_{i} \\bigcup_{j} \\operatorname{image}_2 f (s_{i,j}) t $$$$

Lean4

theorem prod_eq_biUnion_left : s ×ˢ t = ⋃ a ∈ s, (fun b => (a, b)) '' t := by rw [iUnion_image_left, image2_mk_eq_prod]

Похожие утверждения