image_biUnion — Mathlib

English

Applying image after biUnion commutes: (s.image f).biUnion t = s.biUnion (λ a, t (f a)).

Русский

Применение образа после BiUnion совместимо: (s.image f).biUnion t = s.biUnion (λ a, t (f a)).

LaTeX

$$$\\bigl(s\\image f\\bigr)\\biUnion t = s.biUnion \\bigl(\\lambda a. t(f(a))\\bigr)$$$

Lean4

theorem image_biUnion [DecidableEq γ] {f : α → β} {s : Finset α} {t : β → Finset γ} :
    (s.image f).biUnion t = s.biUnion fun a => t (f a) :=
  haveI := Classical.decEq α
  Finset.induction_on s rfl fun a s _ ih => by simp only [image_insert, biUnion_insert, ih]

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