Revise geometry with different types of rectangles and lines.

Bookshelf/Apostol.tex

@@ -82,7 +82,7 @@ A collection of points satisfying \eqref{sec:partition-eq1} is called a
 
 \begin{definition}
 
-  \lean{Common/Set/Intervals/Partition}{Set.Intervals.Partition}
+  \lean{Common/Set/Partition}{Set.Partition}
 
 \end{definition}
 
@@ -114,7 +114,7 @@ That is to say, for each $k = 1, 2, \ldots, n$, there is a real number $s_k$
 
 \begin{definition}
 
-  \lean{Common/Set/Intervals/StepFunction}{Set.Intervals.StepFunction}
+  \lean{Common/Geometry/StepFunction}{Geometry.StepFunction}
 
 \end{definition}
 
@@ -570,7 +570,7 @@ For each set $S$ in $\mathscr{M}$, we have $a(S) \geq 0$.
 
 \begin{axiom}
 
-  \leanPretty{Common/Real/Geometry/Area}{Nonnegative-Property}
+  \leanPretty{Common/Geometry/Area}{Nonnegative-Property}
     {Nonnegative Property}
 
 \end{axiom}
@@ -583,7 +583,7 @@ If $S$ and $T$ are in $\mathscr{M}$, then $S \cup T$ and $S \cap T$ are in
 
 \begin{axiom}
 
-  \leanPretty{Common/Real/Geometry/Area}{Additive-Property}
+  \leanPretty{Common/Geometry/Area}{Additive-Property}
     {Additive Property}
 
 \end{axiom}
@@ -596,7 +596,7 @@ If $S$ and $T$ are in $\mathscr{M}$ with $S \subseteq T$, then $T - S$ is in
 
 \begin{axiom}
 
-  \leanPretty{Common/Real/Geometry/Area}{Difference-Property}
+  \leanPretty{Common/Geometry/Area}{Difference-Property}
     {Difference Property}
 
 \end{axiom}
@@ -609,7 +609,7 @@ If a set $S$ is in $\mathscr{M}$ and if $T$ is congruent to $S$, then $T$ is
 
 \begin{axiom}
 
-  \leanPretty{Common/Real/Geometry/Area}{Invariance-Under-Congruence}
+  \leanPretty{Common/Geometry/Area}{Invariance-Under-Congruence}
     {Invariance Under Congruence}
 
 \end{axiom}
@@ -622,7 +622,7 @@ If the edges of $R$ have lengths $h$ and $k$, then $a(R) = hk$.
 
 \begin{axiom}
 
-  \leanPretty{Common/Real/Geometry/Area}{Choice-of-Scale}
+  \leanPretty{Common/Geometry/Area}{Choice-of-Scale}
     {Choice of Scale}
 
 \end{axiom}
@@ -642,7 +642,7 @@ If there is one and only one number $c$ which satisfies the inequalities
 
 \begin{axiom}
 
-  \leanPretty{Common/Real/Geometry/Area}{Exhaustion-Property}
+  \leanPretty{Common/Geometry/Area}{Exhaustion-Property}
     {Exhaustion Property}
 
 \end{axiom}

Bookshelf/Apostol/Chapter_1_11.lean

@@ -1,9 +1,8 @@
 import Mathlib.Data.Real.Basic
-import Mathlib.Tactic.LibrarySearch
 
 import Common.Real.Floor
+import Common.Geometry.StepFunction
 import Common.Set.Basic
-import Common.Set.Intervals.StepFunction
 
 /-! # Apostol.Chapter_1_11 -/
 
@@ -133,8 +132,6 @@ theorem exercise_7b (ha : a > 0) (hb : b > 0) (hp : Nat.coprime a b)
 
 section
 
-open Set.Intervals
-
 /-- ### Exercise 8
 
 Let `S` be a set of points on the real line. The *characteristic function* of

Common/Geometry/Area.lean

@@ -1,7 +1,8 @@
-import Common.Real.Geometry.Rectangle
+import Common.Geometry.Basic
-import Common.Set.Intervals.StepFunction
+import Common.Geometry.Rectangle.Skew
+import Common.Geometry.StepFunction
 
-/-! # Common.Real.Geometry.Area
+/-! # Common.Geometry.Area
 
 An axiomatic foundation for the concept of *area*. These axioms are those
 outlined in [^1].
@@ -10,7 +11,7 @@ outlined in [^1].
       Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.
 -/
 
-namespace Real.Geometry.Area
+namespace Geometry.Area
 
 /--
 All *measurable sets*, i.e. sets in the plane to which an area can be assigned.
@@ -18,7 +19,7 @@ All *measurable sets*, i.e. sets in the plane to which an area can be assigned.
 The existence of such a class is assumed in the axiomatic definition of area
 introduced by Apostol. He denotes this set of sets as `𝓜`.
 -/
-axiom 𝓜 : Set (Set ℝ²)
+axiom 𝓜 : Set (Set Point)
 
 /--
 A set function mapping every *measurable set* to a value denoting its area.
@@ -33,7 +34,7 @@ axiom area : ∀ ⦃x⦄, x ∈ 𝓜 → ℝ
 For each set `S` in `𝓜`, we have `a(S) ≥ 0`.
 -/
 
