English
Let r be a relation between α and β. For a finite set s of indices and a family f assigning to each index an α-set, the edges from the union over s to t equal the union over s of the edges from each f(a) to t.
Русский
Пусть r — relation между α и β. Пусть s — конечное множество индексов, а f: индексы → Finset α. Рёбра между объединением ⋃_{a∈s} f(a) и t совпадают с объединением по a∈s ребер между f(a) и t.
LaTeX
$$$\operatorname{interedges}(r, \bigcup_{a\in s} f(a), t) = \bigcup_{a\in s} \operatorname{interedges}(r, f(a), t)$$$
Lean4
theorem interedges_biUnion_left (s : Finset ι) (t : Finset β) (f : ι → Finset α) :
interedges r (s.biUnion f) t = s.biUnion fun a ↦ interedges r (f a) t :=
by
ext
simp only [mem_biUnion, mem_interedges_iff, exists_and_right, ← and_assoc]
