Path-connected pairwise intersections #
If every member of a family of path-connected sets contains a path-connected set C, and two
distinct members meet inside C, then every pairwise intersection of the family is path
connected: it is a member of the family or C itself. This is the hypothesis on pairwise
intersections in the generation half of the Seifert--van Kampen theorem, and the form in which it
holds for the summands of a wedge sum.
Main declarations #
TauCeti.isPathConnected_inter_of_pairwise: pairwise intersections of such a family are path connected.
theorem
TauCeti.isPathConnected_inter_of_pairwise
{X : Type u_1}
[TopologicalSpace X]
{ι : Type u_2}
{U : ι → Set X}
{C : Set X}
(hUp : ∀ (i : ι), IsPathConnected (U i))
(hC : IsPathConnected C)
(hCU : ∀ (i : ι), C ⊆ U i)
(hUC : Pairwise fun (i j : ι) => U i ∩ U j ⊆ C)
(i j : ι)
:
IsPathConnected (U i ∩ U j)
If every member of the family contains C and two distinct members meet inside C, then
every pairwise intersection is path connected as soon as C and the members are.