-axiom area_ge_zero {S : Set ℝ²} (h : S ∈ 𝓜): area h ≥ 0
+axiom area_ge_zero {S : Set Point} (h : S ∈ 𝓜): area h ≥ 0
 
 /-! ## Additive Property
 
@@ -41,14 +42,14 @@ If `S` and `T` are in `𝓜`, then `S ∪ T` in `𝓜`, `S ∩ T` in `𝓜`, and
 `a(S ∪ T) = a(S) + a(T) - a(S ∩ T)`.
 -/
 
-axiom measureable_imp_union_measurable {S T : Set ℝ²} (hS : S ∈ 𝓜) (hT : T ∈ 𝓜)
+axiom measureable_imp_union_measurable {S T : Set Point}
-  : S ∪ T ∈ 𝓜
+  (hS : S ∈ 𝓜) (hT : T ∈ 𝓜) : S ∪ T ∈ 𝓜
 
-axiom measurable_imp_inter_measurable {S T : Set ℝ²} (hS : S ∈ 𝓜) (hT : T ∈ 𝓜)
+axiom measurable_imp_inter_measurable {S T : Set Point}
-  : S ∩ T ∈ 𝓜
+  (hS : S ∈ 𝓜) (hT : T ∈ 𝓜) : S ∩ T ∈ 𝓜
 
 axiom union_area_eq_area_add_area_sub_inter_area
-  {S T : Set ℝ²} (hS : S ∈ 𝓜) (hT : T ∈ 𝓜)
+  {S T : Set Point} (hS : S ∈ 𝓜) (hT : T ∈ 𝓜)
   : area (measureable_imp_union_measurable hS hT) =
       area hS + area hT - area (measurable_imp_inter_measurable hS hT)
 
@@ -59,11 +60,11 @@ If `S` and `T` are in `𝓜` with `S ⊆ T`, then `T - S` is in `𝓜` and
 -/
 
 axiom measureable_imp_diff_measurable
-  {S T : Set ℝ²} (hS : S ∈ 𝓜) (hT : T ∈ 𝓜) (h : S ⊆ T)
+  {S T : Set Point} (hS : S ∈ 𝓜) (hT : T ∈ 𝓜) (h : S ⊆ T)
   : T \ S ∈ 𝓜
 
 axiom diff_area_eq_area_sub_area
-  {S T : Set ℝ²} (hS : S ∈ 𝓜) (hT : T ∈ 𝓜) (h : S ⊆ T)
+  {S T : Set Point} (hS : S ∈ 𝓜) (hT : T ∈ 𝓜) (h : S ⊆ T)
   : area (measureable_imp_diff_measurable hS hT h) = area hT - area hS
 
 /-! ## Invariance Under Congruence
@@ -73,14 +74,13 @@ If a set `S` is in `𝓜` and if a set `T` is congruent to `S`, then `T` is also
 -/
 
 axiom measurable_congruent_imp_measurable
-  {S T : Set ℝ²} (hS : S ∈ 𝓜) (h : congruent S T)
+  {S T : Set Point} (hS : S ∈ 𝓜) (h : congruent S T)
   : T ∈ 𝓜
 
 axiom congruent_imp_area_eq_area
-  {S T : Set ℝ²} (hS : S ∈ 𝓜) (h : congruent S T)
+  {S T : Set Point} (hS : S ∈ 𝓜) (h : congruent S T)
   : area hS = area (measurable_congruent_imp_measurable hS h)
 
-
 /-! ## Choice of Scale
 
 (i) Every rectangle `R` is in `𝓜`.
@@ -88,10 +88,10 @@ axiom congruent_imp_area_eq_area
 (ii) If the edges of rectangle `R` have lengths `h` and `k`, then `a(R) = hk`.
 -/
 
-axiom rectangle_measurable (R : Rectangle)
+axiom rectangle_measurable (R : Rectangle.Skew)
   : R.toSet ∈ 𝓜
 
-axiom rectangle_area_eq_mul_edge_lengths (R : Rectangle)
+axiom rectangle_area_eq_mul_edge_lengths (R : Rectangle.Skew)
   : area (rectangle_measurable R) = R.width * R.height
 
 /-! ## Exhaustion Property
@@ -107,24 +107,24 @@ Every step region is measurable. This follows from the choice of scale axiom,
 and the fact all step regions are equivalent to the union of a collection of
 rectangles.
 -/
-theorem step_function_measurable (S : Set.Intervals.StepFunction ℝ)
+theorem step_function_measurable (S : StepFunction)
   : S.toSet ∈ 𝓜 := by
   sorry
 
-def forallSubsetsBetween (k : ℝ) (Q : Set ℝ²) :=
+def forallSubsetsBetween (k : ℝ) (Q : Set Point) :=
-  ∀ S T : Set.Intervals.StepFunction ℝ,
+  ∀ S T : StepFunction,
   (hS : S.toSet ⊆ Q) →
   (hT : Q ⊆ T.toSet) →
   area (step_function_measurable S) ≤ k ∧ k ≤ area (step_function_measurable T)
 
