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

• open_connected_basis (x : α) : (nhds x).HasBasis (fun (s : Set α) => IsOpen s ∧ x ∈ s ∧ IsConnected s) id

  Open connected neighborhoods form a basis of the neighborhoods filter.

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

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

@[instance 100]

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

A space with discrete topology is a locally connected space.

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 : α), (nhds x).HasBasis (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 : α), (nhds x).HasBasis (p x) (b x)) (hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)) : LocallyConnectedSpace α

theorem TopologicalSpace.IsTopologicalBasis.isOpen_isPreconnected {α : Type u} [TopologicalSpace α] [LocallyConnectedSpace α] : IsTopologicalBasis {s : Set α | IsOpen s ∧ IsPreconnected s}

theorem locallyConnectedSpace_iff_isTopologicalBasis_isOpen_isPreconnected {α : Type u} [TopologicalSpace α] : LocallyConnectedSpace α ↔ TopologicalSpace.IsTopologicalBasis {s : Set α | IsOpen s ∧ IsPreconnected s}

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

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

theorem Topology.IsCoinducing.locallyConnectedSpace {α : Type u} {β : Type v} [TopologicalSpace α] [LocallyConnectedSpace α] [TopologicalSpace β] {f : α → β} (hf : IsCoinducing f) : LocallyConnectedSpace β

Any topology coinduced by a locally connected topology is locally connected.

instance instDiscreteTopologyConnectedComponentsOfLocallyConnectedSpace {α : Type u} [TopologicalSpace α] [LocallyConnectedSpace α] : DiscreteTopology (ConnectedComponents α)

If a space is locally connected, the topology of its connected components is discrete.

instance instFiniteConnectedComponentsOfLocallyConnectedSpaceOfCompactSpace {α : Type u} [TopologicalSpace α] [LocallyConnectedSpace α] [CompactSpace α] : Finite (ConnectedComponents α)

A locally connected compact space has finitely many connected components.

instance Prod.locallyConnectedSpace {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [LocallyConnectedSpace α] [LocallyConnectedSpace β] : LocallyConnectedSpace (α × β)

The product of two locally connected spaces is locally connected.

theorem Pi.locallyConnectedSpace_of_finite_not_preconnectedSpace {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), LocallyConnectedSpace (X i)] (hfinite : {i : ι | ¬PreconnectedSpace (X i)}.Finite) : LocallyConnectedSpace ((i : ι) → X i)

If each X i is locally connected and all but finitely many are preconnected, then ∀ i, X i is locally connected.

instance Pi.locallyConnectedSpace_of_finite {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), LocallyConnectedSpace (X i)] : LocallyConnectedSpace ((i : ι) → X i)

A finite product of locally connected spaces is locally connected.

instance Pi.locallyConnectedSpace {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), LocallyConnectedSpace (X i)] [∀ (i : ι), PreconnectedSpace (X i)] : LocallyConnectedSpace ((i : ι) → X i)

A product of preconnected, locally connected spaces is locally connected. Note that an arbitrary product of locally connected spaces need not be locally connected, so the preconnectedness assumption cannot be dropped entirely (though it can be dropped for finitely many factors, see Pi.locallyConnectedSpace_of_finite_not_preconnectedSpace).

theorem Pi.locallyConnectedSpace_iff {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] : LocallyConnectedSpace ((i : ι) → X i) ↔ IsEmpty ((i : ι) → X i) ∨ (∀ (i : ι), LocallyConnectedSpace (X i)) ∧ {i : ι | ¬PreconnectedSpace (X i)}.Finite

A product of spaces is locally connected iff it is empty, or every factor is locally connected and all but finitely many factors are preconnected.