Connected subsets of topological spaces

In this file we define connected subsets of a topological spaces and various other properties and classes related to connectivity.

Main definitions

We define the following properties for sets in a topological space:

• IsConnected: a nonempty set that has no non-trivial open partition. See also the section below in the module doc.
• connectedComponent is the connected component of an element in the space.

We also have a class stating that the whole space satisfies that property: ConnectedSpace

On the definition of connected sets/spaces

In informal mathematics, connected spaces are assumed to be nonempty. We formalise the predicate without that assumption as IsPreconnected. In other words, the only difference is whether the empty space counts as connected. There are good reasons to consider the empty space to be “too simple to be simple” See also https://ncatlab.org/nlab/show/too+simple+to+be+simple, and in particular https://ncatlab.org/nlab/show/too+simple+to+be+simple#relationship_to_biased_definitions.

def IsPreconnected {α : Type u} [TopologicalSpace α] (s : Set α) : Prop

A preconnected set is one where there is no non-trivial open partition.

Equations

• IsPreconnected s = ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

def IsConnected {α : Type u} [TopologicalSpace α] (s : Set α) : Prop

A connected set is one that is nonempty and where there is no non-trivial open partition.

Equations

• IsConnected s = (s.Nonempty ∧ IsPreconnected s)

theorem IsConnected.nonempty {α : Type u} [TopologicalSpace α] {s : Set α} (h : IsConnected s) : s.Nonempty

theorem IsConnected.isPreconnected {α : Type u} [TopologicalSpace α] {s : Set α} (h : IsConnected s) : IsPreconnected s

theorem IsPreirreducible.isPreconnected {α : Type u} [TopologicalSpace α] {s : Set α} (H : IsPreirreducible s) : IsPreconnected s

theorem IsIrreducible.isConnected {α : Type u} [TopologicalSpace α] {s : Set α} (H : IsIrreducible s) : IsConnected s

theorem isPreconnected_empty {α : Type u} [TopologicalSpace α] : IsPreconnected ∅

theorem isConnected_singleton {α : Type u} [TopologicalSpace α] {x : α} : IsConnected {x}

theorem isPreconnected_singleton {α : Type u} [TopologicalSpace α] {x : α} : IsPreconnected {x}

theorem Set.Subsingleton.isPreconnected {α : Type u} [TopologicalSpace α] {s : Set α} (hs : s.Subsingleton) : IsPreconnected s

theorem isPreconnected_of_forall {α : Type u} [TopologicalSpace α] {s : Set α} (x : α) (H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t) : IsPreconnected s

If any point of a set is joined to a fixed point by a preconnected subset, then the original set is preconnected as well.

theorem isPreconnected_of_forall_pair {α : Type u} [TopologicalSpace α] {s : Set α} (H : ∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t) : IsPreconnected s

If any two points of a set are contained in a preconnected subset, then the original set is preconnected as well.

theorem isPreconnected_sUnion {α : Type u} [TopologicalSpace α] (x : α) (c : Set (Set α)) (H1 : ∀ s ∈ c, x ∈ s) (H2 : ∀ s ∈ c, IsPreconnected s) : IsPreconnected (⋃₀ c)

A union of a family of preconnected sets with a common point is preconnected as well.

theorem isPreconnected_iUnion {α : Type u} [TopologicalSpace α] {ι : Sort u_3} {s : ι → Set α} (h₁ : (⋂ (i : ι), s i).Nonempty) (h₂ : ∀ (i : ι), IsPreconnected (s i)) : IsPreconnected (⋃ (i : ι), s i)

theorem IsPreconnected.union {α : Type u} [TopologicalSpace α] (x : α) {s : Set α} {t : Set α} (H1 : x ∈ s) (H2 : x ∈ t) (H3 : IsPreconnected s) (H4 : IsPreconnected t) : IsPreconnected (s ∪ t)

theorem IsPreconnected.union' {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (H : (s ∩ t).Nonempty) (hs : IsPreconnected s) (ht : IsPreconnected t) : IsPreconnected (s ∪ t)

