Connected component of (A∩ B)ᶜ through a point of A∖ B
ProvedconnectedComponentIn_compl_inter_eq_of_isClosed_of_union_eq_univLet be a topological space and let be subsets, both assumed closed, whose union is all of . Assume further that the difference is preconnected, and let be a point of lying in , that is, and . The conclusion is an equality of subsets of : the connected component of inside the subset , in the sense of Mathlib's connectedComponentIn (the connected component of in the subspace , pushed forward to ), equals . Since is covered by and , this right-hand side is exactly ; the statement is phrased with the intersection with the complement rather than with the set difference.
An elementary point-set fact: when is the union of two closed sets and , the open set is the disjoint union of the relatively clopen pieces and , so a preconnected piece containing is the whole connected component of . It is used in the analysis of degenerations of a two-component fibre, where and are the two components and the locus away from their intersection: it is cited by ModularCurve.DRModelPackage.exists_twoLineDegeneration_of_not_smooth and ModularCurve.DRModelPackage.exists_twoLineDegeneration_of_not_smooth_iso_comp_eq.
import Mathlib set_option maxHeartbeats 4000000 set_option synthInstance.maxHeartbeats 400000 set_option backward.isDefEq.respectTransparency.types false set_option autoImplicit false
theorem connectedComponentIn_compl_inter_eq_of_isClosed_of_union_eq_univ
{X : Type*} [TopologicalSpace X] {A B : Set X} (hA : IsClosed A) (hB : IsClosed B)
(hAB : A ∪ B = Set.univ) (hA' : IsPreconnected (A \ B)) {e : X} (he : e ∈ A \ B) :
connectedComponentIn (A ∩ B)ᶜ e = A ∩ (A ∩ B)ᶜ := by sorry