# 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.

source
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.

source
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
source
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
source
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
source
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
source
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 `ContinuousMap`s.

source
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
source
theorem isClopen_iff {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] {s : Set α} :
IsClopen s ↔ s = ∅ ∨ s = Set.univ
source
theorem IsClopen.eq_univ {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] {s : Set α} (h' : IsClopen s) (h : s.Nonempty) :
s = Set.univ
source
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)
source
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.

source
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.

source
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.

source
theorem frontier_eq_empty_iff {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] {s : Set α} :
frontier s = ∅ ↔ s = ∅ ∨ s = Set.univ
source
theorem nonempty_frontier_iff {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] {s : Set α} :
(frontier s).Nonempty ↔ s.Nonempty ∧ s ≠ Set.univ
source
theorem PreconnectedSpace.induction₂' {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] (P : α → α → Prop) (h : ∀ (x : α), ∀ᶠ (y : α) in nhds x, P x y ∧ P y x) (h' : Transitive 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.

source
theorem PreconnectedSpace.induction₂ {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] (P : α → α → Prop) (h : ∀ (x : α), ∀ᶠ (y : α) in nhds x, P x y) (h' : Transitive P) (h'' : Symmetric 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.

source
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.

source
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.

source
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.

source
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.

source
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.

source
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.

source
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.

source
theorem IsClopen.connectedComponent_subset {α : Type u} [TopologicalSpace α] {s : Set α} {x : α} (hs : IsClopen s) (hx : x ∈ s) :
connectedComponent x ⊆ s
source
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.

source
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.

source
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`.

source
theorem preimage_connectedComponent_connected {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})) (hcl : ∀ (T : Set β), IsClosed T ↔ IsClosed (f ⁻¹' T)) (t : β) :
IsConnected (f ⁻¹' connectedComponent t)

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

source
theorem Topology.IsQuotientMap.preimage_connectedComponent {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : IsQuotientMap f) (h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})) (a : α) :
f ⁻¹' connectedComponent (f a) = connectedComponent a
source
theorem Topology.IsQuotientMap.image_connectedComponent {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : IsQuotientMap f) (h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})) (a : α) :
f '' connectedComponent a = connectedComponent (f a)
source
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 := ⋯ }

Instances For

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

The quotient of a space by its connected components

Equations

- ConnectedComponents α = Quotient (connectedComponentSetoid α)

Instances For

source
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''

Instances For

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

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

source
@[simp]
theorem ConnectedComponents.coe_eq_coe {α : Type u} [TopologicalSpace α] {x y : α} :
mk x = mk y ↔ connectedComponent x = connectedComponent y
source
theorem ConnectedComponents.coe_ne_coe {α : Type u} [TopologicalSpace α] {x y : α} :
mk x ≠ mk y ↔ connectedComponent x ≠ connectedComponent y
source
theorem ConnectedComponents.coe_eq_coe' {α : Type u} [TopologicalSpace α] {x y : α} :
mk x = mk y ↔ x ∈ connectedComponent y
source
instance ConnectedComponents.instInhabited {α : Type u} [TopologicalSpace α] [Inhabited α] :
Inhabited (ConnectedComponents α)
Equations

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

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

- ConnectedComponents.instTopologicalSpace = inferInstanceAs (TopologicalSpace (Quotient (connectedComponentSetoid α)))

source
theorem ConnectedComponents.surjective_coe {α : Type u} [TopologicalSpace α] :
Function.Surjective mk
source
theorem ConnectedComponents.isQuotientMap_coe {α : Type u} [TopologicalSpace α] :
Topology.IsQuotientMap mk
source
theorem ConnectedComponents.continuous_coe {α : Type u} [TopologicalSpace α] :
Continuous mk
source
@[simp]
theorem ConnectedComponents.range_coe {α : Type u} [TopologicalSpace α] :
Set.range mk = Set.univ
source
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.

source
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.

source
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

source
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`

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