Added path lemma.

src/dg/complex/space.tex

@@ -38,3 +38,15 @@
 
     (C1) $\Leftrightarrow$ (C2): By the \hyperref[Arzelà-Ascoli Theorem]{theorem:arzela-ascoli}.
 \end{proof}
+
+\begin{definition}[Space of Holomorphic Functions Near a Set]
+\label{definition:holomorphic-function-space-near}
+    Let $E$ be a complete separated locally convex space over $\complex$ and $A \subset \complex$. Direct $\cn_{\complex}^o(A)$ under reverse inclusion, then the inductive limit
+    \[
+    H(A; E) = \varinjlim_{U \in \cn_{\complex}^o(A)} H(U; E)
+    \]
+
+    is the \textbf{space of holomorphic functions near} $A$, and is of type (LF). 
+\end{definition}
+
+