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

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

    Alias of IsEmbedding.isTotallyDisconnected.

    @[deprecated IsEmbedding.isTotallyDisconnected_image]

    Alias of IsEmbedding.isTotallyDisconnected_image.

    @[deprecated IsEmbedding.isTotallyDisconnected_range]

    Alias of IsEmbedding.isTotallyDisconnected_range.

    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

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