Lines in the plane

A line is the range of the parametrization t ↦ lineMap a b t = a + t • (b - a) through two points. Taking the range of the parametrization as the definition, rather than affineSpan ℝ {a, b}, is deliberate: every proof below transports a subset of the line to a subset of ℝ and back, so the parametrization has to be available at once. line_eq_affineSpan records that the two descriptions agree, for a consumer that meets a line as a span.

The transport is a homeomorphism, but it is never bundled as one. Instead the inverse lineCoord a b x = ⟪x - a, b - a⟫ / ‖b - a‖² is defined on the whole plane, is continuous there, and is a two-sided inverse of the parametrization on the line (lineCoord_lineMap, lineMap_lineCoord). Pushing a subset of the line forward along lineCoord and pulling it back along lineMap is all that the arguments below need, and no subspace topology ever appears.

The two facts Appendix C item 1 asks for:

• a nondegenerate compact connected subset of a line is a closed segment;
• a component of the intersection of a line with a bounded open set is a bounded open segment, whose closure is a closed segment with endpoints in the frontier of the open set.

The second is what manufactures crosscuts — the blueprint uses it twice in the proof of the K₃,₃-subdivision corollary ("the closure E of the component of ℓ ∩ F containing y is a crosscut of F") — so its endpoint conclusion is stated as membership in frontier U, and not merely in closure U.

Blueprint

• Plane.line, Plane.lineCoord — Appendix C, item 1 (lines and their parametrization).
• Plane.exists_segment_eq_of_isCompact_isConnected, Plane.exists_segment_eq_of_not_subsingleton — Appendix C, item 1: a nondegenerate compact connected subset of a line is a closed segment.
• Plane.exists_openSegment_eq_connectedComponentIn — Appendix C, item 1: a component of the intersection of a line with a bounded open set is an open segment whose closure is a closed segment with endpoints in the frontier of the open set.
• Plane.eqOn_line_of_fixed — Appendix C, item 1: an affine map fixing two points of a line fixes that line pointwise.
• Plane.affineMap_ext_of_affineIndependent — Appendix C, item 1: an affine map of the plane is determined by its values at three affinely independent points.

exists_Ioo_eq_connectedComponentIn is the one-dimensional core: a component of a bounded open subset of ℝ is an open interval whose endpoints are outside the set.

The real line

A component of a bounded open subset of ℝ is a bounded open interval whose endpoints are missing from the set. Everything the plane statement says about a component of ℓ ∩ U is this fact transported along the parametrization.

theorem Schoenflies.exists_Ioo_eq_connectedComponentIn {T : Set ℝ} (hopen : IsOpen T) (hbdd : Bornology.IsBounded T) {s : ℝ} (hs : s ∈ T) : ∃ (t₀ : ℝ) (t₁ : ℝ), t₀ < t₁ ∧ connectedComponentIn T s = Set.Ioo t₀ t₁ ∧ t₀ ∉ T ∧ t₁ ∉ T

A connected component of a bounded open subset of ℝ is an open interval Ioo t₀ t₁ with t₀ < t₁, and neither endpoint belongs to the set.

Lines and their parametrization

def Schoenflies.Plane.line (a b : Plane) : Set Plane

The line through a and b: the range of the parametrization t ↦ a + t • (b - a). For a = b this degenerates to the single point {a}; the lemmas that need a genuine line take a ≠ b as a hypothesis.

Equations

• a.line b = Set.range ⇑(AffineMap.lineMap a b)

noncomputable def Schoenflies.Plane.lineCoord (a b x : Plane) : ℝ

The coordinate of a point on the line through a and b: the inverse of the parametrization. It is defined on the whole plane — off the line it returns the parameter of the orthogonal projection, which is harmless and buys continuity everywhere.

Equations

• a.lineCoord b x = inner ℝ (x - a) (b - a) / ‖b - a‖ ^ 2

theorem Schoenflies.Plane.mem_line_iff {a b x : Plane} : x ∈ a.line b ↔ ∃ (t : ℝ), (AffineMap.lineMap a b) t = x

theorem Schoenflies.Plane.lineMap_mem_line (a b : Plane) (t : ℝ) : (AffineMap.lineMap a b) t ∈ a.line b

@[simp]

theorem Schoenflies.Plane.left_mem_line (a b : Plane) : a ∈ a.line b

@[simp]

