Preconnected sets: disjoint open covers and compact injective images

A preconnected set covered by a family of pairwise disjoint open sets lies in each member of the family that it meets. This is the form in which connectedness is used to show that a region contained in a union of disjoint open cells lies in a single cell.

Dually, when a preconnected set is the union of a locally finite family of closed sets, any two nonempty members are joined by a chain of members in which consecutive sets meet (IsPreconnected.transGen_of_iUnion_of_isClosed). For instance, the irreducible components of a connected Noetherian space form a connected intersection graph.

The same principle selects a limit: a function which tends to a finite subset of a Hausdorff space along a filter in which arbitrarily small sets have preconnected images tends to a single point of that subset (Filter.Tendsto.exists_mem_tendsto_nhds). For instance, near a point whose punctured neighbourhoods are connected, a continuous function approaching a finite set chooses one of its points.

An open set is not preconnected exactly when it is the union of two disjoint nonempty open sets (IsOpen.not_isPreconnected_iff), as for clopen sets in Mathlib.

A continuous injection on a compact set into a Hausdorff space is a closed embedding of that set, so preconnectedness of the image is equivalent to preconnectedness of the set (IsCompact.isPreconnected_image_iff_of_injOn).

A continuous function on a preconnected set that is locally constant near each point where it takes a given value f z, for some z in the set, is constant (IsPreconnected.eqOn_const_of_eventually_eq). This is how a strong maximum principle spreads from a neighbourhood of a maximum point to the whole domain.

In a T₁ space, the connected component connectedComponentIn s x of a point isolated in s is the point itself (TauCeti.connectedComponentIn_eq_singleton): the component is covered by the open sets {x}ᶜ and a neighbourhood of x meeting s only at x, whose intersection misses s.

theorem IsPreconnected.subset_of_subset_iUnion {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] {s : Set α} {u : ι → Set α} (hs : IsPreconnected s) (hu : ∀ (i : ι), IsOpen (u i)) (hdisj : Pairwise (Function.onFun Disjoint u)) (hsu : s ⊆ ⋃ (i : ι), u i) {i : ι} (hsi : (s ∩ u i).Nonempty) : s ⊆ u i

A preconnected set covered by pairwise disjoint open sets u i lies in each u i that it meets.

theorem IsPreconnected.transGen_of_iUnion_of_isClosed {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] {s : ι → Set α} (hf : LocallyFinite s) (hs : IsPreconnected (⋃ (n : ι), s n)) (hs' : ∀ (i : ι), IsClosed (s i)) (i j : ι) (hi : (s i).Nonempty) (hj : (s j).Nonempty) : Relation.TransGen (fun (a b : ι) => (s a ∩ s b).Nonempty) i j

If the union of a locally finite family of closed sets s i is preconnected, any two nonempty members are joined by a chain of members in which consecutive sets meet. This is the closed counterpart of Mathlib's IsPreconnected.transGen_of_iUnion for open sets; local finiteness makes the unions of subfamilies closed.

theorem IsPreconnected.eqOn_const_of_eventually_eq {α : Type u_1} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] [T1Space β] {U : Set α} {f : α → β} {z : α} (hU : IsPreconnected U) (hz : z ∈ U) (hf : ∀ x ∈ U, ContinuousAt f x) (hlocal : ∀ x ∈ U, f x = f z → ∀ᶠ (y : α) in nhds x, f y = f z) : Set.EqOn f (Function.const α (f z)) U

Local constancy at a value spreads over a preconnected set. Let f be continuous at each point of a preconnected set U and z ∈ U. If f is identically f z near every point of U at which it takes the value f z, then f = f z on all of U.

theorem IsOpen.not_isPreconnected_iff {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsOpen s) : ¬IsPreconnected s ↔ ∃ (a : Set α) (b : Set α), IsOpen a ∧ IsOpen b ∧ a.Nonempty ∧ b.Nonempty ∧ Disjoint a b ∧ s = a ∪ b

An open set is not preconnected exactly when it is the union of two disjoint nonempty open sets.

theorem TauCeti.connectedComponentIn_eq_singleton {α : Type u_1} [TopologicalSpace α] [T1Space α] {s : Set α} {x : α} (hx : x ∈ s) (hiso : ∀ᶠ (z : α) in nhds x, z ∈ s → z = x) : connectedComponentIn s x = {x}

In a T₁ space, a point isolated in a set s is its own connected component in s.

theorem Filter.Tendsto.exists_mem_tendsto_nhds {α : Type u_1} [TopologicalSpace α] {β : Type u_3} [T2Space α] {f : β → α} {l : Filter β} [l.NeBot] {S : Set α} (hS : S.Finite) (hf : Tendsto f l (nhdsSet S)) (hl : ∀ s ∈ l, ∃ t ∈ l, t ⊆ s ∧ IsPreconnected (f '' t)) : ∃ y ∈ S, Tendsto f l (nhds y)

A function tending to a finite subset S of a Hausdorff space along a nontrivial filter l tends to a single point of S, provided every set of l contains a set of l with preconnected image.

theorem IsCompact.isPreconnected_image_iff_of_injOn {α : Type u_1} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] [T2Space β] {f : α → β} {K : Set α} (hK : IsCompact K) (hf : ContinuousOn f K) (hinj : Set.InjOn f K) : IsPreconnected (f '' K) ↔ IsPreconnected K

Preconnectedness pulls back along a continuous injection on a compact set. If f is continuous and injective on a compact K with values in a Hausdorff space, then f '' K is preconnected exactly when K is.

theorem TauCeti.reflTransGen_inter_nonempty_of_isOpen_cover {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] {t : Set ι} {V : ι → Set α} (hU : IsPreconnected (⋃ i ∈ t, V i)) (hV : ∀ i ∈ t, IsOpen (V i)) {i₀ : ι} (hi₀ : i₀ ∈ t) (hVi₀ : (V i₀).Nonempty) {j : ι} (hj : j ∈ t) (hVj : (V j).Nonempty) : Relation.ReflTransGen (fun (i j : ι) => i ∈ t ∧ j ∈ t ∧ (V i ∩ V j).Nonempty) i₀ j

Chains of overlaps in a connected open cover. If the union of the open sets V i, i ∈ t, is preconnected, every nonempty V j is joined to a nonempty piece V i₀ by a chain of pairwise overlapping pieces.