Documentation

Mathlib.Topology.Connected.LocallyConnected

Locally connected topological spaces #

A topological space is locally connected if each neighborhood filter admits a basis of connected open sets. Local connectivity is equivalent to each point having a basis of connected (not necessarily open) sets --- but in a non-trivial way, so we choose this definition and prove the equivalence later in locallyConnectedSpace_iff_connected_basis.

A topological space is locally connected if each neighborhood filter admits a basis of connected open sets. Note that it is equivalent to each point having a basis of connected (non necessarily open) sets but in a non-trivial way, so we choose this definition and prove the equivalence later in locallyConnectedSpace_iff_connected_basis.

Instances

    A space with discrete topology is a locally connected space.

    Equations
    theorem locallyConnectedSpace_iff_connected_subsets {α : Type u} [TopologicalSpace α] :
    LocallyConnectedSpace α ∀ (x : α), Unhds x, ∃ V ∈ nhds x, IsPreconnected V V U
    theorem locallyConnectedSpace_of_connected_bases {α : Type u} [TopologicalSpace α] {ι : Type u_3} (b : αιSet α) (p : αιProp) (hbasis : ∀ (x : α), Filter.HasBasis (nhds x) (p x) (b x)) (hconnected : ∀ (x : α) (i : ι), p x iIsPreconnected (b x i)) :