Topology of the plane: the gaps Mathlib leaves

Appendix C of the blueprint lists the topology imported without proof. Almost all of it is in Mathlib: compactness and Heine–Borel, the compact-to-Hausdorff homeomorphism criterion, connectedness and its stability under images, unions through a common point, adjoining closure points (IsPreconnected.subset_closure), a connected set inside a disjoint union of two opens (IsPreconnected.subset_left_of_subset_union), Metric.diam_closure, thickenings, and the two-piece pasting lemma (continuousOn_union_iff_of_isClosed).

This module collects the few that are not stated in the form the development uses.

Blueprint

• isOpen_connectedComponentIn — Appendix C item 4: components of open subsets of the plane are open. The plane is locally connected, so this is Mathlib's, restated at Plane so that the instance is found once here rather than at every call site.
• frontier_connectedComponentIn_compl_subset — Appendix C item 5: the boundary of a component of the complement of a closed set lies in that closed set. This is the form Part I uses to recognize that a region's frontier sits on the curve.
• continuousOn_union_of_isClosed — Appendix C item 6, the pasting lemma, in the two-piece form the development pastes with.

theorem Schoenflies.Plane.isOpen_connectedComponentIn {U : Set Plane} {x : Plane} (hU : IsOpen U) : IsOpen (connectedComponentIn U x)

Components of an open subset of the plane are open. The plane is locally connected.

theorem Schoenflies.Plane.frontier_connectedComponentIn_compl_subset {K : Set Plane} (hK : IsClosed K) (x : Plane) : frontier (connectedComponentIn Kᶜ x) ⊆ K

Appendix C item 5. The frontier of a component of the complement of a closed set lies in that closed set.

A frontier point off K would be a point of the open set Kᶜ in the closure of the component; adjoining it keeps the component connected, so it was in the component already.

theorem Schoenflies.Plane.continuousOn_union_of_isClosed {f : Plane → Plane} {s t : Set Plane} (hs : IsClosed s) (ht : IsClosed t) (hfs : ContinuousOn f s) (hft : ContinuousOn f t) : ContinuousOn f (s ∪ t)

Appendix C item 6, the pasting lemma, two closed pieces.