Documentation

Mathlib.Topology.Connected.Basic

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:

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 α) :

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

Equations
Instances For
    def IsConnected {α : Type u} [TopologicalSpace α] (s : Set α) :

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

    Equations
    Instances For
      theorem IsConnected.nonempty {α : Type u} [TopologicalSpace α] {s : Set α} (h : IsConnected s) :
      s.Nonempty
      theorem isConnected_singleton {α : Type u} [TopologicalSpace α] {x : α} :
      theorem Set.Subsingleton.isPreconnected {α : Type u} [TopologicalSpace α] {s : Set α} (hs : s.Subsingleton) :
      theorem isPreconnected_of_forall {α : Type u} [TopologicalSpace α] {s : Set α} (x : α) (H : ys, ts, 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 : xs, ys, ts, 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 : sc, x s) (H2 : sc, IsPreconnected s) :

      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) :
      theorem IsPreconnected.union' {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (H : (s t).Nonempty) (hs : IsPreconnected s) (ht : IsPreconnected t) :
      theorem IsConnected.union {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (H : (s t).Nonempty) (Hs : IsConnected s) (Ht : IsConnected t) :
      theorem IsPreconnected.sUnion_directed {α : Type u} [TopologicalSpace α] {S : Set (Set α)} (K : DirectedOn (fun (x x_1 : Set α) => x x_1) S) (H : sS, 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 : it, IsPreconnected (s i)) (K : it, jt, Relation.ReflTransGen (fun (i j : ι) => (s i s j).Nonempty i t) i j) :
      IsPreconnected (nt, 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 : it, IsConnected (s i)) (K : it, jt, Relation.ReflTransGen (fun (i j : ι) => (s i s j).Nonempty i t) i j) :
      IsConnected (nt, 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 : nt, IsPreconnected (s n)) (K : nt, Order.succ n t(s n s (Order.succ n)).Nonempty) :
      IsPreconnected (nt, 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 : nt, IsConnected (s n)) (K : nt, Order.succ n t(s n s (Order.succ n)).Nonempty) :
      IsConnected (nt, 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) :

      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) :

      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.

      The closure of a preconnected set is preconnected as well.

      theorem IsConnected.closure {α : Type u} [TopologicalSpace α] {s : Set α} (H : IsConnected 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) :

      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) :

      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 tIsClosed 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) :
      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) :
      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) :
      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) :
      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) :
      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_isClopen {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (hs : IsPreconnected s) (ht : IsClopen t) (hne : (s t).Nonempty) :
      s t

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

      theorem 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) :
      theorem IsConnected.prod {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsConnected s) (ht : IsConnected 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)
      theorem Sigma.isConnected_iff {ι : Type u_1} {π : ιType u_2} [(i : ι) → TopologicalSpace (π i)] {s : Set ((i : ι) × π i)} :
      IsConnected s ∃ (i : ι) (t : Set (π i)), 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 : Set (π i)), IsPreconnected t s = Sigma.mk i '' t
      theorem Sum.isConnected_iff {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α β)} :
      IsConnected s (∃ (t : Set α), IsConnected t s = Sum.inl '' t) ∃ (t : Set β), IsConnected t s = Sum.inr '' t
      theorem Sum.isPreconnected_iff {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α β)} :
      IsPreconnected s (∃ (t : Set α), IsPreconnected t s = Sum.inl '' t) ∃ (t : Set β), 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
      Instances For
        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
        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 : xF) :
          theorem mem_connectedComponentIn {α : Type u} [TopologicalSpace α] {x : α} {F : Set α} (hx : x F) :
          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 IsPreconnected.subset_connectedComponent {α : Type u} [TopologicalSpace α] {x : α} {s : Set α} (H1 : IsPreconnected s) (H2 : x s) :
          theorem IsPreconnected.subset_connectedComponentIn {α : Type u} [TopologicalSpace α] {s : Set α} {x : α} {F : Set α} (hs : IsPreconnected s) (hxs : x s) (hsF : s F) :
          theorem IsConnected.subset_connectedComponent {α : Type u} [TopologicalSpace α] {x : α} {s : Set α} (H1 : IsConnected s) (H2 : x s) :
          theorem IsPreconnected.connectedComponentIn {α : Type u} [TopologicalSpace α] {x : α} {F : Set α} (h : IsPreconnected F) (hx : x F) :
          theorem connectedComponentIn_eq {α : Type u} [TopologicalSpace α] {x : α} {y : α} {F : Set α} (h : y connectedComponentIn F x) :
          theorem Continuous.image_connectedComponentIn_subset {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {a : α} (hf : Continuous f) (hx : a s) :
          theorem Continuous.mapsTo_connectedComponent {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (h : Continuous f) (a : α) :
          theorem Continuous.mapsTo_connectedComponentIn {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} (h : Continuous f) {a : α} (hx : a s) :
          theorem connectedComponentIn_mono {α : Type u} [TopologicalSpace α] (x : α) {F : Set α} {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.univ in a preconnected space is a preconnected set.

          Instances

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

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

            Instances

              A connected space is nonempty.

              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) :
              Equations
              • =
              theorem DenseRange.preconnectedSpace {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [PreconnectedSpace α] {f : αβ} (hf : DenseRange f) (hc : Continuous f) :
              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]
              Equations
              • =
              @[instance 100]
              Equations
              • =
              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 : απ i), 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 sIsOpen ts t = Set.univs.Nonemptyt.Nonempty(s t).Nonempty
              theorem isClopen_iff {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] {s : Set α} :
              IsClopen s s = s = Set.univ
              theorem IsClopen.eq_univ {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] {s : Set α} (h' : IsClopen s) (h : s.Nonempty) :
              s = Set.univ
              theorem subsingleton_of_disjoint_isClopen {α : Type u} {ι : Type u_1} [TopologicalSpace α] [PreconnectedSpace α] {s : ιSet α} (h_nonempty : ∀ (i : ι), (s i).Nonempty) (h_disj : Pairwise (Disjoint on s)) (h_clopen : ∀ (i : ι), IsClopen (s i)) :

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

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

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

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

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

              theorem frontier_eq_empty_iff {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] {s : Set α} :
              frontier s = s = s = Set.univ
              theorem nonempty_frontier_iff {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] {s : Set α} :
              (frontier s).Nonempty s.Nonempty s Set.univ
              theorem PreconnectedSpace.induction₂' {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] (P : ααProp) (h : ∀ (x : α), ∀ᶠ (y : α) in nhds x, P x y P y x) (h' : 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 : xs, ∀ᶠ (y : α) in nhdsWithin x s, P x y P y x) (h' : ∀ (x y z : α), x sy sz sP x yP y zP 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 : xs, ∀ᶠ (y : α) in nhdsWithin x s, P x y) (h' : ∀ (x y z : α), x sy sz sP x yP y zP x z) (h'' : ∀ (x y : α), x sy sP x yP 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 uIsOpen vs u vs (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 Uv U(s (u v)).Nonemptyu = v)(uU, IsOpen u)s ⋃₀ UuU, s u

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

              theorem disjoint_or_subset_of_isClopen {α : Type u} [TopologicalSpace α] {s : 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 uIsClosed vs u vs (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 uIsClosed vs u vDisjoint u vs 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) :
              theorem connectedComponent_subset_iInter_isClopen {α : Type u} [TopologicalSpace α] {x : α} :
              connectedComponent x ⋂ (Z : { Z : Set α // IsClopen Z x Z }), Z

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

              theorem IsClopen.biUnion_connectedComponent_eq {α : Type u} [TopologicalSpace α] {Z : Set α} (h : IsClopen Z) :
              xZ, 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 : β) :

              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 : α) :
              theorem QuotientMap.image_connectedComponent {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (hf : QuotientMap f) (h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})) (a : α) :

              The setoid of connected components of a topological space

              Equations
              Instances For

                The quotient of a space by its connected components

                Equations
                Instances For

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

                  Equations
                  • ConnectedComponents.mk = Quotient.mk''
                  Instances For
                    Equations
                    • ConnectedComponents.instCoeTC = { coe := ConnectedComponents.mk }
                    Equations
                    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

                    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) = xU, connectedComponent x

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

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

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

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

                    A PreconnectedSpace version of isPreconnected_of_forall_constant