biUnion_image — Mathlib

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]

Похожие утверждения