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.
• IsTotallyDisconnected: all of its connected components are singletons.
• IsTotallySeparated: any two points can be separated by two disjoint opens that cover the set.

For each of these definitions, we also have a class stating that the whole space satisfies that property: ConnectedSpace, TotallyDisconnectedSpace, TotallySeparatedSpace.

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 → Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))

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 = (Set.Nonempty s ∧ IsPreconnected s)

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

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 : Set.Subsingleton s) : IsPreconnected s

theorem isPreconnected_of_forall {α : Type u} [TopologicalSpace α] {s : Set α} (x : α) (H : ∀ (y : α), y ∈ s → ∃ t, 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 : α), x ∈ s → ∀ (y : α), y ∈ s → ∃ t, 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 : Set α), s ∈ c → x ∈ s) (H2 : ∀ (s : Set α), 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₁ : Set.Nonempty (⋂ (i : ι), s i)) (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 : Set.Nonempty (s ∩ t)) (hs : IsPreconnected s) (ht : IsPreconnected t) : IsPreconnected (s ∪ t)

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

theorem IsPreconnected.sUnion_directed {α : Type u} [TopologicalSpace α] {S : Set (Set α)} (K : DirectedOn (fun x x_1 => x ⊆ x_1) S) (H : ∀ (s : Set α), 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 : ι), i ∈ t → IsPreconnected (s i)) (K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → Relation.ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j) : IsPreconnected (⋃ (n : ι) (_ : 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 : Set.Nonempty t) (H : ∀ (i : ι), i ∈ t → IsConnected (s i)) (K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → Relation.ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j) : IsConnected (⋃ (n : ι) (_ : 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 => Set.Nonempty (s i ∩ s j)) 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 => Set.Nonempty (s i ∩ s j)) 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 : β), Set.Nonempty (s n ∩ s (Order.succ n))) : 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 : β), Set.Nonempty (s n ∩ s (Order.succ n))) : 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 : Set.OrdConnected t) (H : ∀ (n : β), n ∈ t → IsPreconnected (s n)) (K : ∀ (n : β), n ∈ t → Order.succ n ∈ t → Set.Nonempty (s n ∩ s (Order.succ n))) : IsPreconnected (⋃ (n : β) (_ : 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 : Set.Nonempty t) (ht : Set.OrdConnected t) (H : ∀ (n : β), n ∈ t → IsConnected (s n)) (K : ∀ (n : β), n ∈ t → Order.succ n ∈ t → Set.Nonempty (s n ∩ s (Order.succ n))) : IsConnected (⋃ (n : β) (_ : 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' → Set.Nonempty (s ∩ t) → Set.Nonempty (s ∩ t') → Set.Nonempty (s ∩ (t ∩ t'))

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_open_map {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set β} (hs : IsPreconnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsOpenMap f) (hsf : s ⊆ Set.range f) : IsPreconnected (f ⁻¹' s)

theorem IsPreconnected.preimage_of_closed_map {α : 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_openMap {α : 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_closedMap {α : 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 : Set.Nonempty (s ∩ u)) (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 : Set.Nonempty (s ∩ v)) (hs : IsPreconnected s) : s ⊆ v

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

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

theorem IsPreconnected.subset_of_closure_inter_subset {α : Type u} [TopologicalSpace α] {s : Set α} {u : Set α} (hs : IsPreconnected s) (hu : IsOpen u) (h'u : Set.Nonempty (s ∩ u)) (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.pi Set.univ s)

@[simp]

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

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

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

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

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

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 | 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 { val := x, property := h } else ∅

theorem connectedComponentIn_eq_image {α : Type u} [TopologicalSpace α] {F : Set α} {x : α} (h : x ∈ F) : connectedComponentIn F x = Subtype.val '' connectedComponent { val := x, property := 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 : α} : Set.Nonempty (connectedComponent x)

theorem connectedComponentIn_nonempty_iff {α : Type u} [TopologicalSpace α] {x : α} {F : Set α} : Set.Nonempty (connectedComponentIn F x) ↔ 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.mapsTo_connectedComponent {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (h : Continuous f) (a : α) : Set.MapsTo f (connectedComponent a) (connectedComponent (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

• isPreconnected_univ : IsPreconnected Set.univ

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

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

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

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

  A connected space is nonempty.

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

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

• @Quotient.instConnectedSpace = @Quotient.instConnectedSpace.proof_1

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 instPreconnectedSpaceProdInstTopologicalSpaceProd {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [PreconnectedSpace α] [PreconnectedSpace β] : PreconnectedSpace (α × β)

Equations

• @instPreconnectedSpaceProdInstTopologicalSpaceProd = @instPreconnectedSpaceProdInstTopologicalSpaceProd.proof_1

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

Equations

• @instConnectedSpaceProdInstTopologicalSpaceProd = @instConnectedSpaceProdInstTopologicalSpaceProd.proof_1

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

Equations

• @instPreconnectedSpaceForAllTopologicalSpace = @instPreconnectedSpaceForAllTopologicalSpace.proof_1

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

Equations

• @instConnectedSpaceForAllTopologicalSpace = @instConnectedSpaceForAllTopologicalSpace.proof_1

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

Equations

• PreirreducibleSpace.preconnectedSpace = PreirreducibleSpace.preconnectedSpace.proof_1

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

Equations

• IrreducibleSpace.connectedSpace = IrreducibleSpace.connectedSpace.proof_1

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

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

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

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 : Set.Nonempty s) : s = Set.univ

theorem subsingleton_of_disjoint_isClopen {α : Type u} {ι : Type u_1} [TopologicalSpace α] [PreconnectedSpace α] {s : ι → Set α} (h_nonempty : ∀ (i : ι), Set.Nonempty (s i)) (h_disj : Pairwise (Disjoint on 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 : ι), Set.Nonempty (s i)) (h_disj : Pairwise (Disjoint on 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 : ι), Set.Nonempty (s i)) (h_disj : Pairwise (Disjoint on 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 α} : Set.Nonempty (frontier s) ↔ Set.Nonempty s ∧ s ≠ Set.univ

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

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.

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.

theorem IsPreconnected.induction₂' {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsPreconnected s) (P : α → α → Prop) (h : ∀ (x : α), 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 : α), 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 → Set.Nonempty (s ∩ (u ∩ v)) → u = v) → (∀ (u : Set α), u ∈ U → IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ 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_clopen {α : Type u} [TopologicalSpace α] {s : Set α} {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.connectedComponent_subset {α : Type u} [TopologicalSpace α] {s : Set α} {x : α} (hs : IsClopen s) (hx : x ∈ s) : connectedComponent x ⊆ s

theorem connectedComponent_subset_iInter_clopen {α : Type u} [TopologicalSpace α] {x : α} : connectedComponent x ⊆ ⋂ (Z : { Z // 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 : α) (_ : x ∈ Z), connectedComponent x = Z

A clopen set is the union of its connected components.

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.

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

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

class LocallyConnectedSpace (α : Type u_3) [TopologicalSpace α] : Prop

• open_connected_basis : ∀ (x : α), Filter.HasBasis (nhds x) (fun s => IsOpen s ∧ x ∈ s ∧ IsConnected s) id

  Open connected neighborhoods form a basis of the neighborhoods filter.

A topological space is locally connected if each neighborhood filter admits a basis of connected open sets. Note that it is equivalent to each point having a basis of connected (non necessarily open) sets but in a non-trivial way, so we choose this definition and prove the equivalence later in locallyConnectedSpace_iff_connected_basis.

theorem locallyConnectedSpace_iff_open_connected_basis {α : Type u} [TopologicalSpace α] : LocallyConnectedSpace α ↔ ∀ (x : α), Filter.HasBasis (nhds x) (fun s => IsOpen s ∧ x ∈ s ∧ IsConnected s) id

theorem locallyConnectedSpace_iff_open_connected_subsets {α : Type u} [TopologicalSpace α] : LocallyConnectedSpace α ↔ ∀ (x : α) (U : Set α), U ∈ nhds x → ∃ V, V ⊆ U ∧ IsOpen V ∧ x ∈ V ∧ IsConnected V

instance DiscreteTopology.toLocallyConnectedSpace (α : Type u_3) [TopologicalSpace α] [DiscreteTopology α] : LocallyConnectedSpace α

A space with discrete topology is a locally connected space.

Equations

• DiscreteTopology.toLocallyConnectedSpace = DiscreteTopology.toLocallyConnectedSpace.proof_1

theorem connectedComponentIn_mem_nhds {α : Type u} [TopologicalSpace α] [LocallyConnectedSpace α] {F : Set α} {x : α} (h : F ∈ nhds x) : connectedComponentIn F x ∈ nhds x

theorem IsOpen.connectedComponentIn {α : Type u} [TopologicalSpace α] [LocallyConnectedSpace α] {F : Set α} {x : α} (hF : IsOpen F) : IsOpen (connectedComponentIn F x)

theorem isOpen_connectedComponent {α : Type u} [TopologicalSpace α] [LocallyConnectedSpace α] {x : α} : IsOpen (connectedComponent x)

theorem isClopen_connectedComponent {α : Type u} [TopologicalSpace α] [LocallyConnectedSpace α] {x : α} : IsClopen (connectedComponent x)

theorem locallyConnectedSpace_iff_connectedComponentIn_open {α : Type u} [TopologicalSpace α] : LocallyConnectedSpace α ↔ ∀ (F : Set α), IsOpen F → ∀ (x : α), x ∈ F → IsOpen (connectedComponentIn F x)

theorem locallyConnectedSpace_iff_connected_subsets {α : Type u} [TopologicalSpace α] : LocallyConnectedSpace α ↔ ∀ (x : α) (U : Set α), U ∈ nhds x → ∃ V, V ∈ nhds x ∧ IsPreconnected V ∧ V ⊆ U

theorem locallyConnectedSpace_iff_connected_basis {α : Type u} [TopologicalSpace α] : LocallyConnectedSpace α ↔ ∀ (x : α), Filter.HasBasis (nhds x) (fun s => s ∈ nhds x ∧ IsPreconnected s) id

theorem locallyConnectedSpace_of_connected_bases {α : Type u} [TopologicalSpace α] {ι : Type u_3} (b : α → ι → Set α) (p : α → ι → Prop) (hbasis : ∀ (x : α), Filter.HasBasis (nhds x) (p x) (b x)) (hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)) : LocallyConnectedSpace α

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

A set s is called totally disconnected if every subset t ⊆ s which is preconnected is a subsingleton, ie either empty or a singleton.

Equations

• IsTotallyDisconnected s = ∀ (t : Set α), t ⊆ s → IsPreconnected t → Set.Subsingleton t

theorem isTotallyDisconnected_empty {α : Type u} [TopologicalSpace α] : IsTotallyDisconnected ∅

theorem isTotallyDisconnected_singleton {α : Type u} [TopologicalSpace α] {x : α} : IsTotallyDisconnected {x}

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

• isTotallyDisconnected_univ : IsTotallyDisconnected Set.univ

  The universal set Set.univ in a totally disconnected space is totally disconnected.

A space is totally disconnected if all of its connected components are singletons.

theorem IsPreconnected.subsingleton {α : Type u} [TopologicalSpace α] [TotallyDisconnectedSpace α] {s : Set α} (h : IsPreconnected s) : Set.Subsingleton s

instance Pi.totallyDisconnectedSpace {α : Type u_3} {β : α → Type u_4} [(a : α) → TopologicalSpace (β a)] [∀ (a : α), TotallyDisconnectedSpace (β a)] : TotallyDisconnectedSpace ((a : α) → β a)

Equations

• @Pi.totallyDisconnectedSpace = @Pi.totallyDisconnectedSpace.proof_1

instance Prod.totallyDisconnectedSpace {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace α] [TotallyDisconnectedSpace β] : TotallyDisconnectedSpace (α × β)

Equations

• @Prod.totallyDisconnectedSpace = @Prod.totallyDisconnectedSpace.proof_1

instance instTotallyDisconnectedSpaceSumInstTopologicalSpaceSum {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace α] [TotallyDisconnectedSpace β] : TotallyDisconnectedSpace (α ⊕ β)

Equations

• @instTotallyDisconnectedSpaceSumInstTopologicalSpaceSum = @instTotallyDisconnectedSpaceSumInstTopologicalSpaceSum.proof_1

instance instTotallyDisconnectedSpaceSigmaInstTopologicalSpaceSigma {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), TotallyDisconnectedSpace (π i)] : TotallyDisconnectedSpace ((i : ι) × π i)

Equations

• @instTotallyDisconnectedSpaceSigmaInstTopologicalSpaceSigma = @instTotallyDisconnectedSpaceSigmaInstTopologicalSpaceSigma.proof_1

theorem isTotallyDisconnected_of_clopen_set {X : Type u_3} [TopologicalSpace X] (hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U) : IsTotallyDisconnected Set.univ

Let X be a topological space, and suppose that for all distinct x,y ∈ X, there is some clopen set U such that x ∈ U and y ∉ U. Then X is totally disconnected.

theorem totallyDisconnectedSpace_iff_connectedComponent_subsingleton {α : Type u} [TopologicalSpace α] : TotallyDisconnectedSpace α ↔ ∀ (x : α), Set.Subsingleton (connectedComponent x)

A space is totally disconnected iff its connected components are subsingletons.

theorem totallyDisconnectedSpace_iff_connectedComponent_singleton {α : Type u} [TopologicalSpace α] : TotallyDisconnectedSpace α ↔ ∀ (x : α), connectedComponent x = {x}

A space is totally disconnected iff its connected components are singletons.

@[simp]

theorem connectedComponent_eq_singleton {α : Type u} [TopologicalSpace α] [TotallyDisconnectedSpace α] (x : α) : connectedComponent x = {x}

@[simp]

theorem Continuous.image_connectedComponent_eq_singleton {α : Type u} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) (a : α) : f '' connectedComponent a = {f a}

The image of a connected component in a totally disconnected space is a singleton.

theorem isTotallyDisconnected_of_totallyDisconnectedSpace {α : Type u} [TopologicalSpace α] [TotallyDisconnectedSpace α] (s : Set α) : IsTotallyDisconnected s

theorem isTotallyDisconnected_of_image {α : Type u} {β : Type v} [TopologicalSpace α] {s : Set α} [TopologicalSpace β] {f : α → β} (hf : ContinuousOn f s) (hf' : Function.Injective f) (h : IsTotallyDisconnected (f '' s)) : IsTotallyDisconnected s

theorem Embedding.isTotallyDisconnected {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Embedding f) {s : Set α} (h : IsTotallyDisconnected (f '' s)) : IsTotallyDisconnected s

instance Subtype.totallyDisconnectedSpace {α : Type u_3} {p : α → Prop} [TopologicalSpace α] [TotallyDisconnectedSpace α] : TotallyDisconnectedSpace (Subtype p)

Equations

• @Subtype.totallyDisconnectedSpace = @Subtype.totallyDisconnectedSpace.proof_1

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

A set s is called totally separated if any two points of this set can be separated by two disjoint open sets covering s.

Equations

• IsTotallySeparated s = ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ s ⊆ u ∪ v ∧ Disjoint u v

theorem isTotallySeparated_empty {α : Type u} [TopologicalSpace α] : IsTotallySeparated ∅

theorem isTotallySeparated_singleton {α : Type u} [TopologicalSpace α] {x : α} : IsTotallySeparated {x}

theorem isTotallyDisconnected_of_isTotallySeparated {α : Type u} [TopologicalSpace α] {s : Set α} (H : IsTotallySeparated s) : IsTotallyDisconnected s

theorem IsTotallySeparated.isTotallyDisconnected {α : Type u} [TopologicalSpace α] {s : Set α} (H : IsTotallySeparated s) : IsTotallyDisconnected s

Alias of isTotallyDisconnected_of_isTotallySeparated.

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

• isTotallySeparated_univ : IsTotallySeparated Set.univ

  The universal set Set.univ in a totally separated space is totally separated.

A space is totally separated if any two points can be separated by two disjoint open sets covering the whole space.

instance TotallySeparatedSpace.totallyDisconnectedSpace (α : Type u) [TopologicalSpace α] [TotallySeparatedSpace α] : TotallyDisconnectedSpace α

Equations

• TotallySeparatedSpace.totallyDisconnectedSpace = TotallySeparatedSpace.totallyDisconnectedSpace.proof_1

instance TotallySeparatedSpace.of_discrete (α : Type u_3) [TopologicalSpace α] [DiscreteTopology α] : TotallySeparatedSpace α

Equations

• TotallySeparatedSpace.of_discrete = TotallySeparatedSpace.of_discrete.proof_1

theorem exists_clopen_of_totally_separated {α : Type u_3} [TopologicalSpace α] [TotallySeparatedSpace α] {x : α} {y : α} (hxy : x ≠ y) : ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ

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 := (_ : Equivalence fun x y => connectedComponent x = connectedComponent y) }

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

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

Equations

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

@[simp]

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

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

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

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

Equations

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

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

Equations

• ConnectedComponents.instTopologicalSpaceConnectedComponents = inferInstanceAs (TopologicalSpace (Quotient (connectedComponentSetoid α)))

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

theorem ConnectedComponents.quotientMap_coe {α : Type u} [TopologicalSpace α] : QuotientMap ConnectedComponents.mk

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

@[simp]

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

theorem Continuous.image_eq_of_connectedComponent_eq {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) (a : α) (b : α) (hab : connectedComponent a = connectedComponent b) : f a = f b

def Continuous.connectedComponentsLift {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) : ConnectedComponents α → β

The lift to connectedComponents α of a continuous map from α to a totally disconnected space

Equations

• Continuous.connectedComponentsLift h x = Quotient.liftOn' x f (_ : ∀ (a b : α), connectedComponent a = connectedComponent b → f a = f b)

theorem Continuous.connectedComponentsLift_continuous {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) : Continuous (Continuous.connectedComponentsLift h)

@[simp]

theorem Continuous.connectedComponentsLift_apply_coe {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) (x : α) : Continuous.connectedComponentsLift h (ConnectedComponents.mk x) = f x

@[simp]

theorem Continuous.connectedComponentsLift_comp_coe {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) : Continuous.connectedComponentsLift h ∘ ConnectedComponents.mk = f

theorem connectedComponents_lift_unique' {α : Type u} [TopologicalSpace α] {β : Sort u_3} {g₁ : ConnectedComponents α → β} {g₂ : ConnectedComponents α → β} (hg : g₁ ∘ ConnectedComponents.mk = g₂ ∘ ConnectedComponents.mk) : g₁ = g₂

theorem Continuous.connectedComponentsLift_unique {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) (g : ConnectedComponents α → β) (hg : g ∘ ConnectedComponents.mk = f) : g = Continuous.connectedComponentsLift h

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 : α) (_ : 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.

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

Equations

• @ConnectedComponents.totallyDisconnectedSpace = @ConnectedComponents.totallyDisconnectedSpace.proof_1

def Continuous.connectedComponentsMap {α : Type u} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] {f : α → β} (h : Continuous f) : ConnectedComponents α → ConnectedComponents β

Functoriality of connectedComponents

Equations

• Continuous.connectedComponentsMap h = Continuous.connectedComponentsLift (_ : Continuous (ConnectedComponents.mk ∘ f))

theorem Continuous.connectedComponentsMap_continuous {α : Type u} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] {f : α → β} (h : Continuous f) : Continuous (Continuous.connectedComponentsMap h)

theorem IsPreconnected.constant {α : Type u} [TopologicalSpace α] {Y : Type u_3} [TopologicalSpace Y] [DiscreteTopology Y] {s : Set α} (hs : IsPreconnected s) {f : α → Y} (hf : ContinuousOn f s) {x : α} {y : α} (hx : x ∈ s) (hy : y ∈ s) : f x = f y

A preconnected set s has the property that every map to a discrete space that is continuous on s is constant on s

theorem isPreconnected_of_forall_constant {α : Type u} [TopologicalSpace α] {s : Set α} (hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), 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.constant {α : Type u} [TopologicalSpace α] {Y : Type u_3} [TopologicalSpace Y] [DiscreteTopology Y] (hp : PreconnectedSpace α) {f : α → Y} (hf : Continuous f) {x : α} {y : α} : f x = f y

A PreconnectedSpace version of isPreconnected.constant

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 IsPreconnected.constant_of_mapsTo {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {S : Set α} (hS : IsPreconnected S) {T : Set β} [DiscreteTopology ↑T] {f : α → β} (hc : ContinuousOn f S) (hTm : Set.MapsTo f S T) {x : α} {y : α} (hx : x ∈ S) (hy : y ∈ S) : f x = f y

Refinement of IsPreconnected.constant only assuming the map factors through a discrete subset of the target.

theorem IsPreconnected.eqOn_const_of_mapsTo {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {S : Set α} (hS : IsPreconnected S) {T : Set β} [DiscreteTopology ↑T] {f : α → β} (hc : ContinuousOn f S) (hTm : Set.MapsTo f S T) (hne : Set.Nonempty T) : ∃ y, y ∈ T ∧ Set.EqOn f (Function.const α y) S

A version of IsPreconnected.constant_of_mapsTo that assumes that the codomain is nonempty and proves that f is equal to const α y on S for some y ∈ T.