The plane, and the compactness toolkit

The plane is EuclideanSpace ℝ (Fin 2). This module fixes that choice, supplies the orientation form det and the right-angle rotation perp used to keep track of the two sides of a polygonal curve, and collects the elementary consequences of compactness and connectedness that the rest of the development uses without comment.

Blueprint

• det, perp — Appendix C, item 1.
• Plane.notMem_of_mem_segment_of_isMinOn — Lemma 1.3 (nearest-point segment).
• Plane.exists_thickening_subset, Plane.exists_dist_pos, Plane.exists_ball_subset_diff — Lemma 1.4 (a), (b), (c) (compact separation).
• Plane.eq_singleton_iInter_of_diam_tendsto_zero — Lemma 1.6 (nested compact singleton).
• Plane.connectedComponentIn_eq_of_frontier_disjoint — Lemma 1.7 (recognizing a component).

Lemma 1.5 (closure and diameter) is Metric.diam_closure in Mathlib.

@[reducible, inline]

abbrev Schoenflies.Plane : Type

The plane.

Equations

• Schoenflies.Plane = EuclideanSpace ℝ (Fin 2)

@[reducible, inline]

abbrev Schoenflies.Plane.mk (x y : ℝ) : Plane

Build a point of the plane from its two coordinates.

Equations

• Schoenflies.Plane.mk x y = !₂[x, y]

@[simp]

theorem Schoenflies.Plane.mk_zero (x y : ℝ) : (mk x y).ofLp 0 = x

@[simp]

theorem Schoenflies.Plane.mk_one (x y : ℝ) : (mk x y).ofLp 1 = y

The orientation form and the right-angle rotation

def Schoenflies.Plane.det (a b : Plane) : ℝ

The orientation form det (a, b) = a₁b₂ - a₂b₁. It is positive exactly when b lies counterclockwise of a.

Equations

• a.det b = a.ofLp 0 * b.ofLp 1 - a.ofLp 1 * b.ofLp 0

def Schoenflies.Plane.perp (u : Plane) : Plane

u turned counterclockwise through a right angle.

Equations

• u.perp = Schoenflies.Plane.mk (-u.ofLp 1) (u.ofLp 0)

@[simp]

theorem Schoenflies.Plane.perp_zero (u : Plane) : u.perp.ofLp 0 = -u.ofLp 1

@[simp]

theorem Schoenflies.Plane.perp_one (u : Plane) : u.perp.ofLp 1 = u.ofLp 0

@[simp]

theorem Schoenflies.Plane.det_self (a : Plane) : a.det a = 0

theorem Schoenflies.Plane.det_comm (a b : Plane) : a.det b = -b.det a

@[simp]

theorem Schoenflies.Plane.det_smul_left (r : ℝ) (a b : Plane) : (r • a).det b = r * a.det b

@[simp]

theorem Schoenflies.Plane.det_smul_right (r : ℝ) (a b : Plane) : a.det (r • b) = r * a.det b

theorem Schoenflies.Plane.det_add_left (a b c : Plane) : (a + b).det c = a.det c + b.det c

theorem Schoenflies.Plane.det_add_right (a b c : Plane) : a.det (b + c) = a.det b + a.det c

@[simp]

theorem Schoenflies.Plane.det_perp_self (u : Plane) : u.det u.perp = ‖u‖ ^ 2

The defining property of perp: it is the counterclockwise right-angle rotation, so it pairs positively with its argument.

theorem Schoenflies.Plane.inner_eq (u v : Plane) : inner ℝ u v = u.ofLp 0 * v.ofLp 0 + u.ofLp 1 * v.ofLp 1

@[simp]

theorem Schoenflies.Plane.perp_perp (u : Plane) : u.perp.perp = -u

Turning twice reverses.

@[simp]

theorem Schoenflies.Plane.inner_perp_self (u : Plane) : inner ℝ u u.perp = 0

@[simp]

theorem Schoenflies.Plane.det_perp_right (u v : Plane) : u.det v.perp = inner ℝ u v

Against perp on the right, det becomes the inner product. Together with det_perp_left this is what lets the strip lemma trade one for the other.

@[simp]

theorem Schoenflies.Plane.det_perp_left (u v : Plane) : u.perp.det v = -inner ℝ u v

theorem Schoenflies.Plane.det_perp_perp (u v : Plane) : u.perp.det v.perp = u.det v

@[simp]

theorem Schoenflies.Plane.norm_perp (u : Plane) : ‖u.perp‖ = ‖u‖

theorem Schoenflies.Plane.det_eq_zero_iff_smul (u v : Plane) (hu : u ≠ 0) : u.det v = 0 ↔ ∃ (r : ℝ), v = r • u

Two vectors are parallel exactly when the orientation form kills them. This is the angle-free reading of "u and v point along one line".

Compactness

theorem Schoenflies.Plane.notMem_of_mem_segment_of_isMinOn {K : Set Plane} {x a y : Plane} (haK : a ∈ K) (hxK : x ∉ K) (hmin : ∀ b ∈ K, dist x a ≤ dist x b) (hy : y ∈ segment ℝ x a) (hya : y ≠ a) : y ∉ K

Lemma 1.3 (nearest-point segment). If a is a point of K nearest to x ∉ K, then the half-open segment [x, a) misses K.

theorem Schoenflies.Plane.exists_thickening_subset {K U : Set Plane} (hK : IsCompact K) (hU : IsOpen U) (h : K ⊆ U) : ∃ ρ > 0, Metric.thickening ρ K ⊆ U

Lemma 1.4 (a) (compact separation). A compact set inside an open set has a uniform neighbourhood inside it. Empty K is allowed: thickening ρ ∅ = ∅.

theorem Schoenflies.Plane.exists_dist_pos {K L : Set Plane} (hK : IsCompact K) (hL : IsCompact L) (hd : Disjoint K L) : ∃ ρ > 0, ∀ p ∈ K, ∀ q ∈ L, ρ ≤ dist p q

Lemma 1.4 (b) (compact separation). Two disjoint nonempty compact sets have positive distance.

theorem Schoenflies.Plane.exists_ball_subset_diff {K U : Set Plane} {x : Plane} (hU : IsOpen U) (hK : IsCompact K) (hx : x ∈ U \ K) : ∃ ρ > 0, Metric.ball x ρ ⊆ U \ K

Lemma 1.4 (c) (compact separation). A point of an open set off a compact set has a ball inside the difference.

theorem Schoenflies.Plane.eq_singleton_iInter_of_diam_tendsto_zero {K : ℕ → Set Plane} (hne : ∀ (n : ℕ), (K n).Nonempty) (hK : ∀ (n : ℕ), IsCompact (K n)) (hmono : Antitone K) (hdiam : Filter.Tendsto (fun (n : ℕ) => Metric.diam (K n)) Filter.atTop (nhds 0)) : ∃ (p : Plane), ⋂ (n : ℕ), K n = {p}

Lemma 1.6 (nested compact singleton). A decreasing sequence of nonempty compact sets whose diameters tend to 0 has a single point in its intersection.

theorem Schoenflies.Plane.connectedComponentIn_eq_of_frontier_disjoint {U V : Set Plane} {x : Plane} (hU : IsOpen U) (hUconn : IsPreconnected U) (hsub : U ⊆ V) (hfr : frontier U ∩ V = ∅) (hx : x ∈ U) : connectedComponentIn V x = U

Lemma 1.7 (recognizing a component). A region inside an open set whose frontier misses that open set is a connected component of it.