theorem IsConnected.union {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (H : (s ∩ t).Nonempty) (Hs : IsConnected s) (Ht : IsConnected t) : IsConnected (s ∪ t)

theorem IsPreconnected.sUnion_directed {α : Type u} [TopologicalSpace α] {S : Set (Set α)} (K : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) S) (H : ∀ s ∈ S, IsPreconnected s) : IsPreconnected (⋃₀ S)

The directed sUnion of a set S of preconnected subsets is preconnected.

theorem IsPreconnected.biUnion_of_reflTransGen {α : Type u} [TopologicalSpace α] {ι : Type u_3} {t : Set ι} {s : ι → Set α} (H : ∀ i ∈ t, IsPreconnected (s i)) (K : ∀ i ∈ t, ∀ j ∈ t, Relation.ReflTransGen (fun (i j : ι) => (s i ∩ s j).Nonempty ∧ i ∈ t) i j) : IsPreconnected (⋃ n ∈ t, s n)

The biUnion of a family of preconnected sets is preconnected if the graph determined by whether two sets intersect is preconnected.

theorem IsConnected.biUnion_of_reflTransGen {α : Type u} [TopologicalSpace α] {ι : Type u_3} {t : Set ι} {s : ι → Set α} (ht : t.Nonempty) (H : ∀ i ∈ t, IsConnected (s i)) (K : ∀ i ∈ t, ∀ j ∈ t, Relation.ReflTransGen (fun (i j : ι) => (s i ∩ s j).Nonempty ∧ i ∈ t) i j) : IsConnected (⋃ n ∈ t, s n)

The biUnion of a family of preconnected sets is preconnected if the graph determined by whether two sets intersect is preconnected.

theorem IsPreconnected.iUnion_of_reflTransGen {α : Type u} [TopologicalSpace α] {ι : Type u_3} {s : ι → Set α} (H : ∀ (i : ι), IsPreconnected (s i)) (K : ∀ (i j : ι), Relation.ReflTransGen (fun (i j : ι) => (s i ∩ s j).Nonempty) i j) : IsPreconnected (⋃ (n : ι), s n)

Preconnectedness of the iUnion of a family of preconnected sets indexed by the vertices of a preconnected graph, where two vertices are joined when the corresponding sets intersect.

theorem IsConnected.iUnion_of_reflTransGen {α : Type u} [TopologicalSpace α] {ι : Type u_3} [Nonempty ι] {s : ι → Set α} (H : ∀ (i : ι), IsConnected (s i)) (K : ∀ (i j : ι), Relation.ReflTransGen (fun (i j : ι) => (s i ∩ s j).Nonempty) i j) : IsConnected (⋃ (n : ι), s n)

theorem IsPreconnected.iUnion_of_chain {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder β] [SuccOrder β] [IsSuccArchimedean β] {s : β → Set α} (H : ∀ (n : β), IsPreconnected (s n)) (K : ∀ (n : β), (s n ∩ s (Order.succ n)).Nonempty) : IsPreconnected (⋃ (n : β), s n)

The iUnion of connected sets indexed by a type with an archimedean successor (like ℕ or ℤ) such that any two neighboring sets meet is preconnected.

theorem IsConnected.iUnion_of_chain {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder β] [SuccOrder β] [IsSuccArchimedean β] [Nonempty β] {s : β → Set α} (H : ∀ (n : β), IsConnected (s n)) (K : ∀ (n : β), (s n ∩ s (Order.succ n)).Nonempty) : IsConnected (⋃ (n : β), s n)

The iUnion of connected sets indexed by a type with an archimedean successor (like ℕ or ℤ) such that any two neighboring sets meet is connected.

theorem IsPreconnected.biUnion_of_chain {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder β] [SuccOrder β] [IsSuccArchimedean β] {s : β → Set α} {t : Set β} (ht : t.OrdConnected) (H : ∀ n ∈ t, IsPreconnected (s n)) (K : ∀ n ∈ t, Order.succ n ∈ t → (s n ∩ s (Order.succ n)).Nonempty) : IsPreconnected (⋃ n ∈ t, s n)

