Filling in the bounded complementary components of a set

The filled hull TauCeti.filledHull K of a subset K of a topological space with a bornology is K together with the bounded connected components of its complement: the points whose component in Kᶜ is bounded. Points of K qualify vacuously, their component in Kᶜ being empty. Filling a circle gives the closed disc it bounds; filling a segment, or any set whose complement is connected and unbounded, changes nothing.

This file develops the definition and structural properties using only a topology and a bornology. In a real seminormed space, filling preserves boundedness and diameter; these bounds are proved in TauCeti/Analysis/Normed/Module/FilledHull.lean.

The trapping property IsPreconnected.subset_filledHull says that a preconnected set disjoint from K lies inside the filled hull as soon as it meets it, since it then lies in a single bounded component. Together with the diameter bound, it gives IsPreconnected.diam_le_diam_of_disjoint: a preconnected set disjoint from a bounded K that meets its filled hull has diameter at most diam K, without regularity assumptions on K.

A point lies outside the filled hull exactly when its component in the complement of K is unbounded. This is the hypothesis of TauCeti.Contour.windingNumber_eq_zero_of_unbounded_component in TauCeti/Analysis/Contour/Winding/UnboundedComponent.lean and of its cycle form TauCeti.Contour.Cycle.windingNumber_eq_zero_of_unbounded_component in TauCeti/Analysis/Contour/Cycle/Winding.lean: for a closed curve with the required regularity, or a contour cycle, the winding number vanishes outside the filled hull of its trace.

Without additional hypotheses on K, the hull need not be closed or connected.

Planar enclosure

For a planar set J, filledHull J \ J consists of its bounded complementary components. The enclosure theorem TauCeti.image_inter_ball_subset_filledHull_of_diam_lt_of_isPreconnected_sdiff_singleton combines winding-number two-sidedness with preconnectedness of K \ {f z₀} to place the near-side image of a circular crosscut inside filledHull K when the far-side image has larger diameter than K. For a Jordan curve, TauCeti.IsJordanCurve.isPathConnected_sdiff_singleton supplies the required preconnectedness. These enclosure and diameter estimates are used in the Carathéodory boundary correspondence in TauCeti/Analysis/Complex/Conformal/Caratheodory.lean.

Main results

• TauCeti.filledHull — the filled hull, and TauCeti.subset_filledHull, TauCeti.filledHull_mono its two structural properties.
• TauCeti.filledHull_eq_self — filling a set whose complement is preconnected and unbounded changes nothing.
• TauCeti.filledHull_eq_self_of_isPreconnected_frontier — an open set with preconnected frontier and unbounded complement has no holes: filling it changes nothing.
• IsPreconnected.subset_filledHull — a preconnected set disjoint from K that meets the filled hull lies in it.
• TauCeti.subset_filledHull_of_frontier_subset — a bounded set whose frontier K swallows lies in the filled hull, with no connectivity asked of it.

def TauCeti.filledHull {E : Type u_1} [TopologicalSpace E] [Bornology E] (K : Set E) : Set E

The filled hull of a set K: the points whose connected component in the complement of K is bounded. Equivalently, K together with the bounded connected components of Kᶜ; a point of K belongs because its component in Kᶜ is empty.

Equations

• TauCeti.filledHull K = {x : E | Bornology.IsBounded (connectedComponentIn Kᶜ x)}

@[simp]

theorem TauCeti.mem_filledHull_iff {E : Type u_1} [TopologicalSpace E] [Bornology E] {K : Set E} {x : E} : x ∈ filledHull K ↔ Bornology.IsBounded (connectedComponentIn Kᶜ x)

theorem TauCeti.subset_filledHull {E : Type u_1} [TopologicalSpace E] [Bornology E] {K : Set E} : K ⊆ filledHull K

A set lies in its filled hull. For x ∈ K the component of x in Kᶜ is empty, and the empty set is bounded.

theorem TauCeti.filledHull_mono {E : Type u_1} [TopologicalSpace E] [Bornology E] {K L : Set E} (h : K ⊆ L) : filledHull K ⊆ filledHull L

Filling is monotone. Enlarging K shrinks the complement, hence shrinks each component of it, hence can only turn unbounded components into bounded ones.

theorem TauCeti.filledHull_eq_self {E : Type u_1} [TopologicalSpace E] [Bornology E] {K : Set E} (h : IsPreconnected Kᶜ) (hu : ¬Bornology.IsBounded Kᶜ) : filledHull K = K

Filling changes nothing when the complement is connected and unbounded. The complement is then a single component and that component is unbounded, so no point outside K is filled in. This is the case of a segment in the plane, and of any set that does not separate the space.

theorem TauCeti.filledHull_eq_self_of_isPreconnected_frontier {E : Type u_1} [TopologicalSpace E] [Bornology E] {K : Set E} [LocallyConnectedSpace E] [PreconnectedSpace E] (hK : IsOpen K) (hf : IsPreconnected (frontier K)) (hu : ¬Bornology.IsBounded Kᶜ) : filledHull K = K

An open set with preconnected frontier has no holes, in a preconnected, locally connected space: if the complement of K is unbounded, filling K changes nothing. The complement is then preconnected (TauCeti.isPreconnected_compl_of_isPreconnected_frontier), so this is TauCeti.filledHull_eq_self. A bounded open set of the plane whose frontier is a Jordan curve is the basic example.

theorem IsPreconnected.subset_filledHull {E : Type u_1} [TopologicalSpace E] [Bornology E] {K S : Set E} (hS : IsPreconnected S) (hSK : Disjoint S K) (hne : (S ∩ TauCeti.filledHull K).Nonempty) : S ⊆ TauCeti.filledHull K

A preconnected set that a set cuts off from infinity lies in its filled hull. If S is preconnected and disjoint from K, then S lies in a single connected component of Kᶜ; meeting the filled hull says that component is bounded, so all of S is in the hull.

theorem TauCeti.subset_filledHull_of_frontier_subset {E : Type u_1} [TopologicalSpace E] [Bornology E] {K S : Set E} (hSb : Bornology.IsBounded S) (hfr : frontier S ⊆ K) : S ⊆ filledHull K

A bounded set whose frontier lies in K is cut off from infinity by K. A point of S \ K lies in interior S, since every non-interior point of S lies on frontier S ⊆ K. Its connected component in Kᶜ cannot leave interior S: were it to, it would meet frontier (interior S) ⊆ frontier S ⊆ K by IsPreconnected.inter_frontier_nonempty, while lying in Kᶜ. So that component is bounded because S is. Points of S ∩ K lie in the filled hull directly.

Unlike IsPreconnected.subset_filledHull this asks nothing of the connectivity of S and nothing about the hull being met, at the price of asking K to swallow the whole frontier — the same trade as between TauCeti.diam_le_diam_of_frontier_subset and IsPreconnected.diam_le_diam_of_disjoint.