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

class LocallyConnectedSpace (α : Type u_3) [] :

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.

• open_connected_basis : ∀ (x : α), (nhds x).HasBasis (fun (s : Set α) => x s ) id

Open connected neighborhoods form a basis of the neighborhoods filter.

Instances
theorem LocallyConnectedSpace.open_connected_basis {α : Type u_3} [] [self : ] (x : α) :
(nhds x).HasBasis (fun (s : Set α) => x s ) id

Open connected neighborhoods form a basis of the neighborhoods filter.

theorem locallyConnectedSpace_iff_open_connected_basis {α : Type u} [] :
∀ (x : α), (nhds x).HasBasis (fun (s : Set α) => x s ) id
theorem locallyConnectedSpace_iff_open_connected_subsets {α : Type u} [] :
∀ (x : α), Unhds x, VU, x V
@[instance 100]

A space with discrete topology is a locally connected space.

Equations
• =
theorem connectedComponentIn_mem_nhds {α : Type u} [] {F : Set α} {x : α} (h : F nhds x) :
theorem IsOpen.connectedComponentIn {α : Type u} [] {F : Set α} {x : α} (hF : ) :
theorem isOpen_connectedComponent {α : Type u} [] {x : α} :
theorem isClopen_connectedComponent {α : Type u} [] {x : α} :
theorem locallyConnectedSpace_iff_connectedComponentIn_open {α : Type u} [] :
∀ (F : Set α), xF,
theorem locallyConnectedSpace_iff_connected_subsets {α : Type u} [] :
∀ (x : α), Unhds x, Vnhds x, V U
theorem locallyConnectedSpace_iff_connected_basis {α : Type u} [] :
∀ (x : α), (nhds x).HasBasis (fun (s : Set α) => s nhds x ) id
theorem locallyConnectedSpace_of_connected_bases {α : Type u} [] {ι : Type u_3} (b : αιSet α) (p : αιProp) (hbasis : ∀ (x : α), (nhds x).HasBasis (p x) (b x)) (hconnected : ∀ (x : α) (i : ι), p x iIsPreconnected (b x i)) :
theorem OpenEmbedding.locallyConnectedSpace {α : Type u} {β : Type v} [] [] {f : βα} (h : ) :
theorem IsOpen.locallyConnectedSpace {α : Type u} [] {U : Set α} (hU : ) :