English
Let r be a relation between α and β. If you take unions on both sides, the edges between these unions decompose as a union over pairs (a,b) from s×t of edges between f(a) and g(b).
Русский
Пусть r — отношение между α и β. Если объединения берутся с обеих сторон, грани между этими объединениями раскладываются в объединение по всем парам (a,b) из s×t ребер между f(a) и g(b).
LaTeX
$$$\operatorname{interedges}(r, \bigcup_{a\in s} f(a), \bigcup_{b\in t} g(b)) = (s \times t)\ biUnion (\lambda ab\, , \operatorname{interedges}(r, f(ab.1), g(ab.2)))$$$
Lean4
theorem interedges_biUnion (s : Finset ι) (t : Finset κ) (f : ι → Finset α) (g : κ → Finset β) :
interedges r (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun ab ↦ interedges r (f ab.1) (g ab.2) := by
simp_rw [product_biUnion, interedges_biUnion_left, interedges_biUnion_right]
