reword

bsubercaseaux · Jun 9, 2024 · 39f9137 · 39f9137
1 parent f7a232b
commit 39f9137
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/ITP/geometry.tex b/ITP/geometry.tex
@@ -16,7 +16,7 @@
 def ConvexEmptyIn (S P : Set Point) : Prop :=
     ConvexIndep S ∧ EmptyShapeIn S P
 
-/-- `HasEmptyKGon k P' means that `P' has a convex `k'-gon in `P' -/
+/-- `HasEmptyKGon k P' means that `P' has a convex, empty `k'-gon -/
 def HasEmptyKGon (k : Nat) (P : Set Point) : Prop :=
     ∃ S : Finset Point, S.card = k ∧ ↑S ⊆ P ∧ ConvexEmptyIn S P
 \end{lstlisting}