biUnion_filter_eq_of_maps_to — Mathlib

English

If f maps s into t, then the big union over t of the preimages of a equals s: t.biUnion (λ a, s.filter (λ c, f c = a)) = s.

Русский

Если отображение f отображает s в t, то сумма по t по предобразам даёт обратно s: t.biUnion (λ a, s.filter (λ c, f c = a)) = s.

LaTeX

$$$\\forall s:\\mathrm{Finset}(\\alpha),\\;\\forall t:\\mathrm{Finset}(\\beta),\\forall f:\\alpha\\to\\beta,\\ (\\forall x\\in s, f(x)\\in t)\\Rightarrow t.biUnion (\\lambda a. s.filter (\\lambda c. f c = a)) = s$$$

Lean4

theorem biUnion_filter_eq_of_maps_to [DecidableEq α] {s : Finset α} {t : Finset β} {f : α → β} (h : ∀ x ∈ s, f x ∈ t) :
    (t.biUnion fun a ↦ s.filter fun c ↦ f c = a) = s := by grind

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