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) [TopologicalSpace α] : Prop

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 : α), Filter.HasBasis (nhds x) (fun (s : Set α) => IsOpen s ∧ x ∈ s ∧ IsConnected s) id

  Open connected neighborhoods form a basis of the neighborhoods filter.

theorem locallyConnectedSpace_iff_open_connected_basis {α : Type u} [TopologicalSpace α] : LocallyConnectedSpace α ↔ ∀ (x : α), Filter.HasBasis (nhds x) (fun (s : Set α) => IsOpen s ∧ x ∈ s ∧ IsConnected s) id

theorem locallyConnectedSpace_iff_open_connected_subsets {α : Type u} [TopologicalSpace α] : LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ nhds x, ∃ V ⊆ U, IsOpen V ∧ x ∈ V ∧ IsConnected V

instance DiscreteTopology.toLocallyConnectedSpace (α : Type u_3) [TopologicalSpace α] [DiscreteTopology α] : LocallyConnectedSpace α

A space with discrete topology is a locally connected space.

Equations

• ⋯ = ⋯

theorem connectedComponentIn_mem_nhds {α : Type u} [TopologicalSpace α] [LocallyConnectedSpace α] {F : Set α} {x : α} (h : F ∈ nhds x) : connectedComponentIn F x ∈ nhds x

theorem IsOpen.connectedComponentIn {α : Type u} [TopologicalSpace α] [LocallyConnectedSpace α] {F : Set α} {x : α} (hF : IsOpen F) : IsOpen (connectedComponentIn F x)

theorem isOpen_connectedComponent {α : Type u} [TopologicalSpace α] [LocallyConnectedSpace α] {x : α} : IsOpen (connectedComponent x)

theorem isClopen_connectedComponent {α : Type u} [TopologicalSpace α] [LocallyConnectedSpace α] {x : α} : IsClopen (connectedComponent x)

theorem locallyConnectedSpace_iff_connectedComponentIn_open {α : Type u} [TopologicalSpace α] : LocallyConnectedSpace α ↔ ∀ (F : Set α), IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)

theorem locallyConnectedSpace_iff_connected_subsets {α : Type u} [TopologicalSpace α] : LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ nhds x, ∃ V ∈ nhds x, IsPreconnected V ∧ V ⊆ U

theorem locallyConnectedSpace_iff_connected_basis {α : Type u} [TopologicalSpace α] : LocallyConnectedSpace α ↔ ∀ (x : α), Filter.HasBasis (nhds x) (fun (s : Set α) => s ∈ nhds x ∧ IsPreconnected s) id

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 i → IsPreconnected (b x i)) : LocallyConnectedSpace α

theorem OpenEmbedding.locallyConnectedSpace {α : Type u} {β : Type v} [TopologicalSpace α] [LocallyConnectedSpace α] [TopologicalSpace β] {f : β → α} (h : OpenEmbedding f) : LocallyConnectedSpace β

theorem IsOpen.locallyConnectedSpace {α : Type u} [TopologicalSpace α] [LocallyConnectedSpace α] {U : Set α} (hU : IsOpen U) : LocallyConnectedSpace ↑U