English
If I is a finite set and f assigns to each i in I a finite set of β, then the union of all these sets across the two-level disjoint union equals the iterated union: the union over a in I of the union over elements of f(a).
Русский
Пусть I — конечное множество и для каждого i∈I задано множество f(i) ⊆ β. Тогда объединение по двум этапам равно повторному поэлементному объединению: ∪_{i∈I} ∪ f(i).
LaTeX
$$$\\bigcup\\limits_{X \\in (I.disjiUnion f\\ hf)} X = \\bigcup\\limits_{a \\in I} \\bigcup\\limits_{X \\in f(a)} X$$$
Lean4
theorem sUnion_disjiUnion {f : α → Finset (Set β)} (I : Finset α) (hf : (I : Set α).PairwiseDisjoint f) :
⋃₀ (I.disjiUnion f hf : Set (Set β)) = ⋃ a ∈ I, ⋃₀ ↑(f a) :=
by
ext
simp only [coe_disjiUnion, Set.mem_sUnion, Set.mem_iUnion, mem_coe, exists_prop]
tauto
