Mathlib.Topology.Connected.LocallyConnected

LocallyConnectedSpace structure

(α : Type*) [TopologicalSpace α]

Full source

/-- 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`. -/
class LocallyConnectedSpace (α : Type*) [TopologicalSpace α] : Prop where
  /-- Open connected neighborhoods form a basis of the neighborhoods filter. -/
  open_connected_basis : ∀ x, (𝓝 x).HasBasis (fun s : Set α => IsOpenIsOpen s ∧ x ∈ s ∧ IsConnected s) id

Locally connected topological space

Informal description

A topological space $\alpha$ is called **locally connected** if for every point $x \in \alpha$, the neighborhood filter $\mathcal{N}(x)$ admits a basis consisting of connected open sets. This means that every neighborhood of $x$ contains a connected open neighborhood of $x$.

locallyConnectedSpace_iff_hasBasis_isOpen_isConnected theorem

: LocallyConnectedSpace α ↔ ∀ x, (𝓝 x).HasBasis (fun s : Set α => IsOpen s ∧ x ∈ s ∧ IsConnected s) id

Full source

theorem locallyConnectedSpace_iff_hasBasis_isOpen_isConnected :
    LocallyConnectedSpaceLocallyConnectedSpace α ↔
      ∀ x, (𝓝 x).HasBasis (fun s : Set α => IsOpen s ∧ x ∈ s ∧ IsConnected s) id :=
  ⟨@LocallyConnectedSpace.open_connected_basis _ _, LocallyConnectedSpace.mk⟩

Characterization of Locally Connected Spaces via Neighborhood Basis of Open Connected Sets

Informal description

A topological space $\alpha$ is locally connected if and only if for every point $x \in \alpha$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of open connected sets containing $x$. That is, for every $x \in \alpha$, a set $U$ is a neighborhood of $x$ if and only if there exists an open connected set $s$ such that $x \in s$ and $s \subseteq U$.

locallyConnectedSpace_iff_subsets_isOpen_isConnected theorem

 : LocallyConnectedSpace α ↔ ∀ x, ∀ U ∈ 𝓝 x, ∃ V : Set α, V ⊆ U ∧ IsOpen V ∧ x ∈ V ∧ IsConnected V

Full source

theorem locallyConnectedSpace_iff_subsets_isOpen_isConnected :
    LocallyConnectedSpaceLocallyConnectedSpace α ↔
      ∀ x, ∀ U ∈ 𝓝 x, ∃ V : Set α, V ⊆ U ∧ IsOpen V ∧ x ∈ V ∧ IsConnected V := by
  simp_rw [locallyConnectedSpace_iff_hasBasis_isOpen_isConnected]
  refine forall_congr' fun _ => ?_
  constructor
  · intro h U hU
    rcases h.mem_iff.mp hU with ⟨V, hV, hVU⟩
    exact ⟨V, hVU, hV⟩
  · exact fun h => ⟨fun U => ⟨fun hU =>
      let ⟨V, hVU, hV⟩ := h U hU
      ⟨V, hV, hVU⟩, fun ⟨V, ⟨hV, hxV, _⟩, hVU⟩ => mem_nhds_iff.mpr ⟨V, hVU, hV, hxV⟩⟩⟩

Characterization of Locally Connected Spaces via Open Connected Neighborhoods

Informal description

A topological space $\alpha$ is locally connected if and only if for every point $x \in \alpha$ and every neighborhood $U$ of $x$, there exists an open connected subset $V \subseteq U$ containing $x$.

DiscreteTopology.toLocallyConnectedSpace instance

(α) [TopologicalSpace α] [DiscreteTopology α] : LocallyConnectedSpace α

Full source

/-- A space with discrete topology is a locally connected space. -/
instance (priority := 100) DiscreteTopology.toLocallyConnectedSpace (α) [TopologicalSpace α]
    [DiscreteTopology α] : LocallyConnectedSpace α :=
  locallyConnectedSpace_iff_subsets_isOpen_isConnected.2 fun x _U hU =>
    ⟨{x}, singleton_subset_iff.2 <| mem_of_mem_nhds hU, isOpen_discrete _, rfl,
      isConnected_singleton⟩

Discrete Topological Spaces are Locally Connected

Informal description

Every topological space with the discrete topology is locally connected. That is, for any type $\alpha$ equipped with the discrete topology, the space $\alpha$ is locally connected, meaning every point has a neighborhood basis consisting of connected open sets.

connectedComponentIn_mem_nhds theorem

[LocallyConnectedSpace α] {F : Set α} {x : α} (h : F ∈ 𝓝 x) : connectedComponentIn F x ∈ 𝓝 x

Full source

theorem connectedComponentIn_mem_nhds [LocallyConnectedSpace α] {F : Set α} {x : α} (h : F ∈ 𝓝 x) :
    connectedComponentInconnectedComponentIn F x ∈ 𝓝 x := by
  rw [(LocallyConnectedSpace.open_connected_basis x).mem_iff] at h
  rcases h with ⟨s, ⟨h1s, hxs, h2s⟩, hsF⟩
  exact mem_nhds_iff.mpr ⟨s, h2s.isPreconnected.subset_connectedComponentIn hxs hsF, h1s, hxs⟩

Connected component in a neighborhood is a neighborhood in locally connected spaces

Informal description

Let $X$ be a locally connected topological space. For any point $x \in X$ and any neighborhood $F$ of $x$, the connected component of $x$ in $F$ is also a neighborhood of $x$.

IsOpen.connectedComponentIn theorem

[LocallyConnectedSpace α] {F : Set α} {x : α} (hF : IsOpen F) : IsOpen (connectedComponentIn F x)

Full source

protected theorem IsOpen.connectedComponentIn [LocallyConnectedSpace α] {F : Set α} {x : α}
    (hF : IsOpen F) : IsOpen (connectedComponentIn F x) := by
  rw [isOpen_iff_mem_nhds]
  intro y hy
  rw [connectedComponentIn_eq hy]
  exact connectedComponentIn_mem_nhds (hF.mem_nhds <| connectedComponentIn_subset F x hy)

Connected components in open sets are open in locally connected spaces

Informal description

Let $X$ be a locally connected topological space. For any open subset $F \subseteq X$ and any point $x \in F$, the connected component of $x$ in $F$ is an open set.

isOpen_connectedComponent theorem

[LocallyConnectedSpace α] {x : α} : IsOpen (connectedComponent x)

Full source

theorem isOpen_connectedComponent [LocallyConnectedSpace α] {x : α} :
    IsOpen (connectedComponent x) := by
  rw [← connectedComponentIn_univ]
  exact isOpen_univ.connectedComponentIn

Connected Components are Open in Locally Connected Spaces

Informal description

In a locally connected topological space $\alpha$, the connected component of any point $x \in \alpha$ is an open set.

isClopen_connectedComponent theorem

[LocallyConnectedSpace α] {x : α} : IsClopen (connectedComponent x)

Full source

theorem isClopen_connectedComponent [LocallyConnectedSpace α] {x : α} :
    IsClopen (connectedComponent x) :=
  ⟨isClosed_connectedComponent, isOpen_connectedComponent⟩

Connected Components are Clopen in Locally Connected Spaces

Informal description

In a locally connected topological space $\alpha$, the connected component of any point $x \in \alpha$ is both closed and open (i.e., clopen).

locallyConnectedSpace_iff_connectedComponentIn_open theorem

: LocallyConnectedSpace α ↔ ∀ F : Set α, IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)

Full source

theorem locallyConnectedSpace_iff_connectedComponentIn_open :
    LocallyConnectedSpaceLocallyConnectedSpace α ↔
      ∀ F : Set α, IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x) := by
  constructor
  · intro h
    exact fun F hF x _ => hF.connectedComponentIn
  · intro h
    rw [locallyConnectedSpace_iff_subsets_isOpen_isConnected]
    refine fun x U hU =>
        ⟨connectedComponentIn (interior U) x,
          (connectedComponentIn_subset _ _).trans interior_subset, h _ isOpen_interior x ?_,
          mem_connectedComponentIn ?_, isConnected_connectedComponentIn_iff.mpr ?_⟩ <;>
      exact mem_interior_iff_mem_nhds.mpr hU

Characterization of Locally Connected Spaces via Open Connected Components

Informal description

A topological space $\alpha$ is locally connected if and only if for every open subset $F \subseteq \alpha$ and every point $x \in F$, the connected component of $x$ in $F$ is an open set.

locallyConnectedSpace_iff_connected_subsets theorem

: LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Full source

theorem locallyConnectedSpace_iff_connected_subsets :
    LocallyConnectedSpaceLocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U := by
  constructor
  · rw [locallyConnectedSpace_iff_subsets_isOpen_isConnected]
    intro h x U hxU
    rcases h x U hxU with ⟨V, hVU, hV₁, hxV, hV₂⟩
    exact ⟨V, hV₁.mem_nhds hxV, hV₂.isPreconnected, hVU⟩
  · rw [locallyConnectedSpace_iff_connectedComponentIn_open]
    refine fun h U hU x _ => isOpen_iff_mem_nhds.mpr fun y hy => ?_
    rw [connectedComponentIn_eq hy]
    rcases h y U (hU.mem_nhds <| (connectedComponentIn_subset _ _) hy) with ⟨V, hVy, hV, hVU⟩
    exact Filter.mem_of_superset hVy (hV.subset_connectedComponentIn (mem_of_mem_nhds hVy) hVU)

Characterization of Locally Connected Spaces via Preconnected Neighborhoods

Informal description

A topological space $\alpha$ is locally connected if and only if for every point $x \in \alpha$ and every neighborhood $U$ of $x$, there exists a neighborhood $V$ of $x$ such that $V$ is preconnected and $V \subseteq U$.

locallyConnectedSpace_iff_connected_basis theorem

: LocallyConnectedSpace α ↔ ∀ x, (𝓝 x).HasBasis (fun s : Set α => s ∈ 𝓝 x ∧ IsPreconnected s) id

Full source

theorem locallyConnectedSpace_iff_connected_basis :
    LocallyConnectedSpaceLocallyConnectedSpace α ↔
      ∀ x, (𝓝 x).HasBasis (fun s : Set α => s ∈ 𝓝 x ∧ IsPreconnected s) id := by
  rw [locallyConnectedSpace_iff_connected_subsets]
  exact forall_congr' fun x => Filter.hasBasis_self.symm

Characterization of Locally Connected Spaces via Preconnected Neighborhood Basis

Informal description

A topological space $\alpha$ is locally connected if and only if for every point $x \in \alpha$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of preconnected sets that are neighborhoods of $x$. In other words, every neighborhood of $x$ contains a preconnected neighborhood of $x$.

locallyConnectedSpace_of_connected_bases theorem

 {ι : Type*} (b : α → ι → Set α) (p : α → ι → Prop) (hbasis : ∀ x, (𝓝 x).HasBasis (p x) (b x))
  (hconnected : ∀ x i, p x i → IsPreconnected (b x i)) : LocallyConnectedSpace α

Full source

theorem locallyConnectedSpace_of_connected_bases {ι : Type*} (b : α → ι → Set α) (p : α → ι → Prop)
    (hbasis : ∀ x, (𝓝 x).HasBasis (p x) (b x))
    (hconnected : ∀ x i, p x i → IsPreconnected (b x i)) : LocallyConnectedSpace α := by
  rw [locallyConnectedSpace_iff_connected_basis]
  exact fun x =>
    (hbasis x).to_hasBasis
      (fun i hi => ⟨b x i, ⟨(hbasis x).mem_of_mem hi, hconnected x i hi⟩, subset_rfl⟩) fun s hs =>
      ⟨(hbasis x).index s hs.1, ⟨(hbasis x).property_index hs.1, (hbasis x).set_index_subset hs.1⟩⟩

Sufficient Condition for Local Connectedness via Preconnected Neighborhood Bases

Informal description

Let $\alpha$ be a topological space, and for each point $x \in \alpha$, let $(b(x, i))_{i \in \iota}$ be a family of sets indexed by $\iota$ and $(p(x, i))_{i \in \iota}$ be a family of predicates on $\iota$. Suppose that for every $x \in \alpha$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of the sets $b(x, i)$ for which $p(x, i)$ holds. Furthermore, assume that for every $x \in \alpha$ and $i \in \iota$, if $p(x, i)$ holds, then the set $b(x, i)$ is preconnected. Then $\alpha$ is a locally connected space.

Topology.IsOpenEmbedding.locallyConnectedSpace theorem

[LocallyConnectedSpace α] [TopologicalSpace β] {f : β → α} (h : IsOpenEmbedding f) : LocallyConnectedSpace β

Full source

lemma Topology.IsOpenEmbedding.locallyConnectedSpace [LocallyConnectedSpace α] [TopologicalSpace β]
    {f : β → α} (h : IsOpenEmbedding f) : LocallyConnectedSpace β := by
  refine locallyConnectedSpace_of_connected_bases (fun _ s ↦ f ⁻¹' s)
    (fun x s ↦ (IsOpen s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) (fun x ↦ ?_)
    (fun x s hxs ↦ hxs.1.2.2.isPreconnected.preimage_of_isOpenMap h.injective h.isOpenMap hxs.2)
  rw [h.nhds_eq_comap]
  exact LocallyConnectedSpace.open_connected_basis (f x) |>.restrict_subset
    (h.isOpen_range.mem_nhds <| mem_range_self _) |>.comap _

Open Embeddings Preserve Local Connectedness

Informal description

Let $\alpha$ be a locally connected topological space and $\beta$ be a topological space. If $f \colon \beta \to \alpha$ is an open embedding, then $\beta$ is also locally connected.

IsOpen.locallyConnectedSpace theorem

[LocallyConnectedSpace α] {U : Set α} (hU : IsOpen U) : LocallyConnectedSpace U

Full source

theorem IsOpen.locallyConnectedSpace [LocallyConnectedSpace α] {U : Set α} (hU : IsOpen U) :
    LocallyConnectedSpace U :=
  hU.isOpenEmbedding_subtypeVal.locallyConnectedSpace

Open Subsets of Locally Connected Spaces are Locally Connected

Informal description

Let $\alpha$ be a locally connected topological space and $U$ be an open subset of $\alpha$. Then $U$ is also a locally connected space.