Shrinking an open set to separate part of a non-accumulating set

If every point of K ⊆ V avoids the closure of Z \ K, the open ambient set V shrinks to an open neighbourhood of K meeting Z in exactly K ∩ Z. This is the localization step for residue computations — a contour region is shrunk until the only singularities it contains are the intended ones.

Main declarations

• TauCeti.exists_isOpen_inter_eq_of_notMem_closure (with the accumulation-hypothesis corollary TauCeti.exists_isOpen_inter_eq_of_not_accPt).

theorem TauCeti.exists_isOpen_inter_eq_of_notMem_closure {X : Type u_1} [TopologicalSpace X] {V Z K : Set X} (hV : IsOpen V) (hKV : K ⊆ V) (hK : ∀ x ∈ K, x ∉ closure (Z \ K)) : ∃ (U : Set X), IsOpen U ∧ K ⊆ U ∧ U ⊆ V ∧ U ∩ Z = K ∩ Z

A set K ⊆ V whose points avoid the closure of Z \ K shrinks the open ambient V to an open neighbourhood meeting Z exactly in K ∩ Z: remove that closure.

theorem TauCeti.exists_isOpen_inter_eq_of_not_accPt {X : Type u_1} [TopologicalSpace X] {V Z K : Set X} (hV : IsOpen V) (hKV : K ⊆ V) (hacc : ∀ x ∈ K, ¬AccPt x (Filter.principal Z)) : ∃ (U : Set X), IsOpen U ∧ K ⊆ U ∧ U ⊆ V ∧ U ∩ Z = K ∩ Z

The separation under the stronger hypothesis that no point of K is an accumulation point of Z at all.