English
Let β be finite and f: β → Set α with each f(b) finite. Then the Finset corresponding to the union ⋃_{x ∈ β} f(x) equals the biUnion of the Finsets (f(x)).toFinset over x.
Русский
Пусть β конечно, и f: β → Set α, причём каждая f(b) конечна. Тогда Finset-обозначение объединения ⋃_{x ∈ β} f(x) равно би-объединению Finset-объединений (f(x)).toFinset по x.
LaTeX
$$$\\operatorname{toFinset}\\left(\\bigcup_{x \\in \\beta} f(x)\\right) = \\operatorname{Finset.biUnion}\\left(\\operatorname{Finset.univ}, \\lambda x, (f(x)).toFinset\\right)$$$
Lean4
theorem toFinset_iUnion [Fintype β] [DecidableEq α] (f : β → Set α) [∀ w, Fintype (f w)] :
Set.toFinset (⋃ (x : β), f x) = Finset.biUnion (Finset.univ : Finset β) (fun x => (f x).toFinset) :=
by
ext v
simp only [mem_toFinset, mem_iUnion, Finset.mem_biUnion, Finset.mem_univ, true_and]