theorem Schoenflies.Plane.right_mem_line (a b : Plane) : b ∈ a.line b

theorem Schoenflies.Plane.line_eq_affineSpan (a b : Plane) : a.line b = ↑line[ℝ, a, b]

The range of the parametrization is the affine span of the two points.

theorem Schoenflies.Plane.continuous_lineCoord (a b : Plane) : Continuous (a.lineCoord b)

@[simp]

theorem Schoenflies.Plane.lineCoord_lineMap {a b : Plane} (hab : a ≠ b) (t : ℝ) : a.lineCoord b ((AffineMap.lineMap a b) t) = t

lineCoord inverts the parametrization on the left.

theorem Schoenflies.Plane.lineMap_lineCoord {a b x : Plane} (hx : x ∈ a.line b) : (AffineMap.lineMap a b) (a.lineCoord b x) = x

lineCoord inverts the parametrization on the right, on the line. This needs no nondegeneracy hypothesis: for a = b both sides are a.

theorem Schoenflies.Plane.lineMap_injective {a b : Plane} (hab : a ≠ b) : Function.Injective ⇑(AffineMap.lineMap a b)

theorem Schoenflies.Plane.isClosed_line (a b : Plane) : IsClosed (a.line b)

A line is closed: it is the set where the parametrization undoes the coordinate.

theorem Schoenflies.Plane.mem_line_iff_det_eq_zero {a b x : Plane} (hab : a ≠ b) : x ∈ a.line b ↔ (b - a).det (x - a) = 0

The angle-free membership test: x lies on the line through a ≠ b exactly when the orientation form kills the two directions.

A compact connected subset of a line is a segment

theorem Schoenflies.Plane.exists_segment_eq_of_isCompact_isConnected {a b : Plane} {S : Set Plane} (hS : S ⊆ a.line b) (hcompact : IsCompact S) (hconn : IsConnected S) : ∃ (p : Plane) (q : Plane), p ∈ S ∧ q ∈ S ∧ S = segment ℝ p q

Appendix C, item 1. A nonempty compact connected subset of a line is a closed segment, whose endpoints belong to the set.

theorem Schoenflies.Plane.exists_segment_eq_of_not_subsingleton {a b : Plane} {S : Set Plane} (hS : S ⊆ a.line b) (hcompact : IsCompact S) (hconn : IsConnected S) (hnontriv : ¬S.Subsingleton) : ∃ (p : Plane) (q : Plane), p ≠ q ∧ p ∈ S ∧ q ∈ S ∧ S = segment ℝ p q

Appendix C, item 1, in the form the blueprint states it: a nondegenerate compact connected subset of a line is a closed segment with distinct endpoints.

A component of a line inside a bounded open set

theorem Schoenflies.Plane.exists_openSegment_eq_connectedComponentIn {a b y : Plane} {U : Set Plane} (hab : a ≠ b) (hU : IsOpen U) (hbdd : Bornology.IsBounded U) (hy : y ∈ a.line b ∩ U) : ∃ (p : Plane) (q : Plane), p ≠ q ∧ p ∈ a.line b ∧ q ∈ a.line b ∧ connectedComponentIn (a.line b ∩ U) y = openSegment ℝ p q ∧ closure (connectedComponentIn (a.line b ∩ U) y) = segment ℝ p q ∧ p ∈ frontier U ∧ q ∈ frontier U

Appendix C, item 1. A connected component of the intersection of a line with a bounded open set U is an open segment of the line; its closure is the closed segment on the same two distinct endpoints, and both endpoints lie in the frontier of U.

This is the crosscut factory: the closed segment meets U in exactly the component, and touches ∂U exactly at its two ends.

Affine maps

theorem Schoenflies.Plane.eqOn_line_of_fixed {a b : Plane} (F : Plane →ᵃ[ℝ] Plane) (ha : F a = a) (hb : F b = b) : Set.EqOn (⇑F) id (a.line b)

Appendix C, item 1. An affine map fixing two points fixes their line pointwise.

theorem Schoenflies.Plane.affineMap_ext_of_affineIndependent {p : Fin 3 → Plane} (hp : AffineIndependent ℝ p) (F G : Plane →ᵃ[ℝ] Plane) (h : ∀ (i : Fin 3), F (p i) = G (p i)) : F = G

Appendix C, item 1. An affine map of the plane is determined by its values at three affinely independent points.