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.connectedComponentis 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.
A connected set is one that is nonempty and where there is no non-trivial open partition.
Equations
- IsConnected s = (s.Nonempty ∧ IsPreconnected s)
Instances For
theorem
IsConnected.nonempty
{α : Type u}
[TopologicalSpace α]
{s : Set α}
(h : IsConnected s)
:
s.Nonempty
theorem
IsConnected.isPreconnected
{α : Type u}
[TopologicalSpace α]
{s : Set α}
(h : IsConnected s)
:
theorem
IsPreirreducible.isPreconnected
{α : Type u}
[TopologicalSpace α]
{s : Set α}
(H : IsPreirreducible s)
:
theorem
IsIrreducible.isConnected
{α : Type u}
[TopologicalSpace α]
{s : Set α}
(H : IsIrreducible s)
:
theorem
Set.Subsingleton.isPreconnected
{α : Type u}
[TopologicalSpace α]
{s : Set α}
(hs : s.Subsingleton)
:
theorem
isPreconnected_of_forall
{α : Type u}
[TopologicalSpace α]
{s : Set α}
(x : α)
(H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t)
:
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)
:
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 t : Set α}
(H1 : x ∈ s)
(H2 : x ∈ t)
(H3 : IsPreconnected s)
(H4 : IsPreconnected t)
:
IsPreconnected (s ∪ t)
theorem
IsPreconnected.union'
{α : Type u}
[TopologicalSpace α]
{s t : Set α}
(H : (s ∩ t).Nonempty)
(hs : IsPreconnected s)
(ht : IsPreconnected t)
:
IsPreconnected (s ∪ t)
theorem
IsConnected.union
{α : Type u}
[TopologicalSpace α]
{s 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 t : Set α}
(H : IsPreconnected s)
(Kst : s ⊆ t)
(Ktcs : t ⊆ closure s)
:
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 t : Set α}
(H : IsConnected s)
(Kst : s ⊆ t)
(Ktcs : t ⊆ closure s)
:
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)
:
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
Topology.IsInducing.isPreconnected_image
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set α}
{f : α → β}
(hf : Topology.IsInducing f)
:
IsPreconnected (f '' s) ↔ IsPreconnected s
@[deprecated Topology.IsInducing.isPreconnected_image]
theorem
Inducing.isPreconnected_image
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set α}
{f : α → β}
(hf : Topology.IsInducing f)
:
IsPreconnected (f '' s) ↔ IsPreconnected s
Alias of Topology.IsInducing.isPreconnected_image.
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 u v : Set α}
(hu : IsOpen u)
(hv : IsOpen v)
(huv : Disjoint u v)
(hsuv : s ⊆ u ∪ v)
(hs : IsPreconnected s)
:
theorem
IsPreconnected.subset_left_of_subset_union
{α : Type u}
[TopologicalSpace α]
{s u 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 u 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 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)
The connected component of a point is the maximal connected set that contains this point.
Equations
- connectedComponent x = ⋃₀ {s : Set α | IsPreconnected s ∧ x ∈ s}
Instances For
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 ∅
Instances For
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_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
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)
:
theorem
connectedComponentIn_eq
{α : Type u}
[TopologicalSpace α]
{x y : α}
{F : Set α}
(h : y ∈ connectedComponentIn F x)
:
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)
:
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
connectedComponentIn_mono
{α : Type u}
[TopologicalSpace α]
(x : α)
{F G : Set α}
(h : F ⊆ G)
:
A preconnected space is one where there is no non-trivial open partition.
- isPreconnected_univ : IsPreconnected Set.univ
The universal set
Set.univin a preconnected space is a preconnected set.
Instances
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.
Instances
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)
:
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)
:
instance
Quotient.instConnectedSpace
{α : Type u}
[TopologicalSpace α]
{s : Setoid α}
[ConnectedSpace α]
:
Equations
- ⋯ = ⋯
theorem
DenseRange.preconnectedSpace
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
[PreconnectedSpace α]
{f : α → β}
(hf : DenseRange f)
(hc : Continuous f)
:
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 α]
:
Equations
- ⋯ = ⋯
@[instance 100]
Equations
- ⋯ = ⋯
theorem
Subtype.preconnectedSpace
{α : Type u}
[TopologicalSpace α]
{s : Set α}
(h : IsPreconnected s)
:
theorem
isConnected_iff_connectedSpace
{α : Type u}
[TopologicalSpace α]
{s : Set α}
:
IsConnected s ↔ ConnectedSpace ↑s