image_biUnion_filter_eq — Mathlib

English

Applying filter inside the biUnion with a predicate g yields a simple expression: (s.image g).biUnion (λ a, s.filter (λ c, g c = a)) = s.

Русский

Фильтр в BiUnion через предикат g превращается в равенство к исходному множеству: (s.image g).biUnion (λ a, s.filter (λ c, g c = a)) = s.

LaTeX

$$$((s.image g).biUnion (\\lambda a. s.filter (\\lambda c. g c = a))) = s$$$

Lean4

theorem image_biUnion_filter_eq [DecidableEq α] (s : Finset β) (g : β → α) :
    ((s.image g).biUnion fun a => s.filter fun c => g c = a) = s :=
  biUnion_filter_eq_of_maps_to fun _ => mem_image_of_mem g

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