English
disjiUnion s f h is the set of elements that belong to some f(i) with i ∈ s; equivalently, a disjoint union of the family f indexed by s.
Русский
disjiUnion s f h — множество элементов, принадлежащих некоторому f(i) при i∈s; это дизjoint union семейства f,(индиксируемого по s).
LaTeX
$$$ disjiUnion\\ s\\ f\\ h = \\{ \\text{union over } i \\in s\\, f(i) \\}$ (with pairwise disjointness hypothesis)$$
Lean4
/-- `disjiUnion s f h` is the set such that `a ∈ disjiUnion s f` iff `a ∈ f i` for some `i ∈ s`.
It is the same as `s.biUnion f`, but it does not require decidable equality on the type. The
hypothesis ensures that the sets are disjoint. -/
def disjiUnion (s : Finset α) (t : α → Finset β) (hf : (s : Set α).PairwiseDisjoint t) : Finset β :=
⟨s.val.bind (Finset.val ∘ t),
Multiset.nodup_bind.2 ⟨fun a _ ↦ (t a).nodup, s.nodup.pairwise fun _ ha _ hb hab ↦ disjoint_val.2 <| hf ha hb hab⟩⟩
