locallyConnectedSpace_iff_open_connected_subsets
theorem locallyConnectedSpace_iff_open_connected_subsets :
∀ {α : Type u} [inst : TopologicalSpace α],
LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ nhds x, ∃ V ⊆ U, IsOpen V ∧ x ∈ V ∧ IsConnected V
This theorem states that for any type `α` with a topological space structure, `α` is a locally connected space if and only if for every point `x` in `α`, and every neighborhood `U` of `x`, there exists a subset `V` of `U` which is not only open and contains `x`, but is also connected. In mathematical terms, a space is locally connected at a point `x` if all neighbourhoods of `x` contain an open connected subset containing `x`. This property should hold for all points in the space for it to be considered a locally connected space.
More concisely: A topological space `α` is locally connected if for every point `x` in `α`, there exists an open and connected neighborhood `V` of `x`.
|
LocallyConnectedSpace.open_connected_basis
theorem LocallyConnectedSpace.open_connected_basis :
∀ {α : Type u_3} [inst : TopologicalSpace α] [self : LocallyConnectedSpace α] (x : α),
(nhds x).HasBasis (fun s => IsOpen s ∧ x ∈ s ∧ IsConnected s) id
This theorem states that in a locally connected space (a topological space where each point has a base of connected neighborhoods), every neighborhood filter, the set of all neighborhoods of a given point `x`, has a basis consisting of open, connected neighborhoods containing `x`. In other words, each neighborhood of `x` can be generated by taking unions of these basis neighborhoods. A neighborhood is a set that contains an open set around `x`, and a set is considered connected if it is nonempty and there are no non-trivial open partitions of it.
More concisely: In a locally connected space, every neighborhood of a point has a basis of open, connected sets.
|
locallyConnectedSpace_of_connected_bases
theorem locallyConnectedSpace_of_connected_bases :
∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} (b : α → ι → Set α) (p : α → ι → Prop),
(∀ (x : α), (nhds x).HasBasis (p x) (b x)) →
(∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)) → LocallyConnectedSpace α
The theorem `locallyConnectedSpace_of_connected_bases` states that for any type `α` equipped with a `TopologicalSpace` instance, and any indexing type `ι`, given a family of sets `b` indexed by `α` and `ι`, and a property `p` dependent on `α` and `ι`, under the conditions that for every `x` in `α`, the neighborhood filter `nhds x` has a basis given by the sets `b x i` for which `p x i` holds, and for each `x` in `α` and `i` in `ι`, if `p x i` holds, then `b x i` is preconnected, then `α` is a locally connected space. In simpler terms, if a topological space has a basis of preconnected sets for every point's neighborhood filter, then it is a locally connected space.
More concisely: If for every point in a topological space and every neighborhood filter, there exists a basis of preconnected sets, then the space is locally connected.
|
isOpen_connectedComponent
theorem isOpen_connectedComponent :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LocallyConnectedSpace α] {x : α},
IsOpen (connectedComponent x)
The theorem `isOpen_connectedComponent` states that for any type `α` that is equipped with a topological space structure and a locally connected space structure, and for any point `x` of type `α`, the connected component of `x` is open in the ambient topological space. Here, the connected component of `x` is defined as the union of all preconnected sets containing `x`, and a set is considered open in a topological space if it belongs to the collection of open sets which defines the topology. This theorem is fundamental in the study of topological spaces and their properties.
More concisely: For any topological space $(X,\tau)$ with a locally connected subspace structure, the connected component of a point $x\in X$ is an open set in $X$.
|