Theorem: Interior of Jordan Curve is Subset of Image of Null-Homotopy

Let $f : \closedint 0 1 \to \R^2$ be a Jordan curve.
Let $H : \closedint 0 1 \times \closedint 0 1 \to \R^2$ be a path homotopy between $f$ and a constant loop.
Then:
:$\Int f \subseteq \Img H$
where $\Int f$ denotes the interior of $f$, and $\Img H$ denotes the image of $H$.

Proof:
Let $\map \Omega {\R^2, \map f 0}$ denote the set of all loops based at $\map f 0$, where $\R^2$ is the real number plane with euclidean topology.
Let $c_{\map f 0}: \closedint 0 1 \to \set { \map f 0 }$ be the constant loop.
That is, $c_{\map f 0}$ is the loop $c_{\map f 0} \in \map \Omega {\R^2, \map f 0}$ such that:
:$\forall t \in \closedint 0 1 : \map {c_{ \map f 0 }} t = \map f 0 $
Let $c_{\map f 0}$ be path-homotopic to $f$.
We are given that $H : \closedint 0 1 \times \closedint 0 1 \to \R^2$ is a path homotopy between $f$ and the constant loop $c_{\map f 0}$.
That is:
:$\forall s \in \closedint 0 1 : \map H {s, 0} = \map f {s} $
:$\forall s \in \closedint 0 1 : \map H {s, 1} = \map {c_{\map f 0}} {s} $
and:
:$\forall t \in \closedint 0 1 : \map H {0, t} = \map f 0 = \map f {0} $
:$\forall t \in \closedint 0 1 : \map H {1, t} = \map f 1 = \map {c_{\map f 0}} {1} $
Since $c_{\map f 0}$ is a constant loop, from Constant Loop is Loop, $c_{\map f 0}$ is a constant mapping.
We also have the image of $c_{\map f 0}$ is equal to $\set {\map f 0}$.
{{Explain|Need to prove that $H$ is continuous to use definition of null-homotopy}}
By definition of null-homotopy, $H$ is a null-homotopy between $f$ and $c_{\map f 0}$.
Let $\sim$ be the equivalence relation on $\closedint 0 1$ defined by:
{{begin-eqn}}
{{eqn | o = \iff
      | q = \forall s_1 \in \openint 0 1 , s_2 \in \closedint 0 1
      | l = s_1 \sim s_2 
      | r = s_2 = s_1
}}
{{eqn | o = \iff
      | q = \forall s_1 \in \set {0, 1} , s_2 \in \closedint 0 1
      | l = s_1 \sim s_2 
      | r = s_2 \in \set {0,1}
}}
{{end-eqn}}
{{Explain|Need to prove that $\sim$ is an equivalence relation}}
From Simple Loop in Hausdorff Space is Homeomorphic to Quotient Space of Interval, it follows that $\Img f$ is homeomorphic to $\closedint 0 1 / \sim$.
{{Explain|Need to prove that the loop is a simple loop to use the result for Simple Loop in Hausdorff Space is Homeomorphic to Quotient Space of Interval}}
Let the homeomorphism between $\closedint 0 1 / \sim$ and $\Img f$ be $h: \closedint 0 1 / \sim \to \Img f$.
Let $h$ be map, defined by:
:$\map h {\eqclass s \sim }  = \map f s$
where $\eqclass s \sim$ denotes the equivalence class defined by $\sim$.
{{explain|Need to check well-definedness of $h$}}
It follows that $h$ is a continuous injective mapping.
{{explain|Need to prove that $h$ is continuous and injective$}}
Define $H_0 : \paren{ \closedint 0 1 / \sim } \times \closedint 0 1 \to D$ for all $s \in \closedint 0 1, t \in \closedint 0 1$ by:
:$\map {H_0} { \eqclass s \sim,t } = \map H {s,t}$
The map $H$ is well-defined, as:
:$\map {H}{0,t} = \map {H}{1,t}$ 
for all $t \in \closedint 0 1$
It follows that:
:$\Img {H_0} = \Img H$
From Composite of Continuous Mappings is Continuous, it follows that $H_0$ is continuous.
As $H$ is a null-homotopy between $f$ and $c_{\map f 0}$, it follows that $H_0$ is a null-homotopy between $h$ and the constant mapping:
:$c_0: \closedint 0 1 / \sim \to \set { \map f 0 }$
From Closed Real Interval is Compact Space, it follows that $\closedint 0 1$ is compact.
From Continuous Image of Compact Space is Compact, it follows that $\Img f$, as well as $\closedint 0 1 / \sim$, are compact.
From Topological Product of Compact Spaces, it follows that:
:$\paren{ \closedint 0 1 / \sim } \times \closedint 0 1$ is compact.
From Continuous Image of Compact Space is Compact, it follows that $\Img {H_0}$ is compact.
From Euclidean Space is Complete Metric Space, it follows that $\closedint 0 1$ is a metric space
From Compact Subspace of Metric Space is Bounded, it follows that $\Img {H_0}$ is bounded.
From the Jordan Curve Theorem, it follows that $\R^2 \setminus \Img f$ is a union of two disjoint connected components.
These components are the interior $\Int f$, which is bounded, and the exterior $\Ext f$, which is unbounded.
By definitions of bounded and unbounded, it follows that there exists some $\mathbf a \in \Ext f \setminus \Img {H_0}$.
Let $\mathbf b \in \R^2 \setminus \Img {H_0}$.
From {Corollary|Borsuk Null-Homotopy Lemma}}, it follows that $\mathbf a$ and $\mathbf b$ lie in the same component of $\R^2 \setminus \Img f$.
That is, $\mathbf b \in \Ext f$.
It follows that if $\mathbf x \in \Int f$, then $\mathbf x \in \Img {H_0}$.
Hence, $\Int f \subseteq \Img H$.
{{qed}}
Category:Jordan Curves
mfkt0qdcx2qjzob8smn96c77wfoydz4