-axiom exhaustion_exists_unique_imp_measurable (Q : Set ℝ²)
+axiom exhaustion_exists_unique_imp_measurable (Q : Set Point)
   : (∃! k : ℝ, forallSubsetsBetween k Q)
   → Q ∈ 𝓜
 
-axiom exhaustion_exists_unique_imp_area_eq (Q : Set ℝ²)
+axiom exhaustion_exists_unique_imp_area_eq (Q : Set Point)
   : ∃ k : ℝ,
       (h : forallSubsetsBetween k Q ∧
         (∀ x : ℝ, forallSubsetsBetween x Q → x = k))
     → area (exhaustion_exists_unique_imp_measurable Q ⟨k, h⟩) = k
 
-end Real.Geometry.Area
+end Geometry.Area

Common/Geometry/Basic.lean

@@ -0,0 +1,38 @@
+import Common.Geometry.Point
+
+/-! # Common.Geometry.Basic
+
+Additional theorems and definitions useful in the context of geometry.
+-/
+
+namespace Geometry
+
+/--
+Two sets `S` and `T` are `similar` **iff** there exists a one-to-one
+correspondence between `S` and `T` such that the distance between any two points
+`P, Q ∈ S` and corresponding points `P', Q' ∈ T` differ by some constant `α`. In
+other words, `α|PQ| = |P'Q'|`.
+-/
+def similar (S T : Set Point) : Prop :=
+  ∃ f : Point → Point, Function.Bijective f ∧
+    ∃ s : ℝ, ∀ x y : Point, x ∈ S ∧ y ∈ T →
+      s * Point.dist x y = Point.dist (f x) (f y)
+
+/--
+Two sets are congruent if they are similar with a scaling factor of `1`.
+-/
+def congruent (S T : Set Point) : Prop :=
+  ∃ f : Point → Point, Function.Bijective f ∧
+    ∀ x y : Point, x ∈ S ∧ y ∈ T →
+      Point.dist x y = Point.dist (f x) (f y)
+
+/--
+Any two `congruent` sets must be similar to one another.
+-/
+theorem congruent_similar {S T : Set Point} : congruent S T → similar S T := by
+  intro hc
+  let ⟨f, ⟨hf, hs⟩⟩ := hc
+  conv at hs => intro x y hxy; arg 1; rw [← one_mul (Point.dist x y)]
+  exact ⟨f, ⟨hf, ⟨1, hs⟩⟩⟩
+
+end Geometry

Common/Geometry/Line.lean

@@ -0,0 +1,24 @@
+import Common.Geometry.Point
+
+/-! # Common.Geometry.Line
+
+A representation of a line in the two-dimensional Cartesian plane.
+-/
+
+namespace Geometry
+
+/--
+A `Line` is represented in vector form (not to be confused with `Vector`).
+It is completely characterized by a point `P` on the line in question and a
+direction vector `dir` parallel to the line. Such a line is represented by
+equation
+```
+\vec{r} = \vec{OP} + t\vec{d},
+```
+where `O` denotes the origin and `t ∈ ℝ`.
+-/
+structure Line where
+  p : Point
+  dir : ℝ × ℝ
+
+end Geometry

Common/Geometry/Point.lean

@@ -0,0 +1,77 @@
+import Mathlib.Data.Real.Basic
+import Mathlib.Data.Real.Sqrt
+
+import Common.Real.Trigonometry
+
+/-! # Common.Geometry.Point
+
+A representation of a point in the two-dimensional Cartesian plane.
+-/
+
+namespace Geometry
+
+structure Point where
+  x : ℝ
+  y : ℝ
+
+noncomputable instance : DecidableEq Point := by
+  intro p₁ p₂
+  have ⟨x₁, y₁⟩ := p₁
+  have ⟨x₂, y₂⟩ := p₂
+  if hp : x₁ = x₂ ∧ y₁ = y₂ then
+    rw [hp.left, hp.right]
+    exact isTrue rfl
+  else
+    rw [not_and_or] at hp
+    refine isFalse ?_
+    intro h
+    injection h with hx hy
+    apply Or.elim hp
+    · intro nx
+      exact absurd hx nx
+    · intro ny
+      exact absurd hy ny
+
+namespace Point
+
+/--
+The function mapping a `Point` to a `2`-tuple of reals.
+-/
+def toTuple (p : Point) : ℝ × ℝ := (p.x, p.y)
+
+/--
+The function mapping a `2`-tuple of reals to a `Point`.
+-/
+def fromTuple (p : ℝ × ℝ) : Point := Point.mk p.1 p.2
+
+/--
+An isomorphism between a `Point` and a `2`-tuple.
+-/
+def isoTuple : Point ≃ ℝ × ℝ :=
+  {
+    toFun := toTuple,
+    invFun := fromTuple,
+    left_inv := by
+      unfold Function.LeftInverse fromTuple toTuple
+      simp,
+    right_inv := by
+      unfold Function.RightInverse Function.LeftInverse fromTuple toTuple
+      simp
+  }
+
+/--
+The length of the straight line segment connecting points `p` and `q`.
+-/
+noncomputable def dist (p q : Point) :=
+  Real.sqrt ((abs (q.x - p.x)) ^ 2 + (abs (q.y - p.y)) ^ 2)
+
+/--
+The undirected angle at `p₂` between the line segments to `p₁` and `p₃`. If
+either of those points equals `p₂`, this is `π / 2`.
+-/
+noncomputable def angle (p₁ p₂ p₃ : Point) : ℝ :=
+  Real.euclideanAngle (toTuple p₁) (toTuple p₂) (toTuple p₃)
+
+end Point
+
+end Geometry

Common/Geometry/Rectangle.lean

@@ -0,0 +1,2 @@
+import Common.Geometry.Rectangle.Orthogonal
+import Common.Geometry.Rectangle.Skew

Common/Geometry/Rectangle/Orthogonal.lean

@@ -0,0 +1,182 @@
+import Mathlib.Data.Fin.Basic
+import Mathlib.Tactic.LibrarySearch
+
+import Common.Geometry.Point
+import Common.Geometry.Segment
+import Common.Geometry.Rectangle.Skew
+
+/-! # Common.Geometry.Rectangle.Orthogonal
+
+A characterization of an orthogonal rectangle.
+-/
+
+namespace Geometry.Rectangle
+
+/--
+An `Orthogonal` rectangle is characterized by two points on opposite corners. It
+is assumed the edges of the rectangle are parallel to the coordinate axes.
+
+A `Point` can alternatively be viewed as an `Orthogonal` rectangle in which the
+two points coincide. A horizontal or vertical `Segment` can alternatively be
+viewed as an `Orthogonal` rectangle with width or height (but not both) `0`.
+-/
+structure Orthogonal where
+  bl : Point  -- bottom left
+  tr : Point  -- top right
+
+namespace Orthogonal
+
+/--
+The width of the `Orthogonal` rectangle.
+-/
+def width (r : Orthogonal) := r.tr.x - r.bl.x
+
+/--
+The height of the `Orthogonal` rectangle.
+-/
+def height (r : Orthogonal) := r.tr.y - r.bl.y
+
+/--
+The top-left corner of the `Orthogonal` rectangle.
+-/
+def tl (r : Orthogonal) : Point := ⟨r.bl.x, r.bl.y + r.height⟩
+
+/--
+The bottom-right corner of the `Orthogonal` rectangle.
+-/
+def br (r : Orthogonal) : Point := ⟨r.bl.x + r.width, r.bl.y⟩
+
+/--
+An `Orthogonal` rectangle's top side is equal in length to its bottom side.
+-/
+theorem dist_top_eq_dist_bottom (r : Orthogonal)
+  : Point.dist r.tl r.tr = Point.dist r.bl r.br := by
+  unfold tl br Point.dist width height
+  norm_num
+
+/--
+An `Orthogonal` rectangle's left side is equal in length to its right side.
+-/
+theorem dist_left_eq_dist_right (r : Orthogonal)
+  : Point.dist r.tl r.bl = Point.dist r.tr r.br := by
+  unfold tl br Point.dist width height
+  norm_num
+
+/--
+Convert an `Orthogonal` rectangle into a `Skew` one.
+-/
+def toSkew (r : Orthogonal) : Skew := ⟨r.tl, r.bl, r.br, sorry⟩
+
+/--
+The set of `Orthogonal` rectangles are embedded in the set of `Skew` rectangles.
+-/
+def skewEmbedding : Orthogonal ↪ Skew :=
+  have : Function.Injective toSkew := by
+    unfold Function.Injective
+    intro r₁ r₂ h
+    unfold toSkew at h
+    have ⟨⟨blx₁, bly₁⟩, ⟨trx₁, try₁⟩⟩ := r₁
+    have ⟨⟨blx₂, bry₂⟩, ⟨trx₂, try₂⟩⟩ := r₂
+    simp
+    simp at h
+    unfold tl br width height at h
+    simp at h
+    exact ⟨⟨h.left.left, h.right.left.right⟩, ⟨h.right.right.left, h.left.right⟩⟩
+  ⟨toSkew, this⟩
+
+/-! ## Point -/
+
+/--
+A `Point` is an `Orthogonal` rectangle in which all points coincide.
+-/
+abbrev AsPoint := Subtype (fun r : Orthogonal => r.bl = r.tr)
+
+namespace AsPoint
+
+/--
+The function mapping an `Orthogonal` rectangle with all points coinciding to a
+`Point`.
+-/
+def toPoint (p : AsPoint) : Point := p.val.tl
+
+/--
+The function mapping a `Point` to an `Orthogonal` rectangle with all points
+coinciding.
+-/
+def fromPoint (p : Point) : AsPoint := ⟨Orthogonal.mk p p, by simp⟩
+
+/--
+An isomorphism between an `Orthogonal` rectangle with all points coinciding and
+a `Point`.
+-/
+def isoPoint : AsPoint ≃ Point :=
+  {
+    toFun := toPoint,
+    invFun := fromPoint,
+    left_inv := by
+      unfold Function.LeftInverse fromPoint toPoint
+      intro ⟨r, hr⟩
+      congr
+      repeat {
+        simp only
+        unfold tl height
+        rw [hr]
+        simp
+      }
+    right_inv := by
+      unfold Function.RightInverse Function.LeftInverse fromPoint toPoint
+      intro ⟨r, hr⟩
+      unfold tl height
+      simp
+  }
+
+/--
+The width of an `AsPoint` is `0`.
+-/
+theorem width_eq_zero (p : AsPoint) : p.val.width = 0 := by
+  unfold Orthogonal.width
+  rw [p.property]
+  simp
+
+/--
+The height of an `AsPoint` is `0`.
+-/
+theorem height_eq_zero (p : AsPoint) : p.val.height = 0 := by
+  unfold Orthogonal.height
+  rw [p.property]
+  simp
+
+end AsPoint
+
+/-! ## Segment -/
+
+/--
+A `Segment` is an `Orthogonal` rectangle either width or height equal to `0`.
+-/
+abbrev AsSegment := Subtype (fun r : Orthogonal =>
+  (r.bl.x = r.tr.x ∧ r.bl.y ≠ r.tr.y) ∨ (r.bl.x ≠ r.tr.x ∧ r.bl.y = r.tr.y))
+
+namespace AsSegment
+
+/--
+Either the width or height of an `AsSegment` is zero.
+-/
+theorem width_or_height_eq_zero (s : AsSegment)
+  : s.val.width = 0 ∨ s.val.height = 0 := by
+  apply Or.elim s.property
+  · intro h
+    refine Or.inl ?_
+    unfold width
+    rw [h.left]
+    simp
+  · intro h
+    refine Or.inr ?_
+    unfold height
+    rw [h.right]
+    simp
+
+end AsSegment
+
+end Orthogonal
+
+end Geometry.Rectangle

