Added the Mean Value Theorem.

src/topology/main/local-path-connected.tex

@@ -0,0 +1,25 @@
+\section{Local Path-Connectedness}
+\label{section:local-path-connected}
+
+\begin{definition}[Locally Path-Connected]
+\label{definition:locally-path-connected}
+    Let $X$ be a topological space, then $X$ is \textbf{locally path-connected} if for every $x \in X$, there exists a fundamental system of neighbourhoods consisting of path-connected sets at $x$.
+\end{definition}
+
+\begin{proposition}
+\label{proposition:locally-path-connected-properties}
+    Let $X$ be a locally path-connected space, then
+    \begin{enumerate}
+        \item The path components of $X$ are open.
+        \item The path components of $X$ are equal to its components.
+        \item $X$ is connected if and only if it is path-connected.
+        \item Every open subset of $X$ is locally path-connected.
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    (1): Let $A \subset X$ be a path component and $x \in A$, then there exists $U \in \cn(x)$ connected. By \ref{proposition:path-connected-union}, $A \cup U \in \cn(x)$ is also connected. Since $A$ is a path-component, $A \cup U \subset A \in \cn(x)$. Thus $A$ is open by \ref{lemma:openneighbourhood}.
+
+    (2): Let $P$ be a path component in $X$ and $C \supset P$ be its connected components. If $C$ is not path-connected, then $P \subsetneq C$ there exists path-components $\seqi{P} \subset 2^C$ such that $C = \bigsqcup_{i \in I}P_i$. In which case, $C \setminus P$ is open by (1), and $C$ is not connected, which is impossible.
+
+    (3): By (2) applied to $X$.
+\end{proof}