Connected subsets and their relation to clopen sets

In this file we show how connected subsets of a topological space are intimately connected to clopen sets.

Main declarations

• IsClopen.biUnion_connectedComponent_eq: a clopen set is the union of its connected components.
• PreconnectedSpace.induction₂: an induction principle for preconnected spaces.
• ConnectedComponents: The connected components of a topological space, as a quotient type.

theorem IsPreconnected.subset_isClopen {α : Type u} [TopologicalSpace α] {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t) (hne : (s ∩ t).Nonempty) : s ⊆ t

Preconnected sets are either contained in or disjoint to any given clopen set.

theorem Sigma.isConnected_iff {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {s : Set ((i : ι) × X i)} : IsConnected s ↔ ∃ (i : ι) (t : Set (X i)), IsConnected t ∧ s = mk i '' t

theorem Sigma.isPreconnected_iff {ι : Type u_1} {X : ι → Type u_2} [hι : Nonempty ι] [(i : ι) → TopologicalSpace (X i)] {s : Set ((i : ι) × X i)} : IsPreconnected s ↔ ∃ (i : ι) (t : Set (X i)), IsPreconnected t ∧ s = mk i '' t

theorem Sum.isConnected_iff {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α ⊕ β)} : IsConnected s ↔ (∃ (t : Set α), IsConnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsConnected t ∧ s = inr '' t

theorem Sum.isPreconnected_iff {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α ⊕ β)} : IsPreconnected s ↔ (∃ (t : Set α), IsPreconnected t ∧ s = inl '' t) ∨ ∃ (t : Set β), IsPreconnected t ∧ s = inr '' t

theorem Continuous.exists_lift_sigma {α : Type u} {ι : Type u_1} {X : ι → Type u_2} [TopologicalSpace α] [ConnectedSpace α] [(i : ι) → TopologicalSpace (X i)] {f : α → (i : ι) × X i} (hf : Continuous f) : ∃ (i : ι) (g : α → X i), Continuous g ∧ f = Sigma.mk i ∘ g

A continuous map from a connected space to a disjoint union Σ i, X i can be lifted to one of the components X i. See also ContinuousMap.exists_lift_sigma for a version with bundled ContinuousMaps.

theorem nonempty_inter {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] {s t : Set α} : IsOpen s → IsOpen t → s ∪ t = Set.univ → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty

theorem isClopen_iff {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] {s : Set α} : IsClopen s ↔ s = ∅ ∨ s = Set.univ

