Theorems · Definition · combinatorics

Finset.disjiUnion

{α : Type u_1} → {β : Type u_2} → (s : Finset α) → (t : α → Finset β) → (↑s).PairwiseDisjoint t → Finset β

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.

Defined in

Mathlib.Data.Finset.Union

Cited by

37 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound