The cluster set of a map on a convex domain

In a real locally convex topological vector space, every point has a neighbourhood basis of convex sets. Their intersections with a convex domain U are convex, hence preconnected. Thus a continuous map on U with values in a compact Hausdorff set has a preconnected cluster set, by TauCeti.isPreconnected_clusterSetOn.

The approach point w need not lie in U. At a point of closure U, compactness also makes the cluster set nonempty, so it is connected; TauCeti.isCompact_clusterSetOn supplies its compactness. No norm or separation assumption on the domain is needed.

For example, the unit disc, half-planes and convex polygons are convex. The cluster set of a bounded holomorphic injection from the unit disc is therefore a continuum at each boundary point. This is the connectedness input for Carathéodory's boundary correspondence, which proves that the continuum is a singleton when the image is a Jordan domain.

Main results

• Convex.isPreconnected_clusterSetOn and Convex.isConnected_clusterSetOn: on a convex domain the cluster set is preconnected, and is connected at a point of the closure.
• Convex.isConnected_clusterSetOn_of_isBounded: the form for a continuous map with bounded image into a proper metric space.

References

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

theorem Convex.isPreconnected_clusterSetOn {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] {U : Set E} {K : Set Y} {f : E → Y} {w : E} (hUc : Convex ℝ U) (hK : IsCompact K) (hfK : Set.MapsTo f U K) (hfc : ContinuousOn f U) : IsPreconnected (TauCeti.clusterSetOn f U w)

A continuous map on a convex domain in a real locally convex space, with values in a compact Hausdorff set, has a preconnected cluster set at every approach point.

theorem Convex.isConnected_clusterSetOn {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] {U : Set E} {K : Set Y} {f : E → Y} {w : E} (hUc : Convex ℝ U) (hK : IsCompact K) (hfK : Set.MapsTo f U K) (hfc : ContinuousOn f U) (hw : w ∈ closure U) : IsConnected (TauCeti.clusterSetOn f U w)

A continuous map on a convex domain in a real locally convex space, with values in a compact Hausdorff set, has a connected cluster set at each point of the closure of its domain. Compactness of the cluster set is given by TauCeti.isCompact_clusterSetOn.

theorem Convex.isConnected_clusterSetOn_of_isBounded {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {Y : Type u_2} [MetricSpace Y] [ProperSpace Y] {U : Set E} {f : E → Y} {w : E} (hUc : Convex ℝ U) (hfc : ContinuousOn f U) (hfb : Bornology.IsBounded (f '' U)) (hw : w ∈ closure U) : IsConnected (TauCeti.clusterSetOn f U w)

A continuous map on a convex domain in a real locally convex space, with bounded image in a proper metric space, has a connected cluster set at each point of the closure of its domain. Compactness of the cluster set is given by TauCeti.isCompact_clusterSetOn_of_isBounded.