theorem IsClopen.eq_univ {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] {s : Set α} (h' : IsClopen s) (h : s.Nonempty) : s = Set.univ

theorem isClopen_preimage_val {X : Type u_3} [TopologicalSpace X] {u v : Set X} (hu : IsOpen u) (huv : Disjoint (frontier u) v) : IsClopen (Subtype.val ⁻¹' u)

theorem subsingleton_of_disjoint_isClopen {α : Type u} {ι : Type u_1} [TopologicalSpace α] [PreconnectedSpace α] {s : ι → Set α} (h_nonempty : ∀ (i : ι), (s i).Nonempty) (h_disj : Pairwise (Function.onFun Disjoint s)) (h_clopen : ∀ (i : ι), IsClopen (s i)) : Subsingleton ι

In a preconnected space, any disjoint family of non-empty clopen subsets has at most one element.

theorem subsingleton_of_disjoint_isOpen_iUnion_eq_univ {α : Type u} {ι : Type u_1} [TopologicalSpace α] [PreconnectedSpace α] {s : ι → Set α} (h_nonempty : ∀ (i : ι), (s i).Nonempty) (h_disj : Pairwise (Function.onFun Disjoint s)) (h_open : ∀ (i : ι), IsOpen (s i)) (h_Union : ⋃ (i : ι), s i = Set.univ) : Subsingleton ι

In a preconnected space, any disjoint cover by non-empty open subsets has at most one element.

theorem subsingleton_of_disjoint_isClosed_iUnion_eq_univ {α : Type u} {ι : Type u_1} [TopologicalSpace α] [PreconnectedSpace α] {s : ι → Set α} (h_nonempty : ∀ (i : ι), (s i).Nonempty) (h_disj : Pairwise (Function.onFun Disjoint s)) [Finite ι] (h_closed : ∀ (i : ι), IsClosed (s i)) (h_Union : ⋃ (i : ι), s i = Set.univ) : Subsingleton ι

In a preconnected space, any finite disjoint cover by non-empty closed subsets has at most one element.

theorem frontier_eq_empty_iff {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] {s : Set α} : frontier s = ∅ ↔ s = ∅ ∨ s = Set.univ

theorem nonempty_frontier_iff {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] {s : Set α} : (frontier s).Nonempty ↔ s.Nonempty ∧ s ≠ Set.univ

theorem PreconnectedSpace.induction₂' {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] (P : α → α → Prop) (h : ∀ (x : α), ∀ᶠ (y : α) in nhds x, P x y ∧ P y x) (h' : IsTrans α P) (x y : α) : P x y

In a preconnected space, given a transitive relation P, if P x y and P y x are true for y close enough to x, then P x y holds for all x, y. This is a version of the fact that, if an equivalence relation has open classes, then it has a single equivalence class.

theorem PreconnectedSpace.induction₂ {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] (P : α → α → Prop) [Std.Symm P] (h : ∀ (x : α), ∀ᶠ (y : α) in nhds x, P x y) (h' : IsTrans α P) (x y : α) : P x y

In a preconnected space, if a symmetric transitive relation P x y is true for y close enough to x, then it holds for all x, y. This is a version of the fact that, if an equivalence relation has open classes, then it has a single equivalence class.

theorem IsPreconnected.induction₂' {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsPreconnected s) (P : α → α → Prop) (h : ∀ x ∈ s, ∀ᶠ (y : α) in nhdsWithin x s, P x y ∧ P y x) (h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : P x y

In a preconnected set, given a transitive relation P, if P x y and P y x are true for y close enough to x, then P x y holds for all x, y. This is a version of the fact that, if an equivalence relation has open classes, then it has a single equivalence class.

theorem IsPreconnected.induction₂ {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsPreconnected s) (P : α → α → Prop) (h : ∀ x ∈ s, ∀ᶠ (y : α) in nhdsWithin x s, P x y) (h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z) (h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : P x y

In a preconnected set, if a symmetric transitive relation P x y is true for y close enough to x, then it holds for all x, y. This is a version of the fact that, if an equivalence relation has open classes, then it has a single equivalence class.

theorem isPreconnected_iff_subset_of_disjoint {α : Type u} [TopologicalSpace α] {s : Set α} : IsPreconnected s ↔ ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

A set s is preconnected if and only if for every cover by two open sets that are disjoint on s, it is contained in one of the two covering sets.

theorem isConnected_iff_sUnion_disjoint_open {α : Type u} [TopologicalSpace α] {s : Set α} : IsConnected s ↔ ∀ (U : Finset (Set α)), (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) → (∀ u ∈ U, IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u

A set s is connected if and only if for every cover by a finite collection of open sets that are pairwise disjoint on s, it is contained in one of the members of the collection.

theorem disjoint_or_subset_of_isClopen {α : Type u} [TopologicalSpace α] {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t) : Disjoint s t ∨ s ⊆ t

Preconnected sets are either contained in or disjoint to any given clopen set.

theorem isPreconnected_iff_subset_of_disjoint_closed {α : Type u} [TopologicalSpace α] {s : Set α} : IsPreconnected s ↔ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

A set s is preconnected if and only if for every cover by two closed sets that are disjoint on s, it is contained in one of the two covering sets.

theorem isPreconnected_iff_subset_of_fully_disjoint_closed {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsClosed s) : IsPreconnected s ↔ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v

A closed set s is preconnected if and only if for every cover by two closed sets that are disjoint, it is contained in one of the two covering sets.

theorem IsClopen.isPreconnected_iff {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsClopen s) : IsPreconnected s ↔ ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b

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

theorem IsClopen.connectedComponent_subset {α : Type u} [TopologicalSpace α] {s : Set α} {x : α} (hs : IsClopen s) (hx : x ∈ s) : connectedComponent x ⊆ s

theorem connectedComponent_subset_iInter_isClopen {α : Type u} [TopologicalSpace α] {x : α} : connectedComponent x ⊆ ⋂ (Z : { Z : Set α // IsClopen Z ∧ x ∈ Z }), ↑Z

The connected component of a point is always a subset of the intersection of all its clopen neighbourhoods.

theorem IsClopen.biUnion_connectedComponent_eq {α : Type u} [TopologicalSpace α] {Z : Set α} (h : IsClopen Z) : ⋃ x ∈ Z, connectedComponent x = Z

A clopen set is the union of its connected components.

theorem IsClopen.biUnion_connectedComponentIn {X : Type u_3} [TopologicalSpace X] {u v : Set X} (hu : IsClopen (Subtype.val ⁻¹' u)) (huv₁ : u ⊆ v) : u = ⋃ x ∈ u, connectedComponentIn v x

If u v : Set X and u ⊆ v is clopen in v, then u is the union of the connected components of v in X which intersect u.

theorem IsClopen.connectedComponentIn_eq {α : Type u} [TopologicalSpace α] {U : Set α} (hU : IsClopen U) {x : α} (hx : x ∈ U) : connectedComponentIn U x = connectedComponent x

theorem Topology.IsCoinducing.isConnected_preimage_of_isClosed {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})) (hcl : IsCoinducing f) {t : Set β} (ht : IsClosed t) (ht' : IsConnected t) : IsConnected (f ⁻¹' t)

The preimage of a connected component is preconnected if the function has connected fibers and a subset is closed iff the preimage is.

@[deprecated Topology.IsCoinducing.isConnected_preimage_of_isClosed (since := "2026-04-01")]

theorem preimage_connectedComponent_connected {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})) (hcl : Topology.IsCoinducing f) (t : β) : IsConnected (f ⁻¹' connectedComponent t)

theorem Topology.IsCoinducing.preimage_connectedComponent {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : IsCoinducing f) (h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})) (a : α) : f ⁻¹' connectedComponent (f a) = connectedComponent a

theorem Topology.IsCoinducing.image_connectedComponent {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : IsCoinducing f) (h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})) (a : α) : f '' connectedComponent a = connectedComponent (f a)

@[implicit_reducible]

def connectedComponentSetoid (α : Type u_3) [TopologicalSpace α] : Setoid α

The setoid of connected components of a topological space

Equations

• connectedComponentSetoid α = { r := fun (x y : α) => connectedComponent x = connectedComponent y, iseqv := ⋯ }

def ConnectedComponents (α : Type u) [TopologicalSpace α] : Type u

The quotient of a space by its connected components

Equations

• ConnectedComponents α = Quotient (connectedComponentSetoid α)

def ConnectedComponents.mk {α : Type u} [TopologicalSpace α] : α → ConnectedComponents α

Coercion from a topological space to the set of connected components of this space.

Equations

• ConnectedComponents.mk = Quotient.mk''

@[implicit_reducible]

instance ConnectedComponents.instCoeTC {α : Type u} [TopologicalSpace α] : CoeTC α (ConnectedComponents α)

Equations

• ConnectedComponents.instCoeTC = { coe := ConnectedComponents.mk }

@[simp]

theorem ConnectedComponents.coe_eq_coe {α : Type u} [TopologicalSpace α] {x y : α} : mk x = mk y ↔ connectedComponent x = connectedComponent y

theorem ConnectedComponents.coe_ne_coe {α : Type u} [TopologicalSpace α] {x y : α} : mk x ≠ mk y ↔ connectedComponent x ≠ connectedComponent y

theorem ConnectedComponents.coe_eq_coe' {α : Type u} [TopologicalSpace α] {x y : α} : mk x = mk y ↔ x ∈ connectedComponent y

@[implicit_reducible]

instance ConnectedComponents.instInhabited {α : Type u} [TopologicalSpace α] [Inhabited α] : Inhabited (ConnectedComponents α)

Equations

• ConnectedComponents.instInhabited = { default := ConnectedComponents.mk default }

@[implicit_reducible]

instance ConnectedComponents.instTopologicalSpace {α : Type u} [TopologicalSpace α] : TopologicalSpace (ConnectedComponents α)

Equations

• ConnectedComponents.instTopologicalSpace = { IsOpen := ConnectedComponents.instTopologicalSpace._aux_1, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

theorem ConnectedComponents.surjective_coe {α : Type u} [TopologicalSpace α] : Function.Surjective mk

theorem ConnectedComponents.isQuotientMap_coe {α : Type u} [TopologicalSpace α] : Topology.IsQuotientMap mk

theorem ConnectedComponents.continuous_coe {α : Type u} [TopologicalSpace α] : Continuous mk

@[simp]

theorem ConnectedComponents.range_coe {α : Type u} [TopologicalSpace α] : Set.range mk = Set.univ

theorem ConnectedComponents.nonempty_iff_nonempty {α : Type u} [TopologicalSpace α] : Nonempty (ConnectedComponents α) ↔ Nonempty α

instance ConnectedComponents.instNonempty {α : Type u} [TopologicalSpace α] [Nonempty α] : Nonempty (ConnectedComponents α)

theorem ConnectedComponents.isEmpty_iff_isEmpty {α : Type u} [TopologicalSpace α] : IsEmpty (ConnectedComponents α) ↔ IsEmpty α

instance ConnectedComponents.subsingleton {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] : Subsingleton (ConnectedComponents α)

noncomputable def ConnectedComponents.equivOfIsClopen {α : Type u} [TopologicalSpace α] {ι : Type u_3} {U : ι → Set α} (hclopen : ∀ (i : ι), IsClopen (U i)) (hdisj : Pairwise (Function.onFun Disjoint U)) (hunion : ⋃ (i : ι), U i = Set.univ) : ConnectedComponents α ≃ (i : ι) × ConnectedComponents ↑(U i)

A pairwise disjoint cover by clopens partitions the connected components.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConnectedComponents.equivOfIsClopen_symm_mk {α : Type u} [TopologicalSpace α] {ι : Type u_3} {U : ι → Set α} (hclopen : ∀ (i : ι), IsClopen (U i)) (hdisj : Pairwise (Function.onFun Disjoint U)) (hunion : ⋃ (i : ι), U i = Set.univ) {i : ι} (x : ↑(U i)) : (equivOfIsClopen hclopen hdisj hunion).symm ⟨i, mk x⟩ = mk ↑x

theorem ConnectedComponents.equivOfIsClopen_mk {α : Type u} [TopologicalSpace α] {ι : Type u_3} {U : ι → Set α} (hclopen : ∀ (i : ι), IsClopen (U i)) (hdisj : Pairwise (Function.onFun Disjoint U)) (hunion : ⋃ (i : ι), U i = Set.univ) {i : ι} (x : α) (hx : x ∈ U i) : (equivOfIsClopen hclopen hdisj hunion) (mk x) = ⟨i, mk ⟨x, hx⟩⟩

noncomputable def ConnectedComponents.equivOfIsClopenOfIsConnected {α : Type u} [TopologicalSpace α] {ι : Type u_3} {U : ι → Set α} (hclopen : ∀ (i : ι), IsClopen (U i)) (hdisj : Pairwise (Function.onFun Disjoint U)) (hunion : ⋃ (i : ι), U i = Set.univ) (hconn : ∀ (i : ι), IsConnected (U i)) : ConnectedComponents α ≃ ι

If ι indexes a disjoint union decomposition of α, it is equivalent to the connected components of α.

Equations

• One or more equations did not get rendered due to their size.

theorem ConnectedComponents.equivOfIsClopenOfIsConnected_mk {α : Type u} [TopologicalSpace α] {ι : Type u_3} {U : ι → Set α} (hclopen : ∀ (i : ι), IsClopen (U i)) (hdisj : Pairwise (Function.onFun Disjoint U)) (hunion : ⋃ (i : ι), U i = Set.univ) (hconn : ∀ (i : ι), IsConnected (U i)) {i : ι} (x : α) (hx : x ∈ U i) : (equivOfIsClopenOfIsConnected hclopen hdisj hunion hconn) (mk x) = i

theorem ConnectedComponents.exists_fun_isClopen_of_infinite (α : Type u) [TopologicalSpace α] [Infinite (ConnectedComponents α)] (n : ℕ) (hn : 0 < n) : ∃ (U : Fin n → Set α), (∀ (i : Fin n), IsClopen (U i)) ∧ (∀ (i : Fin n), (U i).Nonempty) ∧ Pairwise (Function.onFun Disjoint U) ∧ ⋃ (i : Fin n), U i = Set.univ

If X has infinitely many connected components, it admits disjoint union decompositions with arbitrarily many summands.

theorem connectedComponents_preimage_singleton {α : Type u} [TopologicalSpace α] {x : α} : ConnectedComponents.mk ⁻¹' {ConnectedComponents.mk x} = connectedComponent x

The preimage of a singleton in connectedComponents is the connected component of an element in the equivalence class.

theorem connectedComponents_preimage_image {α : Type u} [TopologicalSpace α] (U : Set α) : ConnectedComponents.mk ⁻¹' ConnectedComponents.mk '' U = ⋃ x ∈ U, connectedComponent x

The preimage of the image of a set under the quotient map to connectedComponents α is the union of the connected components of the elements in it.

theorem ConnectedComponents.discreteTopology_iff {α : Type u} [TopologicalSpace α] : DiscreteTopology (ConnectedComponents α) ↔ ∀ (x : α), IsOpen (connectedComponent x)

theorem isPreconnected_of_forall_constant {α : Type u} [TopologicalSpace α] {s : Set α} (hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y) : IsPreconnected s

If every map to Bool (a discrete two-element space), that is continuous on a set s, is constant on s, then s is preconnected

theorem preconnectedSpace_of_forall_constant {α : Type u} [TopologicalSpace α] (hs : ∀ (f : α → Bool), Continuous f → ∀ (x y : α), f x = f y) : PreconnectedSpace α

A PreconnectedSpace version of isPreconnected_of_forall_constant

theorem preconnectedSpace_iff_clopen {α : Type u} [TopologicalSpace α] : PreconnectedSpace α ↔ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = Set.univ

theorem connectedSpace_iff_clopen {α : Type u} [TopologicalSpace α] : ConnectedSpace α ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = Set.univ

instance instCompactSpaceConnectedComponents {α : Type u} [TopologicalSpace α] [CompactSpace α] : CompactSpace (ConnectedComponents α)