Uniform local connectedness

A set s in a pseudometric space is uniformly locally connected when the connected sets joining nearby points can be chosen small at a rate independent of where they are: for every ε > 0 there is a single δ > 0 such that any two points of s at distance less than δ lie in a connected subset of s of diameter at most ε.

This is the metric strengthening of local connectedness, and the two notions are equivalent on a compact set. That equivalence is what this file proves: IsCompact.isUniformlyLocallyConnected derives the uniform statement from the local one by a Lebesgue-number argument, and TauCeti.IsUniformlyLocallyConnected.locallyConnectedSpace returns from the uniform statement to the local one with no compactness at all.

Compactness is genuinely needed for the first direction. The graph of x ↦ sin (1 / x) over (0, 1] is homeomorphic to an interval, hence locally connected, but not uniformly so: the oscillations crowd together as x → 0, so two points of equal ordinate on distinct oscillations come arbitrarily close to one another, while every connected subset of the graph joining them sweeps out a whole oscillation and so meets ordinates near both 1 and -1. Such a set has diameter at least 2, so no δ works for ε = 1. It fails no hypothesis but compactness.

Why this notion

Local connectedness is a statement about one point at a time, and an argument that must produce a small connected set near every point of a set at once cannot use it directly. The uniform form is what such arguments actually consume, and on a compact set it costs nothing extra.

The intended consumer is layer L5 of the conformal-mapping roadmap (TauCetiRoadmap/ConformalMapping/README.md), Carathéodory's boundary correspondence. The sufficiency half of Carathéodory's continuity theorem — a conformal map of the disc onto a bounded domain with locally connected boundary extends continuously to the closed disc — controls the image of a crosscut, and what it asks of the boundary is exactly a uniform ε–δ supply of small connected sets joining nearby boundary points. The boundary of a bounded domain is compact, so the equivalence proved here converts the roadmap's hypothesis into that form once and for all; the conformal consequences are in TauCeti/Analysis/Complex/Conformal/Jordan/Domain.lean and TauCeti/Analysis/Complex/Conformal/LocallyConnectedBoundary.lean.

Nothing here is specific to that application: the definition and both implications are stated for an arbitrary pseudometric space. Mathlib has LocallyConnectedSpace but no metric refinement of it, and no Lebesgue-number consequence of this shape.

Main definitions

• TauCeti.IsUniformlyLocallyConnected — the uniform ε–δ form of local connectedness for a set in a pseudometric space.

Main results

• IsCompact.isUniformlyLocallyConnected — a compact locally connected set is uniformly locally connected.
• TauCeti.IsUniformlyLocallyConnected.locallyConnectedSpace — a uniformly locally connected set is locally connected; no compactness is used.
• TauCeti.IsUniformlyLocallyConnected.exists_isConnected_superset — a small enough subset is enclosed in a small connected subset, at a rate independent of the subset.
• IsCompact.isUniformlyLocallyConnected_iff — on a compact set the two notions agree.
• Convex.isUniformlyLocallyConnected — a convex set in a real normed space is uniformly locally connected, with the joining segment as the connected set.
• TauCeti.isUniformlyLocallyConnected_image_of_isCompact — a continuous image of a compact, locally connected set is uniformly locally connected.

References

