Cluster sets and the continuous extension they produce

The cluster set of a map f on U at a point w is the set of values approached by f z as z → w inside U. It is the standard tool for reading off boundary behaviour: f extends continuously across w exactly when it has a limit along 𝓝[U] w, and — once the values of f are confined to a compact set — that happens as soon as the cluster set at w has at most one element. The compactness is not decoration: the cluster set of z ↦ 1 / z on ball 0 1 \ {0} at 0 is empty, so it is a subsingleton while the map has no limit.

The second classical property of a cluster set, in the same spirit, is that it is a continuum: when the approach regions U ∩ t are connected along a neighbourhood basis of w — as they are at every boundary point of a convex domain — a cluster set with compact ambient values is nonempty, compact and connected. So a boundary cluster set is either a single point or a nondegenerate connected set; it is never a scattered pair of values, and a boundary correspondence theorem has only to rule out the nondegenerate case.

Nothing in this file is specific to one geometry. The definition and its basic API live over an arbitrary pair of topological spaces, the ε-δ characterization over metric spaces, and the extension theorem over an arbitrary T3 codomain, into a compact subset of which the map is assumed to take its values; a proper metric codomain with a bounded image is the special case in which that compact set is supplied by the boundedness. The complex-analytic consequences — that the boundary cluster set of a conformal map lies on the frontier of the image — are in TauCeti/Analysis/Complex/Conformal/ClusterSet.lean, the consumer this file was written for: Carathéodory's boundary correspondence, layer L5 of the conformal-mapping roadmap, is applied by checking that the boundary cluster sets of a Riemann map are singletons and feeding that into TauCeti.exists_continuousOn_closure_eqOn.

The cluster set is {v | MapClusterPt v (𝓝[U] w) f}; Mathlib has the ClusterPt/MapClusterPt API, on which everything below is built, but no name for this set. The extension itself is Mathlib's extendFrom U f, whose continuity comes from continuousOn_extendFrom: all the criterion adds is the production of the pointwise limits that theorem asks for.

Main definitions

• TauCeti.clusterSetOn — the cluster set of f on U at w.
• TauCeti.IsPreconnectedApproachAt — a set has preconnected approach regions at a point.

Main results

• TauCeti.clusterSetOn_eq_iInter and TauCeti.mem_clusterSetOn_iff_forall_exists — the two textbook characterizations, as a nested intersection and in ε-δ form.
• TauCeti.isClosed_clusterSetOn, TauCeti.clusterSetOn_subset_closure_image, TauCeti.isCompact_clusterSetOn and TauCeti.clusterSetOn_nonempty — the cluster set is a closed subset of closure (f '' U), and is compact and nonempty at every point of closure U once f maps U into a compact set.
• TauCeti.clusterSetOn_eq_singleton_of_tendsto, TauCeti.clusterSetOn_eq_singleton_of_continuousWithinAt and TauCeti.exists_tendsto_of_clusterSetOn_subsingleton — a limit along 𝓝[U] w makes the cluster set a singleton, in particular at a point of U where f is continuous; conversely a subsingleton cluster set at a point of closure U produces a limit, provided f maps U into a compact set.
• TauCeti.exists_mem_closure_mem_clusterSetOn, TauCeti.exists_mem_frontier_mem_clusterSetOn_of_notMem_image, TauCeti.closure_image_eq_biUnion_clusterSetOn and TauCeti.closure_image_eq_image_union_biUnion_clusterSetOn — the cluster sets cover the closure of the image once closure U is compact: every adherent value of f '' U is a cluster value at some point of closure U — at a point of frontier U, if the value is not attained and f is continuous — so closure (f '' U) is the union of the cluster sets, and — for continuous f — is the image together with the boundary cluster values.
• TauCeti.exists_continuousOn_closure_eqOn — the extension criterion: a continuous map into a compact set, with subsingleton boundary cluster sets, extends continuously to closure U; TauCeti.exists_continuousOn_closure_eqOn_of_isBounded is the proper-metric form, where the compact set is the closure of the bounded image.
• TauCeti.isPreconnected_clusterSetOn and TauCeti.isConnected_clusterSetOn — the cluster set is a continuum once the approach regions U ∩ t are preconnected along a neighbourhood basis of w; TauCeti.isCompact_clusterSetOn_of_isBounded and TauCeti.isConnected_clusterSetOn_of_isBounded are again the proper-metric forms.
• TauCeti.isPreconnectedApproachAt_of_forall_exists_isPreconnected_superset — the metric-space criterion for preconnected approach regions.

