Documentation

Mathlib.Topology.Connected.TotallyDisconnected

Totally disconnected and totally separated topological spaces #

Main definitions #

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

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

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

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
Instances For

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

    Instances

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

      theorem IsPreconnected.subsingleton {α : Type u} [TopologicalSpace α] [TotallyDisconnectedSpace α] {s : Set α} (h : IsPreconnected s) :
      s.Subsingleton
      instance Pi.totallyDisconnectedSpace {α : Type u_3} {β : αType u_4} [(a : α) → TopologicalSpace (β a)] [∀ (a : α), TotallyDisconnectedSpace (β a)] :
      TotallyDisconnectedSpace ((a : α) → β a)
      Equations
      • =
      instance instTotallyDisconnectedSpaceSigma {ι : Type u_1} {π : ιType u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), TotallyDisconnectedSpace (π i)] :
      TotallyDisconnectedSpace ((i : ι) × π i)
      Equations
      • =
      theorem isTotallyDisconnected_of_isClopen_set {X : Type u_3} [TopologicalSpace X] (hX : Pairwise fun (x y : X) => ∃ (U : Set X), IsClopen U x U yU) :

      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.

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

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

      @[simp]
      theorem Continuous.image_connectedComponent_eq_singleton {α : Type u} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : αβ} (h : Continuous f) (a : α) :

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

      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)) :
      theorem Embedding.isTotallyDisconnected {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (hf : Embedding f) {s : Set α} (h : IsTotallyDisconnected (f '' s)) :
      def IsTotallySeparated {α : Type u} [TopologicalSpace α] (s : Set α) :

      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
      Instances For

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

        • isTotallySeparated_univ : IsTotallySeparated Set.univ

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

        Instances

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

          @[instance 100]
          Equations
          • =
          theorem totallySeparatedSpace_iff_exists_isClopen {α : Type u_3} [TopologicalSpace α] :
          TotallySeparatedSpace α ∀ (x y : α), x y∃ (U : Set α), IsClopen U x U y U
          theorem exists_isClopen_of_totally_separated {α : Type u_3} [TopologicalSpace α] [TotallySeparatedSpace α] {x : α} {y : α} (hxy : x y) :
          ∃ (U : Set α), IsClopen U x U y U
          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

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

          Equations
          Instances For
            theorem Continuous.connectedComponentsLift_continuous {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : αβ} (h : Continuous f) :
            Continuous h.connectedComponentsLift
            @[simp]
            theorem Continuous.connectedComponentsLift_apply_coe {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : αβ} (h : Continuous f) (x : α) :
            h.connectedComponentsLift (ConnectedComponents.mk x) = f x
            @[simp]
            theorem Continuous.connectedComponentsLift_comp_coe {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : αβ} (h : Continuous f) :
            h.connectedComponentsLift 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 = h.connectedComponentsLift

            Functoriality of connectedComponents

            Equations
            • h.connectedComponentsMap = .connectedComponentsLift
            Instances For
              theorem Continuous.connectedComponentsMap_continuous {α : Type u} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] {f : αβ} (h : Continuous f) :
              Continuous h.connectedComponentsMap
              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 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 IsPreconnected.constant_of_mapsTo {α : Type u} [TopologicalSpace α] {S : Set α} (hS : IsPreconnected S) {β : Type u_3} [TopologicalSpace β] {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} [TopologicalSpace α] {S : Set α} (hS : IsPreconnected S) {β : Type u_3} [TopologicalSpace β] {T : Set β} [DiscreteTopology T] {f : αβ} (hc : ContinuousOn f S) (hTm : Set.MapsTo f S T) (hne : T.Nonempty) :
              yT, 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.