From 677420afe0ae649e42034962d546ad6e43e9921e Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Sun, 23 Apr 2023 08:52:37 -0600
Subject: [PATCH] Add sorry's to Apostol exercise set.

---
 OneVariableCalculus/Exercises.lean            |  3 ++-
 .../Exercises/Exercises_1_7.lean              | 20 ++++++++++++++++++-
 2 files changed, 21 insertions(+), 2 deletions(-)

diff --git a/OneVariableCalculus/Exercises.lean b/OneVariableCalculus/Exercises.lean
index 2319674..9e6a5bc 100644
--- a/OneVariableCalculus/Exercises.lean
+++ b/OneVariableCalculus/Exercises.lean
@@ -1 +1,2 @@
-import OneVariableCalculus.Exercises.Exercises_I_3_12
\ No newline at end of file
+import OneVariableCalculus.Exercises.Exercises_I_3_12
+import OneVariableCalculus.Exercises.Exercises_1_7
\ No newline at end of file
diff --git a/OneVariableCalculus/Exercises/Exercises_1_7.lean b/OneVariableCalculus/Exercises/Exercises_1_7.lean
index 6eb4f6f..3bae1d6 100644
--- a/OneVariableCalculus/Exercises/Exercises_1_7.lean
+++ b/OneVariableCalculus/Exercises/Exercises_1_7.lean
@@ -1,6 +1,11 @@
 /-
 Exercises 1.7
 -/
+import OneVariableCalculus.Real.Geometry.Area
+import OneVariableCalculus.Real.Geometry.Rectangle
+
+open Real
+open Real.Geometry.Area
 
 -- ========================================
 -- The properties of area in this set of exercises are to be deduced from the
@@ -16,7 +21,20 @@ Exercises 1.7
 -- (c) The union of a finite collection of line segments in a plane.
 -- ----------------------------------------
 
--- # TODO
+example (p : Point)
+  : p.set_def ∈ 𝓜
+  ∧ ((h : p.set_def ∈ 𝓜) → area h = 0) :=
+  sorry
+
+example (S : Set Point) (hf : Set.Finite S)
+  : (⋃ p ∈ S, p.set_def) ∈ 𝓜
+  ∧ ((h : (⋃ p ∈ S, p.set_def) ∈ 𝓜) → area h = 0) :=
+  sorry
+
+example (S : Set LineSegment) (hf : Set.Finite S)
+  : (⋃ s ∈ S, s.set_def) ∈ 𝓜
+  ∧ ((h : (⋃ s ∈ S, s.set_def) ∈ 𝓜) → area h = 0) :=
+  sorry
 
 -- ----------------------------------------
 -- Exercise 2