Continuous.image_connectedComponent_eq_singleton
theorem Continuous.image_connectedComponent_eq_singleton :
∀ {α : Type u} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β]
[inst_2 : TotallyDisconnectedSpace β] {f : α → β}, Continuous f → ∀ (a : α), f '' connectedComponent a = {f a}
The theorem states that for any point in a topological space, if we have a continuous function mapping this space to a totally disconnected space, the image of the connected component of the point under this function is a singleton set consisting only of the image of the point itself. In other words, no other point in the connected component maps to the same place as the given point under the continuous function. This theorem highlights the isolation of points in a totally disconnected space.
More concisely: Given any continuous function from a topological space to a totally disconnected space and any point in the space, the image of the connected component of that point is a singleton set consisting only of the image of that point.
|
totallyDisconnectedSpace_iff_connectedComponent_subsingleton
theorem totallyDisconnectedSpace_iff_connectedComponent_subsingleton :
∀ {α : Type u} [inst : TopologicalSpace α],
TotallyDisconnectedSpace α ↔ ∀ (x : α), (connectedComponent x).Subsingleton
The theorem states that a topological space is totally disconnected if and only if its connected components are subsingletons. In terms of topology, a space is said to be totally disconnected if there are no connected subsets with more than one point, i.e., for any point in the space, the largest connected set containing that point (the connected component) is a subsingleton (has at most one element).
More concisely: A topological space is totally disconnected if and only if each of its connected components is a subsingleton.
|
isTotallyDisconnected_of_isClopen_set
theorem isTotallyDisconnected_of_isClopen_set :
∀ {X : Type u_3} [inst : TopologicalSpace X],
(Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U) → IsTotallyDisconnected Set.univ
The theorem `isTotallyDisconnected_of_isClopen_set` states that: in any topological space `X`, if for every pair of distinct points `x` and `y` in `X`, there exists a set `U` that is both closed and open (also known as clopen) such that `x` is in `U` and `y` is not in `U`, then `X` is totally disconnected. A topological space is said to be totally disconnected if every subset `t` of `X` that is preconnected (i.e., cannot be represented as the union of two disjoint nonempty open sets) is either a singleton or an empty set. Here, `Set.univ` represents the universal set, which contains all the elements of `X`.
More concisely: If for every pair of distinct points in a topological space, there exists a clopen set separating them, then the space is totally disconnected.
|
connectedComponent_eq_singleton
theorem connectedComponent_eq_singleton :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : TotallyDisconnectedSpace α] (x : α),
connectedComponent x = {x}
This theorem states that for any point `x` in a totally disconnected topological space, the connected component of `x` is just the singleton set containing `x` itself. In other words, in a totally disconnected space, each point forms its own separate connected component, as there are no connections between different points.
More concisely: In a totally disconnected topological space, each point is the connected component of itself.
|
TotallySeparatedSpace.isTotallySeparated_univ
theorem TotallySeparatedSpace.isTotallySeparated_univ :
∀ {α : Type u} [inst : TopologicalSpace α] [self : TotallySeparatedSpace α], IsTotallySeparated Set.univ
The theorem `TotallySeparatedSpace.isTotallySeparated_univ` states that for any type `α` equipped with a topology (i.e., a topological space), if this space is totally separated (as defined by the `TotallySeparatedSpace` structure), then the universal set in this space, denoted by `Set.univ`, is also totally separated. In other words, any two distinct points in the whole space can be separated by two disjoint open sets that cover the whole space.
More concisely: If `α` is a topological space with the `TotallySeparatedSpace` structure, then any two distinct points in `α` can be separated by two disjoint open sets that cover `Set.univ`.
|
IsPreconnected.constant
theorem IsPreconnected.constant :
∀ {α : Type u} [inst : TopologicalSpace α] {Y : Type u_3} [inst_1 : TopologicalSpace Y]
[inst_2 : DiscreteTopology Y] {s : Set α},
IsPreconnected s → ∀ {f : α → Y}, ContinuousOn f s → ∀ {x y : α}, x ∈ s → y ∈ s → f x = f y
This theorem states that for a preconnected set `s` in a topological space `α`, any function `f` from `α` to a discrete topological space `Y` that is continuous on `s` must be constant on `s`. In other words, if `x` and `y` are any two points in `s`, then the value of `f` at `x` is equal to the value of `f` at `y`. This theorem encapsulates the property of preconnected sets that they can't be 'broken apart' by continuous functions into the discrete space.
More concisely: If `s` is a preconnected subset of a topological space `α` and `f : α → Y` is a continuous function with discrete domain `Y`, then `f` is constant on `s`.
|
TotallyDisconnectedSpace.isTotallyDisconnected_univ
theorem TotallyDisconnectedSpace.isTotallyDisconnected_univ :
∀ {α : Type u} [inst : TopologicalSpace α] [self : TotallyDisconnectedSpace α], IsTotallyDisconnected Set.univ := by
sorry
The theorem `TotallyDisconnectedSpace.isTotallyDisconnected_univ` states that for any type `α` equipped with a topological space structure and a condition that it is totally disconnected (as defined by `TotallyDisconnectedSpace α`), the universal set (which includes all elements of `α`) is also totally disconnected. In other words, in such a totally disconnected space, every subset of the universal set that is preconnected (meaning it cannot be represented as a union of two disjoint nonempty closed subsets) is a subsingleton (i.e., it is either empty or consists of a single point).
More concisely: In a totally disconnected topological space, every preconnected subset is a subsingleton.
|
IsPreconnected.subsingleton
theorem IsPreconnected.subsingleton :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : TotallyDisconnectedSpace α] {s : Set α},
IsPreconnected s → s.Subsingleton
The theorem `IsPreconnected.subsingleton` states that for any type `α` that has a structure of a topological space and is a totally disconnected space, and for any set `s` of type `α`, if `s` is preconnected, then `s` is a subsingleton. In other words, if a set in a totally disconnected topological space is preconnected (meaning there is no non-trivial open partition of it), then it must contain at most one element, which is the definition of being a subsingleton.
More concisely: In a totally disconnected topological space, a preconnected subset is a subsingleton.
|
totallyDisconnectedSpace_iff_connectedComponent_singleton
theorem totallyDisconnectedSpace_iff_connectedComponent_singleton :
∀ {α : Type u} [inst : TopologicalSpace α], TotallyDisconnectedSpace α ↔ ∀ (x : α), connectedComponent x = {x} := by
sorry
This theorem states that a topological space is totally disconnected if and only if its connected components are singletons. More specifically, for any type `α` that represents a topological space, the space is totally disconnected (meaning that there does not exist a connected subset with more than one element) if and only if for all points `x` in the space, the connected component of `x` (which is the largest connected set containing `x`) is equal to the set containing `x` alone. This means that each point in the space forms a separate connected component by itself.
More concisely: A topological space is totally disconnected if and only if every point belongs to a connected subset that is equal to the singleton set containing that point.
|
IsPreconnected.eqOn_const_of_mapsTo
theorem IsPreconnected.eqOn_const_of_mapsTo :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {S : Set α},
IsPreconnected S →
∀ {T : Set β} [inst_2 : DiscreteTopology ↑T] {f : α → β},
ContinuousOn f S → Set.MapsTo f S T → T.Nonempty → ∃ y ∈ T, Set.EqOn f (Function.const α y) S
This theorem states that given two topological spaces `α` and `β`, a set `S` in `α` that is preconnected, a continuous function `f` from `α` to `β`, and a nonempty set `T` in `β` such that `f` maps `S` to `T`, there exists some element `y` in `T` such that `f` is equal to the constant function `Function.const α y` on `S`. In other words, if we have a continuous function whose image on a preconnected set is contained within a certain set, then the function must be constant on that preconnected set, taking the value of some element in the target set.
More concisely: Given a preconnected set S in topological space α, a continuous function f from α to β mapping S to a nonempty set T, there exists an element y in T such that f restricts to the constant function with value y on S.
|
IsTotallySeparated.isTotallyDisconnected
theorem IsTotallySeparated.isTotallyDisconnected :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsTotallySeparated s → IsTotallyDisconnected s
The theorem `IsTotallySeparated.isTotallyDisconnected` states that for any set `s` of a given type `α` within a topological space, if `s` is totally separated, then `s` is also totally disconnected. Here, a set is said to be totally separated if any two distinct points in the set can be separated by two disjoint open sets that together cover the entire set. A set is said to be totally disconnected if every subset of the set that is preconnected (meaning, intuitively, that there are no 'holes' in the subset) contains at most one element.
More concisely: If a set in a topological space is totally separated, then it is also totally disconnected.
|
IsPreconnected.constant_of_mapsTo
theorem IsPreconnected.constant_of_mapsTo :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {S : Set α},
IsPreconnected S →
∀ {T : Set β} [inst_2 : DiscreteTopology ↑T] {f : α → β},
ContinuousOn f S → Set.MapsTo f S T → ∀ {x y : α}, x ∈ S → y ∈ S → f x = f y
This theorem, `IsPreconnected.constant_of_mapsTo`, states that given two topological spaces `α` and `β` and a set `S` in `α` that is preconnected (i.e., it cannot be partitioned into two non-empty open sets), if a function `f` from `α` to `β` is continuous on `S` and the image of `S` under `f` is contained in a set `T` in `β` that has a discrete topology, then for any two elements `x` and `y` in `S`, the function values `f(x)` and `f(y)` are equal. In simpler terms, if a continuous function maps a preconnected set into a discrete subset of the target space, then the function must be constant on that set.
More concisely: If a preconnected set in a topological space is mapped continuously to a discrete subset of another topological space, then the function restricts to a constant map on the preconnected set.
|
PreconnectedSpace.constant
theorem PreconnectedSpace.constant :
∀ {α : Type u} [inst : TopologicalSpace α] {Y : Type u_3} [inst_1 : TopologicalSpace Y]
[inst_2 : DiscreteTopology Y], PreconnectedSpace α → ∀ {f : α → Y}, Continuous f → ∀ {x y : α}, f x = f y
This theorem states that for any topological space `α` and any discrete topological space `Y`, if `α` is preconnected and `f` is a continuous function from `α` to `Y`, then the function `f` will produce the same output for any two inputs `x` and `y` from `α`. This is a version of `isPreconnected.constant` theorem specialized for `PreconnectedSpace`.
More concisely: For any preconnected topological space `α` and any continuous function `f` from `α` to a discrete space `Y`, if `x` and `y` are in `α`, then `f(x) = f(y)`.
|