Elementary frontier lemmas

Facts about frontier that carry no structure of their own: straddling, splitting a domain in two, clinging to it from inside, the frontier of an image, and the frontier of a finite union. Each is the topological core of a step that a boundary argument would otherwise carry out inside a concrete space. The list is open-ended; nothing below depends on how many entries it has.

A connected set that straddles a set meets its frontier

A preconnected set that meets both a set V and its complement must meet frontier V: it cannot cross from the inside of V to the outside without touching the boundary. This is the intermediate-value principle in its purely topological form, and it is the mechanism by which a path leaving a set produces a boundary point of that set.

Mathlib records the two extreme cases — frontier_eq_empty_iff and nonempty_frontier_iff say that in a preconnected space the frontier of V is empty exactly when V is ∅ or univ — but not this relative form, which is the one an argument along a segment or a path needs. No hypothesis is placed on V; only preconnectedness of the straddling set is used.

The proof is the standard clopen argument: the complement of frontier V is the disjoint union of the two open sets interior V and interior Vᶜ (compl_frontier_eq_union_interior), so a preconnected set avoiding the frontier lies inside one of them, and then it misses V entirely or is contained in V entirely.

Where the boundary of the image of one side of a split domain can lie

Split a set U into two pieces s and t that a map f sends to disjoint open sets, plus a remainder u. Then frontier (f '' s) ⊆ f '' u ∪ frontier (f '' U) (TauCeti.frontier_image_subset_image_union_frontier_image): the boundary of the image of one side consists of images of the remainder — the cut — and of boundary points of the whole image, and of nothing else.

The proof is a three-way case split. A point p of frontier (f '' s) lies in closure (f '' U), so if it is not on frontier (f '' U) it is a value f w with w in one of the three covering sets. It cannot come from s, since f '' s is open and therefore disjoint from its own frontier; and it cannot come from t, since f '' t is then an open neighbourhood of p, which must meet f '' s, contradicting disjointness of the two images. So w ∈ u.

The source carries no topology; the sides enter topologically only through their images, which are asked to be open and disjoint, and that is all the argument uses of them. What is asked of the sides themselves is purely set-theoretic: s ⊆ U and the covering U ⊆ s ∪ t ∪ u. In particular t need not lie in U, and neither side need be open or disjoint from the other. A consumer whose map is open and injective on two disjoint open sides supplies both image hypotheses, as the conformal one below does through the open mapping theorem and Disjoint.image.

What a set's frontier sees of a subset

A subset A of a set V cannot reach frontier V except through its own frontier:

frontier V ∩ closure A = frontier V ∩ frontier A

(TauCeti.frontier_inter_closure_eq_frontier_inter_frontier). The reason is that closure A is A ∪ frontier A, and a point of A on frontier V is already on frontier A: it is adherent to A and, since interior A ⊆ interior V, it is not interior to A. So the part of frontier V that A clings to has two interchangeable descriptions — as the reach of closure A, and as the meeting of two frontiers. The first is the one an argument about limits of points of A produces; the second is the one a diameter estimate consumes, frontier being where the estimates of a domain-splitting argument live.

Consumers

The straddling, splitting and clinging lemmas serve Carathéodory's boundary correspondence for conformal maps. The first does so through TauCeti/Analysis/Normed/Module/DiamFrontier.lean: a ray leaving a bounded set crosses its frontier, which is what makes the frontier of such a set as wide as the set itself. The second is the splitting step of TauCeti/Analysis/Complex/Conformal/CutDiameter.lean, where s and t are the two sides of a circular crosscut of a domain and u is the crosscut arc. The third is what lets TauCeti/Analysis/Complex/Conformal/ClusterSet.lean identify the boundary piece that one side of such a crosscut cuts off, whose description as a union of cluster sets is naturally a statement about a closure. The image and finite-union lemmas are used quite differently, for a partial homeomorphism of a real coordinate space and for the frontier of a finite union of unit translates of a lattice region. Nothing here is specific to any of those uses; no lemma mentions a metric, let alone a holomorphic map.

Main results

• IsPreconnected.inter_frontier_nonempty — a preconnected set meeting both a set and its complement meets the frontier of that set.
• TauCeti.frontier_image_subset_image_union_frontier_image — for a set split into two sides with disjoint open images plus a remainder, the frontier of the image of the side lying in that set lies on the image of the remainder and on the frontier of the image of the whole.
• TauCeti.frontier_inter_closure_eq_frontier_inter_frontier — the frontier of a set meets the closure of a subset exactly where it meets that subset's frontier.
• TauCeti.frontier_image_subset_of_closure_subset — for an open injective map whose image closure adds at most a set t, the frontier of an image lies on the image of the frontier, together with t.
• TauCeti.frontier_iUnion_subset — the frontier of a union over a finite index type lies in the union of the frontiers.

