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