English
Let s be a finite index set, t a finite set, and f a map from the index to the base type. The disjoint union of the fibers s.filter (f · = a) over a with pairwise disjoint fibers equals t filtered to those a that match f.
Русский
Пусть s — конечное множество, t — конечное множество β, f — α→β. Дисjoint‑объединение волокон, отфильтрованных по равенству f a, эквивалентно фильтрации по соответствующим условиям.
LaTeX
$$$t.disjiUnion (\\lambda a \\mapsto s.filter (f \\cdot = a)) \\text{ pairwiseDisjoint_fibers } = s.filter (\\lambda c \\mapsto f c \\in t)$$$
Lean4
@[simp]
theorem disjiUnion_filter_eq (s : Finset α) (t : Finset β) (f : α → β) :
t.disjiUnion (fun a ↦ s.filter (f · = a)) pairwiseDisjoint_fibers = s.filter fun c ↦ f c ∈ t :=
ext fun b => by simpa using and_comm