References

• E. F. Collingwood and A. J. Lohwater, The Theory of Cluster Sets, Ch. 1.
• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 2.

The cluster set

def TauCeti.clusterSetOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (U : Set X) (w : X) : Set Y

The cluster set of f on U at w: the set of values approached by f z as z tends to w from inside U. Equivalently, the set of cluster points of the filter 𝓝[U] w pushed forward by f.

The point w is not required to lie in U, and the interesting case is w ∈ frontier U, where the cluster set records the boundary behaviour of f. If w ∉ closure U the filter 𝓝[U] w is trivial and the cluster set is empty.

Equations

• TauCeti.clusterSetOn f U w = {v : Y | MapClusterPt v (nhdsWithin w U) f}

@[simp]

theorem TauCeti.mem_clusterSetOn_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {f : X → Y} {v : Y} {w : X} : v ∈ clusterSetOn f U w ↔ MapClusterPt v (nhdsWithin w U) f

Membership in the cluster set is exactly Mathlib's MapClusterPt for the filter 𝓝[U] w. This is the normal form: the alternative characterizations below are deliberately left untagged.

theorem TauCeti.mem_clusterSetOn_iff_frequently {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {f : X → Y} {v : Y} {w : X} : v ∈ clusterSetOn f U w ↔ ∀ s ∈ nhds v, ∃ᶠ (z : X) in nhdsWithin w U, f z ∈ s

Membership in the cluster set, unfolded: every neighbourhood of v is hit by f frequently along 𝓝[U] w.

theorem TauCeti.clusterSetOn_eq_iInter {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {f : X → Y} {w : X} : clusterSetOn f U w = ⋂ s ∈ nhdsWithin w U, closure (f '' s)

The cluster set as a nested intersection, the form in which it is usually defined: the values that cannot be separated from f on any approach region.

Since closure (f '' ·) is monotone, Filter.HasBasis.biInter_mem cuts the intersection down to any basis of 𝓝[U] w; that is how the cluster set is exhibited as a directed intersection in TauCeti.isPreconnected_clusterSetOn, a basis being directed by design.

theorem TauCeti.isClosed_clusterSetOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {f : X → Y} {w : X} : IsClosed (clusterSetOn f U w)

The cluster set is closed: it is a set of cluster points of a filter.

theorem TauCeti.clusterSetOn_mono {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {f : X → Y} {w : X} {V : Set X} (h : U ⊆ V) : clusterSetOn f U w ⊆ clusterSetOn f V w

Enlarging the set along which f is followed enlarges the cluster set.

@[simp]

theorem TauCeti.clusterSetOn_inter_of_mem_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {f : X → Y} {w : X} {V : Set X} (hV : V ∈ nhds w) : clusterSetOn f (U ∩ V) w = clusterSetOn f U w

The cluster set is local: cutting the approach set down by a neighbourhood of the point leaves it unchanged, since 𝓝[U ∩ V] w = 𝓝[U] w when V ∈ 𝓝 w. The converse inclusion to TauCeti.clusterSetOn_mono therefore holds for such a V, and a cluster set may be computed inside any ball about w.

theorem TauCeti.clusterSetOn_subset_closure_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {f : X → Y} {w : X} : clusterSetOn f U w ⊆ closure (f '' U)

Every cluster value is a limit of image points: the cluster set sits inside closure (f '' U).

theorem TauCeti.isCompact_clusterSetOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {K : Set Y} {f : X → Y} {w : X} [T2Space Y] (hK : IsCompact K) (hfK : Set.MapsTo f U K) : IsCompact (clusterSetOn f U w)

The cluster set is compact whenever f maps U into a compact set: it is a closed subset of that set.

theorem TauCeti.clusterSetOn_nonempty {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {K : Set Y} {f : X → Y} {w : X} (hK : IsCompact K) (hfK : Set.MapsTo f U K) (hw : w ∈ closure U) : (clusterSetOn f U w).Nonempty

The cluster set is nonempty at every point of the closure, provided f maps U into a compact set. Some such hypothesis is needed: the cluster set of z ↦ 1 / z on ball 0 1 \ {0} at 0 is empty, the values escaping to infinity.

Cluster sets and limits

theorem TauCeti.clusterSetOn_eq_singleton_of_tendsto {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {f : X → Y} {v : Y} {w : X} [T2Space Y] (hw : w ∈ closure U) (hv : Filter.Tendsto f (nhdsWithin w U) (nhds v)) : clusterSetOn f U w = {v}

If f has a limit v along 𝓝[U] w, the cluster set is exactly {v}.

@[simp]

theorem TauCeti.clusterSetOn_eq_singleton_of_continuousWithinAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {f : X → Y} {w : X} [T2Space Y] (hw : w ∈ U) (hfc : ContinuousWithinAt f U w) : clusterSetOn f U w = {f w}

At a point of U where f is continuous the cluster set is the value. Nothing but f w is approached, so a cluster set carries information only at points off U — which is why a boundary-correspondence theorem never has to say anything about the interior.

This is the normal form of a cluster set at an interior continuity point, and is tagged @[simp]: with the two hypotheses to hand, simp [*] rewrites clusterSetOn f U w to {f w}.

theorem TauCeti.exists_tendsto_of_clusterSetOn_subsingleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {K : Set Y} {f : X → Y} {w : X} (hK : IsCompact K) (hfK : Set.MapsTo f U K) (hw : w ∈ closure U) (hsub : (clusterSetOn f U w).Subsingleton) : ∃ (v : Y), Filter.Tendsto f (nhdsWithin w U) (nhds v)

A subsingleton cluster set is an honest limit. If f maps U into a compact set and the cluster set at w ∈ closure U has at most one element, then f converges along 𝓝[U] w.

The compactness hypothesis is what makes this a genuine converse to TauCeti.clusterSetOn_eq_singleton_of_tendsto rather than a vacuous one: it forces the cluster set to be nonempty, by TauCeti.clusterSetOn_nonempty, and a filter with values in a compact set and a unique cluster point converges to it.

The cluster sets cover the closure of the image

theorem TauCeti.exists_mem_closure_mem_clusterSetOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {f : X → Y} {v : Y} (hU : IsCompact (closure U)) (hv : v ∈ closure (f '' U)) : ∃ w ∈ closure U, v ∈ clusterSetOn f U w

Every adherent value of the image is a cluster value at some point of closure U, provided closure U is compact.

Aggregated over w, this is the converse of TauCeti.clusterSetOn_subset_closure_image, and it is where compactness of the domain side enters. That hypothesis cannot be dropped: on U = Set.Ici (0 : ℝ), whose closure is not compact, the map f x = 1 / (1 + x) has image Set.Ioc 0 1 and so has 0 adherent to it, yet 0 is a cluster value of f at no point at all — the approach points have escaped to infinity.

No continuity is needed, and the proof is pure filter theory. The filter comap f (𝓝 v) ⊓ 𝓟 U — "inside U, with image near v" — is nontrivial because v is adherent to f '' U, and it is carried by 𝓟 (closure U); compactness supplies a cluster point w of it, and the witnessing filter 𝓝 w ⊓ (comap f (𝓝 v) ⊓ 𝓟 U) is a nontrivial filter refining 𝓝[U] w whose image under f refines 𝓝 v, which is exactly what v ∈ clusterSetOn f U w asserts.

theorem TauCeti.exists_mem_frontier_mem_clusterSetOn_of_notMem_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {f : X → Y} {v : Y} [T2Space Y] (hU : IsCompact (closure U)) (hfc : ContinuousOn f U) (hvc : v ∈ closure (f '' U)) (hvn : v ∉ f '' U) : ∃ w ∈ frontier U, v ∈ clusterSetOn f U w

An unattained adherent value of the image is a cluster value at a boundary point. The sharpening of TauCeti.exists_mem_closure_mem_clusterSetOn that puts the witness on frontier U rather than merely on closure U, for a f continuous on U: a witness inside U would have the single cluster value f w, by TauCeti.clusterSetOn_eq_singleton_of_continuousWithinAt, and v is assumed not to be a value of f on U.

Neither openness of U nor any hypothesis on frontier U is needed.

theorem TauCeti.closure_image_eq_biUnion_clusterSetOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {f : X → Y} (hU : IsCompact (closure U)) : closure (f '' U) = ⋃ w ∈ closure U, clusterSetOn f U w

The cluster sets cover the closure of the image. For a compact closure U, the closure of f '' U is exactly the union of the cluster sets of f on U over the points of closure U.

Both inclusions have already been recorded: TauCeti.clusterSetOn_subset_closure_image gives one and TauCeti.exists_mem_closure_mem_clusterSetOn the other.

theorem TauCeti.closure_image_eq_image_union_biUnion_clusterSetOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} {f : X → Y} [T2Space Y] (hU : IsCompact (closure U)) (hfc : ContinuousOn f U) : closure (f '' U) = f '' U ∪ ⋃ w ∈ frontier U, clusterSetOn f U w

The closure of the image is the image together with the boundary cluster values. The refinement of TauCeti.closure_image_eq_biUnion_clusterSetOn for a continuous f: the points of U contribute only the values f w themselves, by TauCeti.clusterSetOn_eq_singleton_of_continuousWithinAt, so the whole of the new material sits over frontier U.

This is the form in which the covering is used: subtracting f '' U from both sides identifies closure (f '' U) \ f '' U with the union of the boundary cluster sets, as soon as one knows that the boundary cluster values avoid f '' U. That difference is the frontier of the image only when f '' U is open — which is an extra hypothesis, not part of this theorem, and is what conformality supplies in TauCeti.biUnion_clusterSetOn_eq_frontier_image.

The metric picture

theorem TauCeti.mem_clusterSetOn_iff_forall_exists {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {U : Set X} {f : X → Y} {v : Y} {w : X} : v ∈ clusterSetOn f U w ↔ ∀ ε > 0, ∀ δ > 0, ∃ z ∈ U, dist z w < δ ∧ dist (f z) v < ε

The ε-δ form of membership in the cluster set: f takes values arbitrarily close to v at points of U arbitrarily close to w.

The Cauchy criterion for a subsingleton cluster set

theorem TauCeti.subsingleton_clusterSetOn_of_forall_exists {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [MetricSpace Y] {U : Set X} {f : X → Y} {w : X} (h : ∀ ε > 0, ∃ δ > 0, ∀ x ∈ U ∩ Metric.ball w δ, ∀ y ∈ U ∩ Metric.ball w δ, dist (f x) (f y) ≤ ε) : (clusterSetOn f U w).Subsingleton

A uniformly small oscillation on the approach regions makes the cluster set a subsingleton. If, for every ε > 0, the values of f on U ∩ ball w δ are within ε of one another for some δ > 0, then f has at most one cluster value at w along U.

This is the Cauchy criterion in cluster-set form, and it is how a quantitative boundary estimate is turned into the hypothesis of TauCeti.exists_tendsto_of_clusterSetOn_subsingleton and of TauCeti.exists_continuousOn_closure_eqOn: two cluster values are approached at points of U arbitrarily close to w, hence at two points of a single approach region, where the hypothesis holds them within ε of each other.

Nothing is claimed about existence of a cluster value, which is a compactness matter; the codomain is a genuine metric space rather than a pseudometric one because the conclusion is an equality of points.

The extension criterion

theorem TauCeti.exists_continuousOn_closure_eqOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {U : Set X} {K : Set Y} {f : X → Y} (hUo : IsOpen U) (hfc : ContinuousOn f U) (hK : IsCompact K) (hfK : Set.MapsTo f U K) (hsub : ∀ w ∈ frontier U, (clusterSetOn f U w).Subsingleton) : ∃ (F : X → Y), ContinuousOn F (closure U) ∧ Set.EqOn F f U

The extension criterion. A continuous function on an open U, taking values in a compact set and whose cluster set at each boundary point has at most one element, extends continuously to closure U.

The compactness is what TauCeti.exists_tendsto_of_clusterSetOn_subsingleton consumes to turn each subsingleton boundary cluster set into a limit; at an interior point continuity already supplies the limit. Having a limit at every point of closure U, the map extends by Mathlib's extendFrom, which is continuous on closure U by continuousOn_extendFrom and agrees with f on U by extendFrom_extends. TauCeti.exists_continuousOn_closure_eqOn_of_isBounded is the common special case of a bounded-image map into a proper metric space.

This is the form in which a boundary-correspondence theorem is applied: whatever geometric hypothesis one places on frontier U, it is used only to check that the boundary cluster sets are singletons, and this theorem converts that check into a continuous extension. No cluster-set hypothesis is needed at the interior points of U, where continuity already makes the cluster set the singleton {f w}.

The conclusion is exactly a continuous extension: F is continuous on closure U and agrees with f on U. Nothing is claimed about injectivity of F on closure U; that is an independent matter, requiring a separate proof that F is injective on frontier U.

theorem TauCeti.exists_continuousOn_closure_eqOn_of_isBounded {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MetricSpace Y] [ProperSpace Y] {U : Set X} {f : X → Y} (hUo : IsOpen U) (hfc : ContinuousOn f U) (hfb : Bornology.IsBounded (f '' U)) (hsub : ∀ w ∈ frontier U, (clusterSetOn f U w).Subsingleton) : ∃ (F : X → Y), ContinuousOn F (closure U) ∧ Set.EqOn F f U

The extension criterion for a bounded map into a proper metric space. The special case of TauCeti.exists_continuousOn_closure_eqOn in which the compact set containing the values of f is the closure of a bounded image, properness of the codomain being what makes that closure compact.

The cluster set as a continuum

theorem TauCeti.isPreconnected_clusterSetOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {U : Set X} {K : Set Y} {f : X → Y} {w : X} (hK : IsCompact K) (hfK : Set.MapsTo f U K) (hfc : ContinuousOn f U) (hconn : ∀ s ∈ nhds w, ∃ t ∈ nhds w, t ⊆ s ∧ IsPreconnected (U ∩ t)) : IsPreconnected (clusterSetOn f U w)

The cluster set is preconnected when the approach regions are. If f is continuous on U with values in a compact set, and w has a neighbourhood basis of sets t whose trace U ∩ t on U is preconnected, then the cluster set of f on U at w is preconnected.

The basis hypothesis is what a domain contributes: it holds at every point of the closure of a convex U, and more generally whenever U is locally connected along its boundary. It cannot be dropped — the cluster set of a map on a disconnected U is a union of the cluster sets along the pieces, which have no reason to meet.

The proof writes the cluster set as ⋂ t, closure (f '' (U ∩ t)) over such a basis, by TauCeti.clusterSetOn_eq_iInter and Filter.HasBasis.biInter_mem, whose monotonicity hypothesis is met by closure (f '' ·). Each member is a compact preconnected set — the continuous image of a preconnected set, closed up, inside the compact K — and the family is directed downwards because the basis is. So TauCeti.isPreconnected_iInter_of_directed applies.

theorem TauCeti.isConnected_clusterSetOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {U : Set X} {K : Set Y} {f : X → Y} {w : X} (hK : IsCompact K) (hfK : Set.MapsTo f U K) (hfc : ContinuousOn f U) (hw : w ∈ closure U) (hconn : ∀ s ∈ nhds w, ∃ t ∈ nhds w, t ⊆ s ∧ IsPreconnected (U ∩ t)) : IsConnected (clusterSetOn f U w)

The cluster set is a continuum: nonempty, compact and connected. This is the classical statement of Collingwood–Lohwater, under the hypotheses of TauCeti.isPreconnected_clusterSetOn together with w ∈ closure U, which is what makes the approach filter 𝓝[U] w nontrivial and hence the cluster set nonempty.

Compactness is TauCeti.isCompact_clusterSetOn and is not repeated here.

theorem TauCeti.isCompact_clusterSetOn_of_isBounded {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MetricSpace Y] [ProperSpace Y] {U : Set X} {f : X → Y} {w : X} (hfb : Bornology.IsBounded (f '' U)) : IsCompact (clusterSetOn f U w)

The cluster set of a map with bounded image into a proper metric space is compact: the special case of TauCeti.isCompact_clusterSetOn in which the compact set containing the values is the closure of the bounded image.

theorem TauCeti.isConnected_clusterSetOn_of_isBounded {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MetricSpace Y] [ProperSpace Y] {U : Set X} {f : X → Y} {w : X} (hfc : ContinuousOn f U) (hfb : Bornology.IsBounded (f '' U)) (hw : w ∈ closure U) (hconn : ∀ s ∈ nhds w, ∃ t ∈ nhds w, t ⊆ s ∧ IsPreconnected (U ∩ t)) : IsConnected (clusterSetOn f U w)

The continuum form for a bounded map into a proper metric space, the special case of TauCeti.isConnected_clusterSetOn in which the compact set containing the values is the closure of the bounded image.

Preconnected approach regions

def TauCeti.IsPreconnectedApproachAt {X : Type u_1} [TopologicalSpace X] (U : Set X) (a : X) : Prop

A set has preconnected approach regions at a if every neighbourhood of a contains a smaller neighbourhood whose trace on the set is preconnected. This is the exact local input in the cluster-set continuum theorem (TauCeti.isPreconnected_clusterSetOn).

Equations

• TauCeti.IsPreconnectedApproachAt U a = ∀ s ∈ nhds a, ∃ t ∈ nhds a, t ⊆ s ∧ IsPreconnected (U ∩ t)

theorem TauCeti.isPreconnectedApproachAt_def {X : Type u_1} [TopologicalSpace X] {U : Set X} {a : X} : IsPreconnectedApproachAt U a ↔ ∀ s ∈ nhds a, ∃ t ∈ nhds a, t ⊆ s ∧ IsPreconnected (U ∩ t)

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

theorem TauCeti.isPreconnectedApproachAt_of_forall_exists_isPreconnected_superset {Y : Type u_2} [PseudoMetricSpace Y] {U : Set Y} {a : Y} (h : ∀ ε > 0, ∃ δ > 0, ∃ C ⊆ U ∩ Metric.ball a ε, IsPreconnected C ∧ U ∩ Metric.ball a δ ⊆ C) : IsPreconnectedApproachAt U a

Local connectedness gives preconnected approach regions. If for every ε > 0 some preconnected C ⊆ U ∩ ball a ε contains U ∩ ball a δ for a δ > 0, then U has preconnected approach regions at a.