Finset induction for set-indexed additivity: generalize the ambient set

To prove finite additivity deg(F, Ω) = ∑ i ∈ s, deg(F, U i) from the two-set lemma deg Ω = deg Ω₁ + deg Ω₂, use induction s using Finset.induction_on generalizing Ω. In the insert a s step, take Ω₁ = U a and Ω₂ = V := ⋃ i ∈ s, U i, and apply the induction hypothesis with Ω := V. The admissibility side condition for V comes from two facts. First, frontier V misses V because V is open. Second, frontier V misses U a, by (hdisj.symm.closure_left hUa).ne_of_mem (open sets disjoint from V are disjoint from closure V). Disjointness of U a from V is Set.disjoint_iUnion₂_right.2. The pairwise-disjoint hypothesis restricts with hdisj.subset (by simp). Generalizing Ω is the key move. Without it the IH talks about the wrong ambient domain and nothing closes.