ClosureOverlap

Supporting results for the classification of compact one-dimensional manifolds.

theorem OneMfld.nonempty_closure_inter_diff {X : Type u} [TopologicalSpace X] {U V : Set X} (hVconn : IsConnected V) (hUopen : IsOpen U) (hVopen : IsOpen V) (hUV : (U ∩ V).Nonempty) (hVU : (V \ U).Nonempty) : (closure U ∩ (V \ U)).Nonempty