• R. L. Moore, Foundations of Point Set Theory, Ch. IV (uniform local connectedness, "property S").
• J. G. Hocking and G. S. Young, Topology, Ch. 3.
• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 2 (the use in Carathéodory's continuity theorem).

def TauCeti.IsUniformlyLocallyConnected {X : Type u_1} [PseudoMetricSpace X] (s : Set X) : Prop

A set s is uniformly locally connected if for every ε > 0 there is a δ > 0 such that any two points of s at distance less than δ are joined by a connected subset of s of diameter at most ε.

The smallness of the joining set is spelled out as a pairwise distance bound rather than as Metric.diam C ≤ ε, because Metric.diam is 0 on an unbounded set, which would let an unbounded C satisfy the condition vacuously. The lemma TauCeti.IsUniformlyLocallyConnected.exists_isConnected_diam_le recovers the diameter phrasing, boundedness of the joining set being one of its consequences.

Equations

• TauCeti.IsUniformlyLocallyConnected s = ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, ∀ b ∈ s, dist a b < δ → ∃ C ⊆ s, IsConnected C ∧ a ∈ C ∧ b ∈ C ∧ ∀ x ∈ C, ∀ y ∈ C, dist x y ≤ ε

theorem TauCeti.isUniformlyLocallyConnected_def {X : Type u_1} [PseudoMetricSpace X] {s : Set X} : IsUniformlyLocallyConnected s ↔ ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, ∀ b ∈ s, dist a b < δ → ∃ C ⊆ s, IsConnected C ∧ a ∈ C ∧ b ∈ C ∧ ∀ x ∈ C, ∀ y ∈ C, dist x y ≤ ε

TauCeti.IsUniformlyLocallyConnected restated as an Iff, so that it can be established and consumed in its native pairwise-distance form without unfolding the definition — which downstream modules cannot do, the definition being public but not exposed.

theorem TauCeti.IsUniformlyLocallyConnected.exists_isConnected {X : Type u_1} [PseudoMetricSpace X] {s : Set X} (h : IsUniformlyLocallyConnected s) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ a ∈ s, ∀ b ∈ s, dist a b < δ → ∃ C ⊆ s, IsConnected C ∧ a ∈ C ∧ b ∈ C ∧ ∀ x ∈ C, ∀ y ∈ C, dist x y ≤ ε

The elimination form of TauCeti.IsUniformlyLocallyConnected: each ε > 0 comes with a δ > 0 serving every pair of points of s at distance less than δ at once.

theorem TauCeti.IsUniformlyLocallyConnected.exists_isConnected_diam_le {X : Type u_1} [PseudoMetricSpace X] {s : Set X} (h : IsUniformlyLocallyConnected s) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ a ∈ s, ∀ b ∈ s, dist a b < δ → ∃ C ⊆ s, IsConnected C ∧ a ∈ C ∧ b ∈ C ∧ Bornology.IsBounded C ∧ Metric.diam C ≤ ε

The diameter phrasing of TauCeti.IsUniformlyLocallyConnected: the joining set is bounded and has diameter at most ε.

theorem TauCeti.isUniformlyLocallyConnected_iff_exists_isConnected_diam_le {X : Type u_1} [PseudoMetricSpace X] {s : Set X} : IsUniformlyLocallyConnected s ↔ ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, ∀ b ∈ s, dist a b < δ → ∃ C ⊆ s, IsConnected C ∧ a ∈ C ∧ b ∈ C ∧ Bornology.IsBounded C ∧ Metric.diam C ≤ ε

TauCeti.IsUniformlyLocallyConnected is equivalent to its diameter phrasing: it may be established, and not just used, from joining sets that are bounded and of diameter at most ε.

theorem TauCeti.IsUniformlyLocallyConnected.exists_isConnected_superset {X : Type u_1} [PseudoMetricSpace X] {s : Set X} (h : IsUniformlyLocallyConnected s) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ t ⊆ s, Bornology.IsBounded t → t.Nonempty → Metric.diam t < δ → ∃ S ⊆ s, IsConnected S ∧ t ⊆ S ∧ Metric.diam S ≤ ε

A uniformly locally connected set encloses each of its small subsets in a small connected set. For every ε > 0 there is a single δ > 0 — depending on s and ε alone — such that every nonempty bounded subset of s of diameter less than δ is contained in a connected subset of s of diameter at most ε.

This upgrades the two-point statement TauCeti.IsUniformlyLocallyConnected.exists_isConnected from a pair of points to a whole small set, one connected set swallowing the subset entirely. The δ produced is the two-point modulus of ε / 2, not of ε: the enclosing set is reached from the fixed point a below, so each of its points is allowed only half of the budget.

The enclosing set is built by taking every candidate at once, as in TauCeti.IsUniformlyLocallyConnected.locallyConnectedSpace: fix a point a of the subset and unite every preconnected subset of s that contains a and stays within ε / 2 of it.

@[simp]

theorem TauCeti.isUniformlyLocallyConnected_empty {X : Type u_1} [PseudoMetricSpace X] : IsUniformlyLocallyConnected ∅

The empty set is uniformly locally connected, vacuously.

theorem Convex.isUniformlyLocallyConnected {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {t : Set E} (ht : Convex ℝ t) : TauCeti.IsUniformlyLocallyConnected t

A convex set is uniformly locally connected: two points at distance less than ε / 2 are joined by the segment between them, which stays in the set by convexity and, by segment_subset_closedBall_left, inside the closed ball of radius dist a b < ε / 2 about the first endpoint, so its points are pairwise within ε.

This is the basic example, and the one the closed disc supplies in the conformal application.

The compact case: local connectedness suffices

theorem IsCompact.isUniformlyLocallyConnected {X : Type u_1} [PseudoMetricSpace X] {s : Set X} [LocallyConnectedSpace ↑s] (hs : IsCompact s) : TauCeti.IsUniformlyLocallyConnected s

A compact locally connected set is uniformly locally connected.

Given ε > 0, local connectedness supplies for each point a connected open neighbourhood inside the ball of radius ε / 2 about it — the connected component of that ball, open precisely because the subspace is locally connected. These cover the compact set, and a Lebesgue number δ for the cover does the rest: two points at distance less than δ lie in a common ball of radius δ, hence in a common member of the cover, whose points are pairwise within ε of one another.

The converse: uniform local connectedness implies local connectedness

theorem TauCeti.IsUniformlyLocallyConnected.locallyConnectedSpace {X : Type u_1} [PseudoMetricSpace X] {s : Set X} (h : IsUniformlyLocallyConnected s) : LocallyConnectedSpace ↑s

A uniformly locally connected set is locally connected. No compactness is needed.

The connected neighbourhood of a point x of s inside a prescribed ball is built by taking all candidates at once: the union of every connected subset of s that contains x and stays within ε / 2 of it. The union is connected because all its members contain x, it stays inside the ball of radius ε about x, and it is a neighbourhood of x in s because the uniform hypothesis puts every point within δ of x into one of the sets being united.

theorem IsCompact.isUniformlyLocallyConnected_iff {X : Type u_1} [PseudoMetricSpace X] {s : Set X} (hs : IsCompact s) : TauCeti.IsUniformlyLocallyConnected s ↔ LocallyConnectedSpace ↑s

On a compact set, uniform local connectedness and local connectedness agree. The forward implication is TauCeti.IsUniformlyLocallyConnected.locallyConnectedSpace, which needs no compactness; the backward one is IsCompact.isUniformlyLocallyConnected, which does.

Continuous images

theorem TauCeti.isUniformlyLocallyConnected_image_of_isCompact {X : Type u_1} [PseudoMetricSpace X] {Z : Type u_2} [TopologicalSpace Z] [T2Space X] {t : Set Z} {g : Z → X} [LocallyConnectedSpace ↑t] (ht : IsCompact t) (hg : ContinuousOn g t) : IsUniformlyLocallyConnected (g '' t)

A continuous image of a compact, locally connected set is uniformly locally connected. The uniform companion of TauCeti.locallyConnectedSpace_image_of_isCompact: that lemma makes the image locally connected, the image is compact, and on a compact set the two notions agree.