Shrinking a family of compact cores to open subsets avoiding finitely many closed sets

Point-set topology for the shrinking of the pieces in the gluing of local complexifications BW59, Proposition 1. Given spaces Y i, compact cores K i ⊆ Y i, a family S₂ of pairs (a, b) with closed sets E₂ (a, b) ⊆ Y a × Y b disjoint from K a × K b, and a family S₃ of triples with closed sets E₃ (a, b, c) ⊆ Y a × Y b × Y c disjoint from K a × K b × K c, such that every index meets only finitely many pairs and triples, there are open subsets A i ⊇ K i with A a × A b disjoint from E₂ (a, b) and A a × A b × A c disjoint from E₃ (a, b, c) (exists_shrink): the tube lemma for each constraint (Mathlib's generalized_tube_lemma), and finite intersections.

Conventions. The constraint open subsets are indexed so that no transport along an equality of indices is needed: for the index i the pairs (i, j) contribute their first open subsets, the pairs (j, i) their second, and likewise the three positions of the triples. With no constraints A i = univ; an empty K i may still be constrained by the other cores. Not in the sources.

The tube lemma as disjointness from a closed set

theorem AnalyticSpace.Glue.exists_isOpen_prod_disjoint {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} (hs : IsCompact s) (ht : IsCompact t) {E : Set (X × Y)} (hE : IsClosed E) (hd : Disjoint (s ×ˢ t) E) : ∃ (u : Set X) (v : Set Y), IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint (u ×ˢ v) E

theorem AnalyticSpace.Glue.exists_isOpen_prod3_disjoint {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {s : Set X} {t : Set Y} {r : Set Z} (hs : IsCompact s) (ht : IsCompact t) (hr : IsCompact r) {E : Set (X × Y × Z)} (hE : IsClosed E) (hd : Disjoint (s ×ˢ t ×ˢ r) E) : ∃ (u : Set X) (v : Set Y) (w : Set Z), IsOpen u ∧ IsOpen v ∧ IsOpen w ∧ s ⊆ u ∧ t ⊆ v ∧ r ⊆ w ∧ Disjoint (u ×ˢ v ×ˢ w) E

The shrinking

theorem AnalyticSpace.Glue.exists_shrink {ι : Type u} {Y : ι → Type v} [(i : ι) → TopologicalSpace (Y i)] (K : (i : ι) → Set (Y i)) (hK : ∀ (i : ι), IsCompact (K i)) (S₂ : Set (ι × ι)) (E₂ : (p : ι × ι) → Set (Y p.1 × Y p.2)) (hE₂ : ∀ p ∈ S₂, IsClosed (E₂ p)) (hK₂ : ∀ p ∈ S₂, Disjoint (K p.1 ×ˢ K p.2) (E₂ p)) (hfin₂ : ∀ (i : ι), {p : ι × ι | p ∈ S₂ ∧ (p.1 = i ∨ p.2 = i)}.Finite) (S₃ : Set (ι × ι × ι)) (E₃ : (t : ι × ι × ι) → Set (Y t.1 × Y t.2.1 × Y t.2.2)) (hE₃ : ∀ t ∈ S₃, IsClosed (E₃ t)) (hK₃ : ∀ t ∈ S₃, Disjoint (K t.1 ×ˢ K t.2.1 ×ˢ K t.2.2) (E₃ t)) (hfin₃ : ∀ (i : ι), {t : ι × ι × ι | t ∈ S₃ ∧ (t.1 = i ∨ t.2.1 = i ∨ t.2.2 = i)}.Finite) : ∃ (A : (i : ι) → Set (Y i)), (∀ (i : ι), IsOpen (A i)) ∧ (∀ (i : ι), K i ⊆ A i) ∧ (∀ p ∈ S₂, Disjoint (A p.1 ×ˢ A p.2) (E₂ p)) ∧ ∀ t ∈ S₃, Disjoint (A t.1 ×ˢ A t.2.1 ×ˢ A t.2.2) (E₃ t)

The shrinking. Open subsets A i ⊇ K i avoiding finitely many closed pair and triple constraints.