Common/Geometry/Rectangle/Skew.lean

@@ -0,0 +1,176 @@
+import Common.Geometry.Point
+import Common.Geometry.Segment
+import Common.Real.Trigonometry
+
+/-! # Common.Geometry.Rectangle.Skew
+
+A characterization of a skew rectangle.
+-/
+
+namespace Geometry.Rectangle
+
+/--
+A `Skew` rectangle is characterized by three points and the angle formed between
+them.
+
+A `Point` can alternatively be viewed as a `Skew` rectangle in which all three
+points coincide. A `Segment` can alternatively be viewed as a `Skew` rectangle
+in which two of the three points coincide. Note that, by definition of
+`Point.angle`, such a situation does indeed yield an angle of `π / 2`.
+-/
+structure Skew where
+  tl : Point  -- top left
+  bl : Point  -- bottom left
+  br : Point  -- bottom right
+  has_right_angle : Point.angle tl bl br = Real.pi / 2
+
+namespace Skew
+
+/--
+The top-right corner of the `Skew` rectangle.
+-/
+def tr (r : Skew) : Point :=
+  ⟨r.tl.x + r.br.x - r.bl.x, r.tl.y + r.br.y - r.bl.y⟩
+
+/--
+A `Skew` rectangle's top side is equal in length to its bottom side.
+-/
+theorem dist_top_eq_dist_bottom (r : Skew)
+  : Point.dist r.tl r.tr = Point.dist r.bl r.br := by
+  unfold tr Point.dist
+  simp only
+  repeat rw [add_comm, sub_right_comm, add_sub_cancel']
+
+/--
+A `Skew` rectangle's left side is equal in length to its right side.
+-/
+theorem dist_left_eq_dist_right (r : Skew)
+  : Point.dist r.tl r.bl = Point.dist r.tr r.br := by
+  unfold tr Point.dist
+  simp only
+  repeat rw [
+    sub_sub_eq_add_sub,
+    add_comm,
+    sub_add_eq_sub_sub,
+    sub_right_comm,
+    add_sub_cancel'
+  ]
+
+/--
+Computes the width of a `Skew` rectangle.
+-/
+noncomputable def width (r : Skew) : ℝ :=
+  Point.dist r.bl r.br
+
+/--
+Computes the height of a `Skew` rectangle.
+-/
+noncomputable def height (r : Skew) : ℝ :=
+  Point.dist r.bl r.tl
+
+/--
+A mapping from a `Skew` rectangle to the set describing the region enclosed by
+the rectangle.
+-/
+def toSet (r : Skew) : Set Point := sorry
+
+/-! ## Point -/
+
+/--
+A `Point` is a `Skew` rectangle in which all points coincide.
+-/
+abbrev AsPoint := Subtype (fun r : Skew => r.tl = r.bl ∧ r.bl = r.br)
+
+namespace AsPoint
+
+/--
+The function mapping a `Skew` rectangle with all points coinciding to a `Point`.
+-/
+def toPoint (p : AsPoint) : Point := p.val.tl
+
+/--
+The function mapping a `Point` to a `Skew` rectangle with all points coinciding.
+-/
+def fromPoint (p : Point) : AsPoint :=
+  have hp : Point.angle p p p = Real.pi / 2 := by
+    unfold Point.angle Real.euclideanAngle
+    simp
+  ⟨Skew.mk p p p hp, by simp⟩
+
+/--
+An isomorphism between a `Skew` rectangle with all points coinciding and a
+`Point`.
+-/
+def isoPoint : AsPoint ≃ Point :=
+  {
+    toFun := toPoint,
+    invFun := fromPoint,
+    left_inv := by
+      unfold Function.LeftInverse fromPoint toPoint
+      simp only
+      intro p
+      congr
+      · exact p.property.left
+      · rw [p.property.left]
+        exact p.property.right
+    right_inv := by
+      unfold Function.RightInverse Function.LeftInverse fromPoint toPoint
+      simp only
+      intro _
+      triv
+  }
+
+/--
+The width of an `AsPoint` is `0`.
+-/
+theorem width_eq_zero (p : AsPoint) : p.val.width = 0 := by
+  unfold Skew.width
+  rw [p.property.right]
+  unfold Point.dist
+  simp
+
+/--
+The height of an `AsPoint` is `0`.
+-/
+theorem height_eq_zero (p : AsPoint) : p.val.height = 0 := by
+  unfold Skew.height
+  rw [p.property.left]
+  unfold Point.dist
+  simp
+
+end AsPoint
+
+/-! ## Segment -/
+
+/--
+A `Segment` is a `Skew` rectangle in which two of three points coincide.
+-/
+abbrev AsSegment := Subtype (fun r : Skew =>
+  (r.tl = r.bl ∧ r.bl ≠ r.br) ∨ (r.tl ≠ r.bl ∧ r.bl = r.br))
+
+namespace AsSegment
+
+/--
+Either the width or height of an `AsSegment` is zero.
+-/
+theorem width_or_height_eq_zero (s : AsSegment)
+  : s.val.width = 0 ∨ s.val.height = 0 := by
+  apply Or.elim s.property
+  · intro h
+    refine Or.inr ?_
+    unfold height
+    rw [h.left]
+    unfold Point.dist
+    simp
+  · intro h
+    refine Or.inl ?_
+    unfold width
+    rw [h.right]
+    unfold Point.dist
+    simp
+
+end AsSegment
+
+end Skew
+
+end Geometry.Rectangle

Common/Geometry/Segment.lean

@@ -0,0 +1,19 @@
+import Common.Geometry.Point
+
+/-! # Common.Geometry.Segment
+
+A representation of a line segment in the two-dimensional Cartesian plane.
+-/
+
+namespace Geometry
+
+/--
+A characterization of a line segment.
+
+The segment comprises of all points between points `p` and `q`, inclusive.
+-/
+structure Segment where
+  p : Point
+  q : Point
+
+end Geometry

Common/Geometry/StepFunction.lean

@@ -0,0 +1,34 @@
+import Common.Geometry.Point
+import Common.Set.Partition
+
+/-! # Common.Geometry.StepFunction
+
+Characterization of step functions.
+-/
+
+namespace Geometry
+
+open Set Partition
+
+/--
+A function `f`, whose domain is a closed interval `[a, b]`, is a `StepFunction`
+if there exists a `Partition` `P = {x₀, x₁, …, xₙ}` of `[a, b]` such that `f` is
+constant on each open subinterval of `P`.
+-/
+structure StepFunction where
+  p : Partition ℝ
+  toFun : ∀ x ∈ p.toIcc, ℝ
+  const_open_subintervals :
+    ∀ (hI : I ∈ p.openSubintervals), ∃ c, ∀ (hy : y ∈ I),
+      toFun y (mem_open_subinterval_mem_closed_interval hI hy) = c
+
+namespace StepFunction
+
+/--
+The ordinate set of the function.
+-/
+def toSet (s : StepFunction) : Set Point := sorry
+
+end StepFunction
+
+end Geometry

Common/Real.lean

@@ -1,4 +1,4 @@
-import Common.Real.Basic
+import Common.Real.Floor
-import Common.Real.Geometry
 import Common.Real.Rational
 import Common.Real.Sequence
+import Common.Real.Trigonometry

Common/Real/Basic.lean

@@ -1,30 +0,0 @@
-import Mathlib.Data.Real.Basic
-
-/-! # Common.Real.Basic
-
-A collection of basic notational conveniences.
--/
-
-/--
-An abbreviation of `ℝ²` as the Cartesian product `ℝ × ℝ`.
--/
-notation "ℝ²" => ℝ × ℝ
-
-namespace Real
-
-/--
-Definitionally, the area of a unit circle.
-
-###### PORT
-
-As of now, this remains an `axiom`, but it should be replaced by the definition
-in `Mathlib` once ported to Lean 4.
--/
-axiom pi : ℝ
-
-/--
-An abbreviation of `pi` as symbol `π`.
--/
-notation "π" => pi
-
-end Real

Common/Real/Geometry.lean

@@ -1,3 +0,0 @@
-import Common.Real.Geometry.Area
-import Common.Real.Geometry.Basic
-import Common.Real.Geometry.Rectangle

Common/Real/Geometry/Basic.lean

@@ -1,62 +0,0 @@
-import Mathlib.Data.Real.Sqrt
-
-import Common.Real.Basic
-
-/-! # Common.Real.Geometry.Basic
-
-A collection of useful definitions and theorems around geometry.
--/
-
-namespace Real
-
-/--
-The undirected angle at `p₂` between the line segments to `p₁` and `p₃`. If
-either of those points equals `p₂`, this is `π / 2`.
-
-###### PORT
-
-This should be replaced with the original Mathlib `geometry.euclidean.angle`
-definition once ported.
--/
-axiom angle (p₁ p₂ p₃ : ℝ²) : ℝ
-
-noncomputable def euclideanAngle (p₁ p₂ p₃ : ℝ²) :=
-  if p₁ = p₂ ∨ p₂ = p₃ then π / 2 else angle p₁ p₂ p₃
-
-notation "∠" => euclideanAngle
-
-/--
-Determine the distance between two points in `ℝ²`.
--/
-noncomputable def dist (x y : ℝ²) :=
-  Real.sqrt ((abs (y.1 - x.1)) ^ 2 + (abs (y.2 - x.2)) ^ 2)
-
-/--
-Two sets `S` and `T` are `similar` **iff** there exists a one-to-one
-correspondence between `S` and `T` such that the distance between any two points
-`P, Q ∈ S` and corresponding points `P', Q' ∈ T` differ by some constant `α`. In
-other words, `α|PQ| = |P'Q'|`.
--/
-def similar (S T : Set ℝ²) : Prop :=
-  ∃ f : ℝ² → ℝ², Function.Bijective f ∧
-    ∃ s : ℝ, ∀ x y : ℝ², x ∈ S ∧ y ∈ T →
-      s * dist x y = dist (f x) (f y)
-
-/--
-Two sets are congruent if they are similar with a scaling factor of `1`.
--/
-def congruent (S T : Set (ℝ × ℝ)) : Prop :=
-  ∃ f : ℝ² → ℝ², Function.Bijective f ∧
-    ∀ x y : ℝ², x ∈ S ∧ y ∈ T →
-      dist x y = dist (f x) (f y)
-
-/--
-Any two `congruent` sets must be similar to one another.
--/
-theorem congruent_similar {S T : Set ℝ²} : congruent S T → similar S T := by
-  intro hc
-  let ⟨f, ⟨hf, hs⟩⟩ := hc
-  conv at hs => intro x y hxy; arg 1; rw [← one_mul (dist x y)]
-  exact ⟨f, ⟨hf, ⟨1, hs⟩⟩⟩
-
-end Real

Common/Real/Geometry/Rectangle.lean

@@ -1,147 +0,0 @@
-import Common.Real.Geometry.Basic
-
-/-! # Common.Real.Geometry.Rectangle
-
-A characterization of a rectangle. This follows the definition as outlined in
-[^1]. Note that a `Point` and a `LineSegment` are both considered rectangles,
-with one or both dimensions equal to `0` respectively.
-
-[^1]: Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an
-      Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.
--/
-
-namespace Real
-
-/--
-A `Rectangle` is characterized by three distinct points and the angle formed
-between line segments originating from the "bottom left" point.
--/
-structure Rectangle where
-  top_left : ℝ²
-  bottom_left : ℝ²
-  bottom_right : ℝ²
-  forms_right_angle : ∠ top_left bottom_left bottom_right = π / 2
-
-namespace Rectangle
-
-/--
-The top-right corner of the rectangle, oriented with respect to the other
-vertices.
--/
-def topRight (r : Rectangle) : ℝ² :=
-  ( r.top_left.fst + r.bottom_right.fst - r.bottom_left.fst
-  , r.top_left.snd + r.bottom_right.snd - r.bottom_left.snd
-  )
-
-/--
-A `Rectangle` is the locus of points bounded by its edges.
--/
-def toSet (r : Rectangle) : Set ℝ² :=
-  sorry
-
-/--
-A `Rectangle`'s top side is equal in length to its bottom side.
--/
-theorem dist_top_eq_dist_bottom (r : Rectangle)
-  : dist r.top_left r.topRight = dist r.bottom_left r.bottom_right := by
-  unfold topRight dist
-  repeat rw [add_comm, sub_right_comm, add_sub_cancel']
-
-/--
-A `Rectangle`'s left side is equal in length to its right side.
--/
-theorem dist_left_eq_dist_right (r : Rectangle)
-  : dist r.top_left r.bottom_left = dist r.topRight r.bottom_right := by
-  unfold topRight dist
-  repeat rw [
-    sub_sub_eq_add_sub,
-    add_comm,
-    sub_add_eq_sub_sub,
-    sub_right_comm,
-    add_sub_cancel'
-  ]
-  
-/--
-Computes the width of a `Rectangle`.
--/
-noncomputable def width (r : Rectangle) : ℝ :=
-  dist r.bottom_left r.bottom_right
-
-/--
-Computes the height of a `Rectangle`.
--/
-noncomputable def height (r : Rectangle) : ℝ :=
-  dist r.bottom_left r.top_left
-
-end Rectangle
-
-/--
-A `Point` is a `Rectangle` in which all points coincide.
--/
-abbrev Point := Subtype (fun r : Rectangle =>
-  r.top_left = r.bottom_left ∧ r.bottom_left = r.bottom_right)
-
-namespace Point
-
-/--
-A `Point` is the set consisting of just itself.
--/
-def toSet (p : Point) : Set ℝ² := p.val.toSet
-
-/--
-The width of a `Point` is `0`.
--/
-theorem width_eq_zero (p : Point) : p.val.width = 0 := by
-  unfold Rectangle.width
-  rw [p.property.right]
-  unfold dist
-  simp
-
-/--
-The height of a `Point` is `0`.
--/
-theorem height_eq_zero (p : Point) : p.val.height = 0 := by
-  unfold Rectangle.height
-  rw [p.property.left]
-  unfold dist
-  simp
-
-end Point
-
-/--
-A `LineSegment` is a `Rectangle` in which two of the three points coincide.
--/
-abbrev LineSegment := Subtype (fun r : Rectangle =>
-  (r.top_left = r.bottom_left ∧ r.bottom_left ≠ r.bottom_right) ∨
-  (r.top_left ≠ r.bottom_left ∧ r.bottom_left = r.bottom_right))
-
-namespace LineSegment
-
-/--
-A `LineSegment` `s` is the set of points corresponding to the shortest line
-segment joining the two distinct points of `s`.
--/
-def toSet (s : LineSegment) : Set ℝ² := s.val.toSet
-
-/--
-Either the width or height of a `LineSegment` is zero.
--/
-theorem width_or_height_eq_zero (s : LineSegment)
-  : s.val.width = 0 ∨ s.val.height = 0 := by
-  apply Or.elim s.property
-  · intro h
-    refine Or.inr ?_
-    unfold Rectangle.height
-    rw [h.left]
-    unfold dist
-    simp
-  · intro h
-    refine Or.inl ?_
-    unfold Rectangle.width
-    rw [h.right]
-    unfold dist
-    simp
-
-end LineSegment
-
-end Real

Common/Real/Rational.lean

@@ -1,4 +1,4 @@
-import Common.Real.Basic
+import Mathlib.Data.Real.Basic
 
 /-! # Common.Real.Rational
 

Common/Real/Trigonometry.lean

@@ -0,0 +1,26 @@
+import Mathlib.Data.Real.Basic
+
+/-! # Common.Real.Trigonometry
+
+Additional theorems and definitions useful in the context of trigonometry. Most
+of these will likely be deleted once the corresponding functions in `Mathlib`
+are ported to Lean 4.
+-/
+
+namespace Real
+
+/--
+The standard `π` variable with value `3.14159...`.
+-/
+axiom pi : ℝ
+
+/--
+The undirected angle at `p₂` between the line segments to `p₁` and `p₃`. If
+either of those points equals `p₂`, this is `π / 2`.
+-/
+axiom angle (p₁ p₂ p₃ : ℝ × ℝ) : ℝ
+
+noncomputable def euclideanAngle (p₁ p₂ p₃ : ℝ × ℝ) :=
+  if p₁ = p₂ ∨ p₂ = p₃ then pi / 2 else angle p₁ p₂ p₃
+
+end Real

Common/Set.lean

@@ -1,2 +1,2 @@
 import Common.Set.Basic
-import Common.Set.Intervals
+import Common.Set.Partition

Common/Set/Intervals.lean

@@ -1,2 +0,0 @@
-import Common.Set.Intervals.Partition
-import Common.Set.Intervals.StepFunction

Common/Set/Intervals/StepFunction.lean

@@ -1,35 +0,0 @@
-import Common.List.Basic
-import Common.Set.Intervals.Partition
-
-/-! # Common.Set.Intervals.StepFunction
-
-Characterization of step functions.
--/
-
-namespace Set.Intervals
-
-open Partition
-
-/--
-A function `f`, whose domain is a closed interval `[a, b]`, is a `StepFunction`
-if there exists a `Partition` `P = {x₀, x₁, …, xₙ}` of `[a, b]` such that `f` is
-constant on each open subinterval of `P`.
--/
-structure StepFunction (α : Type _) [Preorder α] [@DecidableRel α LT.lt] where
-  p : Partition α
-  toFun : ∀ x ∈ p.toIcc, α
-  const_open_subintervals :
-    ∀ (hI : I ∈ p.openSubintervals), ∃ c : α, ∀ (hy : y ∈ I),
-      toFun y (mem_open_subinterval_mem_closed_interval hI hy) = c
-
-namespace StepFunction
-
-/--
-The locus of points between the `x`-axis and the function.
--/
-def toSet [Preorder α] [@DecidableRel α LT.lt]
-  (s : StepFunction α) : Set (α × α) := sorry
-
-end StepFunction
-
-end Set.Intervals

Common/Set/Partition.lean

@@ -4,12 +4,12 @@ import Mathlib.Data.Set.Intervals.Basic
 
 import Common.List.Basic
 
-/-! # Common.Set.Intervals.Partition
+/-! # Common.Set.Partition
 
 Additional theorems and definitions useful in the context of sets.
 -/
 
-namespace Set.Intervals
+namespace Set
 
 open List
 
@@ -134,4 +134,4 @@ theorem mem_open_subinterval_mem_closed_interval
 
 end Partition
 
-end Set.Intervals
+end Set