The exterior of a closed ball is preconnected #
In a real normed space of dimension at least two the complement of a closed ball is preconnected:
it is the union, over the radii M exceeding the ball's, of the spheres of radius M, strung
together along a single ray from the centre.
Every unbounded complementary component of a bounded set meets the exterior of any closed ball
containing that set. Preconnectedness of the exterior therefore forces all such components to
coincide. This uniqueness result and the corresponding filled-hull alternative are proved in
TauCeti/Analysis/Normed/Module/FilledHull.lean.
Main results #
TauCeti.isPreconnected_compl_closedBall— the exterior of a closed ball is preconnected in a real normed space of dimension at least two.
References #
- Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 2.
theorem
TauCeti.isPreconnected_compl_closedBall
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(h : 1 < Module.rank ℝ E)
(x : E)
(r : ℝ)
:
The exterior of a closed ball is preconnected in a real normed space of dimension at least two.