English
The image of a biUnion distributes over the inner image: (s.biUnion t).image f = s.biUnion (λ a, (t a).image f).
Русский
Образ BiUnion распределяется над внутренним образом: (s.biUnion t).image f = s.biUnion (λ a, (t a).image f).
LaTeX
$$$\\bigl(s.biUnion t\\bigr).image f = s.biUnion (\\lambda a. (t a).image f)$$$
Lean4
theorem biUnion_image [DecidableEq γ] {s : Finset α} {t : α → Finset β} {f : β → γ} :
(s.biUnion t).image f = s.biUnion fun a => (t a).image f :=
haveI := Classical.decEq α
Finset.induction_on s rfl fun a s _ ih => by simp only [biUnion_insert, image_union, ih]