Structures · Topology

LocallyConnectedSpace

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

Defined in

Mathlib.Topology.Connected.LocallyConnected

Shape

One type argument · adds open_connected_basis