theorem IsPreconnected.inter_frontier_nonempty {X : Type u_1} [TopologicalSpace X] {S V : Set X} (hS : IsPreconnected S) (h₁ : (S ∩ V).Nonempty) (h₂ : (S \ V).Nonempty) : (S ∩ frontier V).Nonempty

A preconnected set that meets both a set and its complement meets its frontier. If S is preconnected and contains a point of V and a point outside V, then S meets frontier V.

Nothing is assumed about V; the argument is that (frontier V)ᶜ is the union of the two disjoint open sets interior V and interior Vᶜ, so a preconnected set missing the frontier is confined to one of them and therefore cannot straddle V.

theorem TauCeti.frontier_image_subset_image_union_frontier_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace Y] {f : X → Y} {U s t u : Set X} (hfs : IsOpen (f '' s)) (hft : IsOpen (f '' t)) (hst : Disjoint (f '' s) (f '' t)) (hsU : s ⊆ U) (hcov : U ⊆ s ∪ t ∪ u) : frontier (f '' s) ⊆ f '' u ∪ frontier (f '' U)

The boundary of the image of one side of a split domain lies on the image of the remainder and on the boundary of the image of the domain. If U is covered by two sets s, t with disjoint open images together with a third set u, and s ⊆ U, then frontier (f '' s) ⊆ f '' u ∪ frontier (f '' U).

The conclusion is about s, the side that is asked to lie in U. The argument treats the two sides alike apart from that, so a consumer with t ⊆ U in hand bounds t as well by swapping their roles.

A frontier point of f '' s lies in closure (f '' U), so if it is not a frontier point of f '' U it is a value f w with w in one of the three covering sets: w ∈ s would place it inside the open set f '' s, which is disjoint from its own frontier, and w ∈ t inside the open set f '' t, which meets f '' s because the point is in its closure, contradicting disjointness of the two images. So w ∈ u.

The source carries no topology at all: U and the three sets covering it are constrained only by the two set-theoretic hypotheses hsU : s ⊆ U and hcov : U ⊆ s ∪ t ∪ u, while every topological hypothesis, and the conclusion, lives in the target. In particular t need not lie in U, and the two sides need be neither open nor disjoint nor separated by injectivity — only their images need be open and disjoint, which is what the argument uses and what an injective open map on two disjoint open sides supplies.

theorem TauCeti.frontier_inter_closure_eq_frontier_inter_frontier {X : Type u_1} [TopologicalSpace X] {A V : Set X} (hAV : A ⊆ V) : frontier V ∩ closure A = frontier V ∩ frontier A

The frontier of a set meets the closure of a subset exactly where it meets that subset's frontier. For any A ⊆ V,

frontier V ∩ closure A = frontier V ∩ frontier A.

Writing closure A as A ∪ frontier A, the first piece brings nothing new: a point of A on frontier V is adherent to A and is kept out of interior A by interior A ⊆ interior V, so it already lies on frontier A. Only the inclusion A ⊆ V is used — V need be neither open nor closed, and A is arbitrary.

So the part of frontier V that A clings to may be described either as its meeting with closure A or as its meeting with frontier A. An argument about limits of points of A produces the first; a diameter estimate obtained by splitting V into pieces consumes the second.

theorem TauCeti.frontier_image_subset_of_closure_subset {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {t : Set Y} (hf : IsOpenMap f) (hfi : Function.Injective f) (hcl : closure (f '' s) ⊆ f '' closure s ∪ t) : frontier (f '' s) ⊆ f '' frontier s ∪ t

The frontier of an image lies on the image of the frontier, plus whatever the closure adds. For an open injective f whose image closure satisfies closure (f '' s) ⊆ f '' closure s ∪ t,

frontier (f '' s) ⊆ f '' frontier s ∪ t.

The extra set t absorbs whatever an unbounded direction of s escapes to: without it the inclusion would say that the frontier of an image is the image of a frontier, which fails as soon as f sends a divergent sequence somewhere convergent. A consumer supplies t together with the closure hypothesis, typically from a compactness statement about the image; it is often a single point, but nothing in the argument needs that.

Openness and injectivity are both used, and neither can be dropped: openness keeps the image of the interior inside the interior of the image, and injectivity is what turns a difference of images into the image of a difference.

theorem TauCeti.frontier_iUnion_subset {X : Type u_1} [TopologicalSpace X] {ι : Type u_2} [Finite ι] (A : ι → Set X) : frontier (⋃ (i : ι), A i) ⊆ ⋃ (i : ι), frontier (A i)

The frontier of a finite union lies in the union of the frontiers. Finiteness is essential, not a convenience of the proof: for an infinite union the inclusion fails — the rationals are a countable union of singletons, each its own frontier, yet their union has frontier all of ℝ.