Catching a bounded set inside a square

The outer face of a plane graph is found by catching the whole drawing — finitely many points and finitely many compact arcs — inside one axis-parallel square, and then observing that the outside of that square is connected (isConnected_beyondSquare) and therefore lies in a single face. This module is the "catching" half.

The key identity is beyondSquare_eq_compl: the outside of a square, as defined by a coordinate inequality, is the complement of the closed square. It is what lets the connectedness theorem be applied to a complement.

Blueprint

• beyondSquare_eq_compl — the outside of a square is the complement of the closed square.
• exists_closedSquare_of_isBounded, IsCompact.exists_closedSquare — a bounded set is caught inside a square about the origin.
• isOpen_compl_of_finite_isCompact — the complement of a finite union of compact sets is open; the exterior of a plane graph is open for this reason.

@[simp]

theorem Schoenflies.Plane.supDist_zero (x : Plane) : x.supDist 0 = x.supNorm

theorem Schoenflies.Plane.beyondSquare_eq_compl (r : ℝ) : beyondSquare r = (closedSquare 0 r)ᶜ

The outside of a square is exactly the complement of the closed square.

theorem Schoenflies.Plane.exists_closedSquare_of_isBounded {s : Set Plane} (hs : Bornology.IsBounded s) : ∃ (r : ℝ), 0 ≤ r ∧ s ⊆ closedSquare 0 r

A bounded set sits inside a closed square about the origin, of nonnegative radius.

theorem Schoenflies.Plane.IsCompact.exists_closedSquare {s : Set Plane} (hs : IsCompact s) : ∃ (r : ℝ), 0 ≤ r ∧ s ⊆ closedSquare 0 r

theorem Schoenflies.Plane.closedSquare_mono {r s : ℝ} (h : r ≤ s) : closedSquare 0 r ⊆ closedSquare 0 s

Two squares about the origin merge by taking the larger radius; kept nonnegative so that callers never split on which is larger.

theorem Schoenflies.Plane.exists_closedSquare_of_finite {ι : Type u_1} {S : ι → Set Plane} {t : Set ι} (ht : t.Finite) (hS : ∀ i ∈ t, Bornology.IsBounded (S i)) : ∃ (r : ℝ), 0 ≤ r ∧ ⋃ i ∈ t, S i ⊆ closedSquare 0 r

A finite family of bounded sets is caught inside one square.

theorem Schoenflies.Plane.isOpen_compl_of_finite_isCompact {ι : Type u_1} {S : ι → Set Plane} {t : Set ι} (ht : t.Finite) (hS : ∀ i ∈ t, IsCompact (S i)) : IsOpen (⋃ i ∈ t, S i)ᶜ

The complement of a finite union of compact sets is open. The exterior of a plane graph — finitely many vertices and finitely many compact edge arcs — is open for this reason.