English
Let s be a finite index set and for each a in s let f(a) be a finite set of β and for each b in f(a) let g(b) be a finite set of γ. Under the usual disjointness hypotheses, the iterated disjoint union can be regrouped as a single disjoint union indexed by elements of s, where each fibre is the disjoint union of f(a) with g.
Русский
Пусть s — конечное множество‑индекс, для каждого a∈s дано множество f(a) ⊆ β и для каждого b∈f(a) дано множество g(b) ⊆ γ. При обычных предположениях о попарной непересичаемости, повторяющееся объединение по disjiUnion можно перестроить в одно объединение, индексированное по элементам s, где каждая волоконная часть равна f(a) disjiUnion g.
LaTeX
$$$(s.disjiUnion f\,h_1).disjiUnion g\,h_2 = s.attach.disjiUnion\\Bigl( a \\mapsto (f(a).disjiUnion g) \\Bigr)\\Bigl( \\text{with the appropriate disjointness provided by }h_2 \\Bigr)$$$
Lean4
theorem disjiUnion_disjiUnion (s : Finset α) (f : α → Finset β) (g : β → Finset γ) (h1 h2) :
(s.disjiUnion f h1).disjiUnion g h2 =
s.attach.disjiUnion
(fun a ↦
((f a).disjiUnion g) fun _ hb _ hc ↦
h2 (mem_disjiUnion.mpr ⟨_, a.prop, hb⟩) (mem_disjiUnion.mpr ⟨_, a.prop, hc⟩))
fun a _ b _ hab ↦
disjoint_left.mpr fun x hxa hxb ↦
by
obtain ⟨xa, hfa, hga⟩ := mem_disjiUnion.mp hxa
obtain ⟨xb, hfb, hgb⟩ := mem_disjiUnion.mp hxb
refine
disjoint_left.mp (h2 (mem_disjiUnion.mpr ⟨_, a.prop, hfa⟩) (mem_disjiUnion.mpr ⟨_, b.prop, hfb⟩) ?_) hga hgb
rintro rfl
exact disjoint_left.mp (h1 a.prop b.prop <| Subtype.coe_injective.ne hab) hfa hfb :=
eq_of_veq <| Multiset.bind_assoc.trans (Multiset.attach_bind_coe _ _).symm
