Set.PairwiseDisjoint.biUnion_finset

theorem Set.PairwiseDisjoint.biUnion_finset : ∀ {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] {s : Set ι'} {g : ι' → Finset ι} {f : ι → α}, (s.PairwiseDisjoint fun i' => (g i').sup f) → (∀ i ∈ s, (↑(g i)).PairwiseDisjoint f) → (⋃ i ∈ s, ↑(g i)).PairwiseDisjoint f

This theorem states that in the context of a complete lattice, and given three types `α`, `ι`, and `ι'`, a set `s` of type `ι'`, a function `g` from `ι'` to `Finset ι`, and a function `f` from `ι` to `α`, if two conditions are met then the union of the images under `g` of the elements in `s` is pairwise disjoint under `f`. The two conditions are: first, `s` is pairwise disjoint under the supremum of `f` over the image of `g`; second, for all elements in `s`, the image under `g` is pairwise disjoint under `f`. In less formal terms, this theorem tells us that if we can't find two different elements in `s` that have overlapping images under `g` when we apply the function `f`, and each collection of elements resulting from applying `g` to any element of `s` doesn't have overlapping elements under `f`, then there's no overlap under `f` when we apply `g` to every element in `s` and take the union.

More concisely: In a complete lattice, if a set `s` of type `ι'` is pairwise disjoint under the supremum of a function `f` from `ι` to `α` over `g(s)`, and each image `g(x)` of an element `x` in `s` is pairwise disjoint under `f`, then the images of `s` under `g` have pairwise disjoint images under `f` when taken as sets in `α`.