The iUnion of preconnected sets indexed by a subset of a type with an archimedean successor (like ℕ or ℤ) such that any two neighboring sets meet is preconnected.

theorem IsConnected.biUnion_of_chain {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder β] [SuccOrder β] [IsSuccArchimedean β] {s : β → Set α} {t : Set β} (hnt : t.Nonempty) (ht : t.OrdConnected) (H : ∀ n ∈ t, IsConnected (s n)) (K : ∀ n ∈ t, Order.succ n ∈ t → (s n ∩ s (Order.succ n)).Nonempty) : IsConnected (⋃ n ∈ t, s n)

The iUnion of connected sets indexed by a subset of a type with an archimedean successor (like ℕ or ℤ) such that any two neighboring sets meet is preconnected.

theorem IsPreconnected.subset_closure {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (H : IsPreconnected s) (Kst : s ⊆ t) (Ktcs : t ⊆ closure s) : IsPreconnected t

Theorem of bark and tree: if a set is within a preconnected set and its closure, then it is preconnected as well. See also IsConnected.subset_closure.

theorem IsConnected.subset_closure {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (H : IsConnected s) (Kst : s ⊆ t) (Ktcs : t ⊆ closure s) : IsConnected t

Theorem of bark and tree: if a set is within a connected set and its closure, then it is connected as well. See also IsPreconnected.subset_closure.

theorem IsPreconnected.closure {α : Type u} [TopologicalSpace α] {s : Set α} (H : IsPreconnected s) : IsPreconnected (closure s)

The closure of a preconnected set is preconnected as well.

theorem IsConnected.closure {α : Type u} [TopologicalSpace α] {s : Set α} (H : IsConnected s) : IsConnected (closure s)

The closure of a connected set is connected as well.

theorem IsPreconnected.image {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (H : IsPreconnected s) (f : α → β) (hf : ContinuousOn f s) : IsPreconnected (f '' s)

The image of a preconnected set is preconnected as well.

theorem IsConnected.image {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (H : IsConnected s) (f : α → β) (hf : ContinuousOn f s) : IsConnected (f '' s)

The image of a connected set is connected as well.

theorem isPreconnected_closed_iff {α : Type u} [TopologicalSpace α] {s : Set α} : IsPreconnected s ↔ ∀ (t t' : Set α), IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty

theorem Inducing.isPreconnected_image {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : α → β} (hf : Inducing f) : IsPreconnected (f '' s) ↔ IsPreconnected s

theorem IsPreconnected.preimage_of_isOpenMap {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set β} (hs : IsPreconnected s) (hinj : Function.Injective f) (hf : IsOpenMap f) (hsf : s ⊆ Set.range f) : IsPreconnected (f ⁻¹' s)

theorem IsPreconnected.preimage_of_isClosedMap {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set β} (hs : IsPreconnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsClosedMap f) (hsf : s ⊆ Set.range f) : IsPreconnected (f ⁻¹' s)

theorem IsConnected.preimage_of_isOpenMap {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set β} (hs : IsConnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsOpenMap f) (hsf : s ⊆ Set.range f) : IsConnected (f ⁻¹' s)

theorem IsConnected.preimage_of_isClosedMap {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set β} (hs : IsConnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsClosedMap f) (hsf : s ⊆ Set.range f) : IsConnected (f ⁻¹' s)

theorem IsPreconnected.subset_or_subset {α : Type u} [TopologicalSpace α] {s : Set α} {u : Set α} {v : Set α} (hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hs : IsPreconnected s) : s ⊆ u ∨ s ⊆ v

theorem IsPreconnected.subset_left_of_subset_union {α : Type u} [TopologicalSpace α] {s : Set α} {u : Set α} {v : Set α} (hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hsu : (s ∩ u).Nonempty) (hs : IsPreconnected s) : s ⊆ u

theorem IsPreconnected.subset_right_of_subset_union {α : Type u} [TopologicalSpace α] {s : Set α} {u : Set α} {v : Set α} (hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hsv : (s ∩ v).Nonempty) (hs : IsPreconnected s) : s ⊆ v

theorem IsPreconnected.subset_of_closure_inter_subset {α : Type u} [TopologicalSpace α] {s : Set α} {u : Set α} (hs : IsPreconnected s) (hu : IsOpen u) (h'u : (s ∩ u).Nonempty) (h : closure u ∩ s ⊆ u) : s ⊆ u

If a preconnected set s intersects an open set u, and limit points of u inside s are contained in u, then the whole set s is contained in u.

theorem IsPreconnected.prod {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsPreconnected s) (ht : IsPreconnected t) : IsPreconnected (s ×ˢ t)

theorem IsConnected.prod {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsConnected s) (ht : IsConnected t) : IsConnected (s ×ˢ t)

theorem isPreconnected_univ_pi {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → TopologicalSpace (π i)] {s : (i : ι) → Set (π i)} (hs : ∀ (i : ι), IsPreconnected (s i)) : IsPreconnected (Set.univ.pi s)

@[simp]

theorem isConnected_univ_pi {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → TopologicalSpace (π i)] {s : (i : ι) → Set (π i)} : IsConnected (Set.univ.pi s) ↔ ∀ (i : ι), IsConnected (s i)

def connectedComponent {α : Type u} [TopologicalSpace α] (x : α) : Set α

The connected component of a point is the maximal connected set that contains this point.

Equations

• connectedComponent x = ⋃₀ {s : Set α | IsPreconnected s ∧ x ∈ s}

def connectedComponentIn {α : Type u} [TopologicalSpace α] (F : Set α) (x : α) : Set α

Given a set F in a topological space α and a point x : α, the connected component of x in F is the connected component of x in the subtype F seen as a set in α. This definition does not make sense if x is not in F so we return the empty set in this case.

Equations

• connectedComponentIn F x = if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅

theorem connectedComponentIn_eq_image {α : Type u} [TopologicalSpace α] {F : Set α} {x : α} (h : x ∈ F) : connectedComponentIn F x = Subtype.val '' connectedComponent ⟨x, h⟩

theorem connectedComponentIn_eq_empty {α : Type u} [TopologicalSpace α] {F : Set α} {x : α} (h : x ∉ F) : connectedComponentIn F x = ∅

theorem mem_connectedComponent {α : Type u} [TopologicalSpace α] {x : α} : x ∈ connectedComponent x

theorem mem_connectedComponentIn {α : Type u} [TopologicalSpace α] {x : α} {F : Set α} (hx : x ∈ F) : x ∈ connectedComponentIn F x

theorem connectedComponent_nonempty {α : Type u} [TopologicalSpace α] {x : α} : (connectedComponent x).Nonempty

theorem connectedComponentIn_nonempty_iff {α : Type u} [TopologicalSpace α] {x : α} {F : Set α} : (connectedComponentIn F x).Nonempty ↔ x ∈ F

theorem connectedComponentIn_subset {α : Type u} [TopologicalSpace α] (F : Set α) (x : α) : connectedComponentIn F x ⊆ F

theorem isPreconnected_connectedComponent {α : Type u} [TopologicalSpace α] {x : α} : IsPreconnected (connectedComponent x)

theorem isPreconnected_connectedComponentIn {α : Type u} [TopologicalSpace α] {x : α} {F : Set α} : IsPreconnected (connectedComponentIn F x)

theorem isConnected_connectedComponent {α : Type u} [TopologicalSpace α] {x : α} : IsConnected (connectedComponent x)

theorem isConnected_connectedComponentIn_iff {α : Type u} [TopologicalSpace α] {x : α} {F : Set α} : IsConnected (connectedComponentIn F x) ↔ x ∈ F

theorem IsPreconnected.subset_connectedComponent {α : Type u} [TopologicalSpace α] {x : α} {s : Set α} (H1 : IsPreconnected s) (H2 : x ∈ s) : s ⊆ connectedComponent x

theorem IsPreconnected.subset_connectedComponentIn {α : Type u} [TopologicalSpace α] {s : Set α} {x : α} {F : Set α} (hs : IsPreconnected s) (hxs : x ∈ s) (hsF : s ⊆ F) : s ⊆ connectedComponentIn F x

theorem IsConnected.subset_connectedComponent {α : Type u} [TopologicalSpace α] {x : α} {s : Set α} (H1 : IsConnected s) (H2 : x ∈ s) : s ⊆ connectedComponent x

theorem IsPreconnected.connectedComponentIn {α : Type u} [TopologicalSpace α] {x : α} {F : Set α} (h : IsPreconnected F) (hx : x ∈ F) : connectedComponentIn F x = F

theorem connectedComponent_eq {α : Type u} [TopologicalSpace α] {x : α} {y : α} (h : y ∈ connectedComponent x) : connectedComponent x = connectedComponent y

theorem connectedComponent_eq_iff_mem {α : Type u} [TopologicalSpace α] {x : α} {y : α} : connectedComponent x = connectedComponent y ↔ x ∈ connectedComponent y

theorem connectedComponentIn_eq {α : Type u} [TopologicalSpace α] {x : α} {y : α} {F : Set α} (h : y ∈ connectedComponentIn F x) : connectedComponentIn F x = connectedComponentIn F y

theorem connectedComponentIn_univ {α : Type u} [TopologicalSpace α] (x : α) : connectedComponentIn Set.univ x = connectedComponent x

theorem connectedComponent_disjoint {α : Type u} [TopologicalSpace α] {x : α} {y : α} (h : connectedComponent x ≠ connectedComponent y) : Disjoint (connectedComponent x) (connectedComponent y)

theorem isClosed_connectedComponent {α : Type u} [TopologicalSpace α] {x : α} : IsClosed (connectedComponent x)

theorem Continuous.image_connectedComponent_subset {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (h : Continuous f) (a : α) : f '' connectedComponent a ⊆ connectedComponent (f a)

theorem Continuous.image_connectedComponentIn_subset {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {a : α} (hf : Continuous f) (hx : a ∈ s) : f '' connectedComponentIn s a ⊆ connectedComponentIn (f '' s) (f a)

theorem Continuous.mapsTo_connectedComponent {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (h : Continuous f) (a : α) : Set.MapsTo f (connectedComponent a) (connectedComponent (f a))

theorem Continuous.mapsTo_connectedComponentIn {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (h : Continuous f) {a : α} (hx : a ∈ s) : Set.MapsTo f (connectedComponentIn s a) (connectedComponentIn (f '' s) (f a))

theorem irreducibleComponent_subset_connectedComponent {α : Type u} [TopologicalSpace α] {x : α} : irreducibleComponent x ⊆ connectedComponent x

theorem connectedComponentIn_mono {α : Type u} [TopologicalSpace α] (x : α) {F : Set α} {G : Set α} (h : F ⊆ G) : connectedComponentIn F x ⊆ connectedComponentIn G x

class PreconnectedSpace (α : Type u) [TopologicalSpace α] : Prop

A preconnected space is one where there is no non-trivial open partition.

• isPreconnected_univ : IsPreconnected Set.univ

  The universal set Set.univ in a preconnected space is a preconnected set.

theorem PreconnectedSpace.isPreconnected_univ {α : Type u} [TopologicalSpace α] [self : PreconnectedSpace α] : IsPreconnected Set.univ

The universal set Set.univ in a preconnected space is a preconnected set.

class ConnectedSpace (α : Type u) [TopologicalSpace α] extends PreconnectedSpace : Prop

A connected space is a nonempty one where there is no non-trivial open partition.

• isPreconnected_univ : IsPreconnected Set.univ
• toNonempty : Nonempty α

  A connected space is nonempty.

theorem ConnectedSpace.toNonempty {α : Type u} [TopologicalSpace α] [self : ConnectedSpace α] : Nonempty α

A connected space is nonempty.

theorem isConnected_univ {α : Type u} [TopologicalSpace α] [ConnectedSpace α] : IsConnected Set.univ

theorem preconnectedSpace_iff_univ {α : Type u} [TopologicalSpace α] : PreconnectedSpace α ↔ IsPreconnected Set.univ

theorem connectedSpace_iff_univ {α : Type u} [TopologicalSpace α] : ConnectedSpace α ↔ IsConnected Set.univ

theorem isPreconnected_range {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [PreconnectedSpace α] {f : α → β} (h : Continuous f) : IsPreconnected (Set.range f)

theorem isConnected_range {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [ConnectedSpace α] {f : α → β} (h : Continuous f) : IsConnected (Set.range f)

theorem Function.Surjective.connectedSpace {α : Type u} {β : Type v} [TopologicalSpace α] [ConnectedSpace α] [TopologicalSpace β] {f : α → β} (hf : Function.Surjective f) (hf' : Continuous f) : ConnectedSpace β

instance Quotient.instConnectedSpace {α : Type u} [TopologicalSpace α] {s : Setoid α} [ConnectedSpace α] : ConnectedSpace (Quotient s)

Equations

• ⋯ = ⋯

theorem DenseRange.preconnectedSpace {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [PreconnectedSpace α] {f : α → β} (hf : DenseRange f) (hc : Continuous f) : PreconnectedSpace β

theorem connectedSpace_iff_connectedComponent {α : Type u} [TopologicalSpace α] : ConnectedSpace α ↔ ∃ (x : α), connectedComponent x = Set.univ

theorem preconnectedSpace_iff_connectedComponent {α : Type u} [TopologicalSpace α] : PreconnectedSpace α ↔ ∀ (x : α), connectedComponent x = Set.univ

@[simp]

theorem PreconnectedSpace.connectedComponent_eq_univ {X : Type u_3} [TopologicalSpace X] [h : PreconnectedSpace X] (x : X) : connectedComponent x = Set.univ

instance instPreconnectedSpaceProd {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [PreconnectedSpace α] [PreconnectedSpace β] : PreconnectedSpace (α × β)

Equations

• ⋯ = ⋯

instance instConnectedSpaceProd {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [ConnectedSpace α] [ConnectedSpace β] : ConnectedSpace (α × β)

Equations

• ⋯ = ⋯

instance instPreconnectedSpaceForall {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), PreconnectedSpace (π i)] : PreconnectedSpace ((i : ι) → π i)

Equations

• ⋯ = ⋯

instance instConnectedSpaceForall {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), ConnectedSpace (π i)] : ConnectedSpace ((i : ι) → π i)

Equations

• ⋯ = ⋯

@[instance 100]

instance PreirreducibleSpace.preconnectedSpace (α : Type u) [TopologicalSpace α] [PreirreducibleSpace α] : PreconnectedSpace α

Equations

• ⋯ = ⋯

@[instance 100]

instance IrreducibleSpace.connectedSpace (α : Type u) [TopologicalSpace α] [IrreducibleSpace α] : ConnectedSpace α

Equations

• ⋯ = ⋯

theorem Subtype.preconnectedSpace {α : Type u} [TopologicalSpace α] {s : Set α} (h : IsPreconnected s) : PreconnectedSpace ↑s

theorem Subtype.connectedSpace {α : Type u} [TopologicalSpace α] {s : Set α} (h : IsConnected s) : ConnectedSpace ↑s

theorem isPreconnected_iff_preconnectedSpace {α : Type u} [TopologicalSpace α] {s : Set α} : IsPreconnected s ↔ PreconnectedSpace ↑s

theorem isConnected_iff_connectedSpace {α : Type u} [TopologicalSpace α] {s : Set α} : IsConnected s ↔ ConnectedSpace ↑s