avewright/proofwiki-math huggingface dataset:
Theorem: Distance from Point to Subset is Continuous Function

Let $M = \struct {X, d}$ be a metric space.
Let $A \subseteq X$ be a non-empty subset of $X$.
Let $f: X \to \R$ be the function defined as:
:$\forall x \in X: \map f x = \map d {x, A}$
where $\map d {x, A}$ denotes the distance from $x$ to $A$.
Then $f$ is continuous.

Proof:
$\forall x, y \in X, \forall z \in A$, by the definition of the distance from $x$ to $A$, we have:
:$\map d {x, A} \le \map d {x, z} \le \map d {x, y} + \map d {y, z}$
From Triangle Inequality on Distance from Point to Subset:
:$\map d {x, A} \le \map d {x, y} + \map d {y, A}$
and:
:$\map d {y, A} \le \map d {x, y} + \map d {x, A}$
Therefore:
:$\norm {\map d {x, A} - \map d {y, A} } \le \map d {x, y}$
We can conclude that $f$ is continuous.
{{qed}}
Theorem: Neighbourhood of Point Contains Point of Subset iff Distance is Zero

Let $M = \struct {X, d}$ be a metric space.
Let $A \subseteq X$ be a non-empty subset of $X$.
Let $x \in X$.
Then every neighborhood of $x$ contains a point of $A$ {{iff}}:
:$\map d {x, A} = 0$
where $\map d {x, A}$ denotes the distance from $x$ to $A$.

Proof:
=== Sufficient Condition ===
Let $x \in X$.
Let every neighborhood of $x$ contain a point in $A$.
Every open ball $\map {B_\epsilon} x$ centered at $x$ is seen to be a neighborhood of $x$ in $M$.
But then this implies that for every $\epsilon \in \R_{\gt 0}$ there must exists a $y \in A$ such that:
:$\map d {x, y} < \epsilon$
From this it is seen that $\map d {x, A} = 0$.
{{qed|lemma}}
Theorem: Mapping from Cartesian Product under Chebyshev Distance to Real Number Line is Continuous

Let $M = \struct {A, d'}$ be a metric space.
Let $\ds \AA = A \times A$ be the cartesian product of $A$ with itself.
Let $d_\infty: \AA \times \AA \to \R$ be the Chebyshev distance on $\AA$:
:$\ds \map {d_\infty} {x, y} = \max \set {\map {d'} {x_1, y_1}, \map {d'} {x_2, y_2} }$
where $x = \tuple {x_1, x_2}, y = \tuple {y_1, y_2} \in \AA$.
Then the mapping:
:$d': \struct {A \times A, d_\infty} \to \struct {\R, d}$
where $d$ is the usual metric, is continuous.

Proof:
From definition of continuous mapping:
We just need to show that:
:$\forall \tuple {a, b} \in A \times A: \forall \epsilon \in \R_{>0}: \exists \delta \in \R_{>0}: \forall \tuple {x, y} \in A \times A: \map {d_\infty} {\tuple {x, y}, \tuple {a, b}} < \delta \implies \map d {\map {d'} {x, y}, \map {d'} {a, b}} < \epsilon$
Let $\tuple {a, b} \in A \times A$ and $\epsilon \in \R_{>0}$.
Let $\tuple {x, y} \in A \times A$.
Suppose $\map {d_\infty} {\tuple {x, y}, \tuple {a, b}} < \dfrac \epsilon 2$.
Then:
{{begin-eqn}}
{{eqn | l = \map d {\map {d'} {x, y}, \map {d'} {a, b} }
      | r = \size {\map {d'} {x, y} - \map {d'} {a, b} }
      | c = {{Defof|Euclidean Metric on Real Number Line}}
}}
{{eqn | o = \le
      | r = \size {\map {d'} {x, y} - \map {d'} {a, y} } + \size {\map {d'} {a, y} - \map {d'} {a, b} }
      | c = Triangle Inequality
}}
{{eqn | o = \le
      | r = \map {d'} {x, a} + \map {d'} {y, b}
      | c = Reverse Triangle Inequality on $d'$
}}
{{eqn | o = \le
      | r = 2 \max \set {\map {d'} {x, a}, \map {d'} {y, b} }
      | c =
}}
{{eqn | o = \le
      | r = 2 \map {d_\infty} {\tuple {x, y}, \tuple {a, b} }
      | c = {{Defof|Chebyshev Distance}}
}}
{{eqn | o = <
      | r = 2 \cdot \frac \epsilon 2
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
Therefore $d'$ is continuous.
{{qed}}
Theorem: Empty Set is Open and Closed in Metric Space

Let $M = \struct {A, d}$ be a metric space.
Then the empty set $\O$ is both open and closed in $M$.

Proof:
From Empty Set is Open in Metric Space, $\O$ is open in $M$.
From Empty Set is Closed in Metric Space, $\O$ is closed in $M$.
{{qed}}
Theorem: Empty Set is Closed/Metric Space

Let $M = \struct {A, d}$ be a metric space.
Then the empty set $\O$ is closed in $M$.

Proof:
From Metric Space is Open in Itself, $A$ is open in $M$.
But:
:$\O = \relcomp A A$
where $\complement_A$ denotes the set complement relative to $A$.
The result follows by definition of closed set.
{{qed}}
Theorem: Metric Space is Closed in Itself

Let $M = \struct {A, d}$ be a metric space.
Then $A$ is closed in $M$.

Proof:
From Empty Set is Open in Metric Space, $\O$ is open in $M$.
But:
:$A = \relcomp A \O$
where $\complement_A$ denotes the set complement relative to $A$.
The result follows by definition of closed set.
{{qed}}
Theorem: Metric Space is Open and Closed in Itself

Let $M = \struct {A, d}$ be a metric space.
Then $A$ is both open and closed in $M$.

Proof:
From Metric Space is Open in Itself, $A$ is open in $M$.
From Metric Space is Closed in Itself, $A$ is closed in $M$.
{{qed}}
Theorem: Subset of Metric Space contains Limits of Sequences iff Closed

Let $M = \struct {A, d}$ be a metric space.
Let $H \subseteq A$.
Then $H$ is closed in $M$ {{iff}}:
:for each sequence $\sequence {a_n}$ of points of $H$ that converges to a point $a \in A$, it follows that $a \in H$.

Proof:
=== Necessary Condition ===
Let $H$ be closed in $M$.
Suppose that:
:$\ds \lim_{n \mathop \to \infty} a_n = a$
and:
:$\forall n \in \N_{>0}: a_n \in H$
If the set $\set {a_1, a_2, \ldots}$ is infinite then every neighborhood of $a$ contains infinitely many points of $H$.
Thus $a$ is a limit point of $H$.
So by definition of closed set, $a \in H$.
On the other hand, if $\set {a_1, a_2, \ldots}$ is finite, then for some $N \in \N$:
:$n, m > N \implies a_n = a_m$
Since:
:$\ds \lim_{n \mathop \to \infty} a_n = a$
Then:
:$\forall n > N: \map d {a_n, a} = 0$
Thus:
:$a_n = a$
and so:
:$a \in H$
{{qed|lemma}}
Theorem: Subset of Metric Space is Closed iff contains all Zero Distance Points

Let $M = \struct {A, d}$ be a metric space.
Let $H \subseteq A$.
Then $H$ is closed in $M$ {{iff}}:
:$\forall x \in A: \map d {x, H} = 0 \implies x \in H$
where $\map d {x, H}$ denotes the distance between $x$ and $H$.

Proof:
=== Necessary Condition ===
Let $H$ be closed in $M$.
Let $x \in A: \map d {x, H} = 0 \implies x \in H$.
By Existence of Sequence in Subset of Metric Space whose Limit is Infimum there exists a sequence $\sequence {a_n}$ of points of $H$ such that:
:$\ds \lim_{n \mathop \to \infty} \map d {x, a_n} = 0$
So every neighborhood of $x$ contains points of $H$.
If some $a_n \in H$ then $x \in H$.
Otherwise each $a_n$ is different from $x$
Then $x$ is the limit of $\sequence {a_n}$ and hence of $H$.
Thus $x \in H$ by definition of closed set.
{{qed|lemma}}
Theorem: Continuity of Mapping between Metric Spaces by Closed Sets

Let $M_1 = \struct {A_1, d_1}$ and $M_2 = \struct {A_2, d_2}$ be metric spaces.
Let $f: A_1 \to A_2$ be a mapping.
Then $f$ is continuous {{iff}}:
:for every $V \subseteq A_2$ which is closed in $M_2$, $f^{-1} \sqbrk V$ is closed in $M_1$.

Proof:
First the following is established.
Let $W \in A_2$.
We note that:
:$f^{-1} \sqbrk {A_2} = A_1$
Hence, from Preimage of Set Difference under Mapping:
:$f^{-1} \sqbrk {A_2 \setminus W} = A_1 \setminus f^{-1} \sqbrk W$
Theorem: Metric Space defined by Closed Sets

Let $M = \struct {A, d}$ be a metric space.
Then:
{{begin-axiom}}
{{axiom | n = \text C 1
        | lc= $A$ is closed in $M$
}}
{{axiom | n = \text C 2
        | lc= $\O$ is closed in $M$
}}
{{axiom | n = \text C 3
        | lc= The union of a finite number of closed sets of $M$ is a closed set of $M$
}}
{{axiom | n = \text C 4
        | lc= The intersection of arbitrarily many closed sets of $M$ is a closed set of $M$
}}
{{end-axiom}}

Proof:
From Metric Space is Closed in Itself, $\text C 1$ holds.
{{qed|lemma}}
From Empty Set is Closed in Metric Space, $\text C 2$ holds.
{{qed|lemma}}
Let $\ds \bigcup_{i \mathop = 1}^n V_i$ be the union of a finite number of closed sets of $M$.
Then from De Morgan's laws:
:$\ds A \setminus \bigcup_{i \mathop = 1}^n V_i = \bigcap_{i \mathop = 1}^n \paren {A \setminus V_i}$
By definition of closed set, each of the $A \setminus V_i$ is by definition open in $M$.
We have that $\ds \bigcap_{i \mathop = 1}^n \paren {A \setminus V_i}$ is the intersection of a finite number of open sets of $M$.
Therefore, by Finite Intersection of Open Sets of Metric Space is Open, $\ds \bigcap_{i \mathop = 1}^n \paren {A \setminus V_i} = A \setminus \bigcup_{i \mathop = 1}^n V_i$ is likewise open in $M$.
Then by definition of closed set, $\ds \bigcup_{i \mathop = 1}^n V_i$ is closed in $M$.
Thus $\text C 3$ holds.
{{qed|lemma}}
Let $I$ be an indexing set (either finite or infinite).
Let $\ds \bigcap_{i \mathop \in I} V_i$ be the intersection of a indexed family of closed sets of $M$ indexed by $I$.
Then from De Morgan's laws:
:$\ds A \setminus \bigcap_{i \mathop \in I} V_i = \bigcup_{i \mathop \in I} \paren {A \setminus V_i}$
By definition of closed set, each of $A \setminus V_i$ are by definition open in $M$.
We have that $\ds \bigcup_{i \mathop \in I} \paren {A \setminus V_i}$ is the union of a family of open sets of $M$ indexed by $I$.
Therefore, by definition of a topology, $\ds \bigcup_{i \mathop \in I} \paren {A \setminus V_i} = A \setminus \bigcap_{i \mathop \in I} V_i$ is likewise open in $M$.
Then by definition of closed set, $\ds \bigcap_{i \mathop \in I} V_i$ is closed in $M$.
Thus $\text C 4$ holds.
{{qed}}
Theorem: Infinite Union of Closed Sets of Metric Space may not be Closed

Let $M = \struct {A, d}$ be a metric space.
Let $V_1, V_2, V_3, \ldots$ be an infinite set of closed sets of $M$.
Then it is not necessarily the case that $\ds \bigcup_{n \mathop \in \N} V_n$ is itself a closed set of $M$.

Proof:
Consider the closed real interval:
:$\closedint {\dfrac 1 n} 1 \subseteq \R$
From Closed Real Interval is Closed Set, $\closedint {\dfrac 1 n} 1$  is closed in $\R$ for all $n \in \N$.
But:
:$\ds \bigcup_{n \mathop \in \N} \closedint {\dfrac 1 n} 1 = \hointl 0 1$
The result follows from Half-Open Real Interval is neither Open nor Closed.
{{qed}}
Theorem: Open Sets of Cartesian Product of Metric Spaces under Chebyshev Distance

Let $M_1 = \struct {A_1, d_1}, M_2 = \struct {A_2, d_2}, \ldots, M_n = \struct {A_n, d_n}$ be metric spaces.
Let $\ds \AA = \prod_{i \mathop = 1}^n A_i$ be the cartesian product of $A_1, A_2, \ldots, A_n$.
Let $d_\infty: \AA \times \AA \to \R$ be the Chebyshev distance on $\AA$:
:$\ds \map {d_\infty} {x, y} = \max_{i \mathop = 1}^n \set {\map {d_i} {x_i, y_i} }$
where $x = \tuple {x_1, x_2, \ldots, x_n}, y = \tuple {y_1, y_2, \ldots, y_n} \in \AA$.
For $i \in \set {1, 2, \ldots, n}$, let $U_i$ be open in $M_i$.
Then $\ds \prod_{i \mathop = 1}^n U_i$ is open in $M = \struct {\AA, d_\infty}$.

Proof:
A set $U$ is open {{iff}} it is the neighborhood of each of its points.
That is:
:$\forall a \in U: \exists \delta \in \R_{>0}: \map {B_\delta} a \subseteq U$
where $\map {B_\delta} a$ denotes the open $\delta$-ball of $a$.
Let $I = \set {1, 2, \ldots, n}$.
For all $i \in I$, let $U_i$ be open in $M_i$.
Then:
{{begin-eqn}}
{{eqn | q = \forall i \in I
      | l = a_i
      | o = \in
      | r = U_i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {B_\delta} {a_i}
      | o = \subseteq
      | r = U_i
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall x_i \in A
      | l = \map d {x_i, a_i}
      | o = \in
      | r = U_i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_i
      | o = \in
      | r = U_i
      | c = 
}}
{{end-eqn}}
For all $i \in I$, let $\map d {x_i, a_i} < \delta$.
Then:
{{begin-eqn}}
{{eqn | l = \max_{i \mathop \in I} \set {\map d {x_i, a_i} }
      | o = <
      | r = \delta
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \family {x_i}
      | o = \in
      | r = \map {B_\delta} a
      | c = where $a = \family {a_1}$
}}
{{eqn | ll= \leadsto
      | l = x_i
      | o = \in
      | r = U_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall i \in I
      | l = \family {x_i}
      | o = \in
      | r = \prod_{i \mathop \in I} U_i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {B_\delta} a
      | o = \subseteq
      | r = \prod_{i \mathop \in I} U_i
      | c = 
}}
{{end-eqn}}
Hence $\ds \prod_{i \mathop \in I} U_i$ is open in $M$.
{{qed}}
Theorem: Basis for Product of Metric Spaces under Chebyshev Distance

Let $M_1 = \struct {A_1, d_1}, M_2 = \struct {A_2, d_2}, \ldots, M_n = \struct {A_n, d_n}$ be metric spaces.
Let $\ds \AA = \prod_{i \mathop = 1}^n A_i$ be the cartesian product of $A_1, A_2, \ldots, A_n$.
Let $d_\infty: \AA \times \AA \to \R$ be the Chebyshev distance on $\AA$:
:$\ds \map {d_\infty} {x, y} = \max_{i \mathop = 1}^n \set {\map {d_i} {x_i, y_i} }$
where $x = \tuple {x_1, x_2, \ldots, x_n}, y = \tuple {y_1, y_2, \ldots, y_n} \in \AA$.
For $i \in \set {1, 2, \ldots, n}$, let $U_i$ be open in $M_i$.
Then $\set {\ds \prod_{i \mathop = 1}^n U_i}$ is a basis for the open sets of $M = \struct {\AA, d_\infty}$.

Proof:
Let $U$ be an open set of $M$.
Then for all $a \in U$, we have:
:$\map {B_\delta} a \subseteq U$
for some $\delta \in \R_{>0}$.
Then:
:$\ds \bigcup_{i \mathop = 1}^n \map {B_\delta} {a_i} \subseteq U$
and the result follows.
{{qed}}
Theorem: Open Balls form Basis for Open Sets of Metric Space

Let $M = \struct {A, d}$ be a metric space.
Let $\BB$ be the set of all open balls of $M$.
Then $\BB$ is a basis for the open sets of $M$.

Proof:
Let $U$ be an open set of $M$.
Then by definition:
:$\forall y \in U: \exists \epsilon \in \R_{>0}: \map {B_\epsilon} y \subseteq U$
Thus:
:$\ds U = \bigcup_{y \mathop \in U} \map {B_\epsilon} y$
{{qed}}
Theorem: Graph of Continuous Mapping between Metric Spaces is Closed in Chebyshev Product

Let $M_1 = \struct {A_1, d_1}$ and $M_2 = \struct {A_2, d_2}$ be metric spaces.
Let $f: A_1 \to A_2$ be a continuous mapping.
Let $\AA = A_1 \times A_2$ be the cartesian product of $A_1$ and $A_2$.
Let $d_\infty: \AA \times \AA \to \R$ be the Chebyshev distance on $\AA$:
:$\ds \map {d_\infty} {x, y} = \max \set {\map {d_1} {x_1, y_1}, \map {d_2} {x_2, y_2} }$
where $x = \tuple {x_1, x_2}, y = \tuple {y_1, y_2} \in \AA$.
Let $\Gamma_f$ be the graph of $f$.
Then $\Gamma_f$ is a closed set of $\struct {\AA, d_\infty}$.

Proof:
Let $f: A_1 \to A_2$ be continuous.
Then:
:$\forall a \in A_1: \ds \lim_{n \mathop \to \infty} x_n = a \implies \lim_{n \mathop \to \infty} \map f {x_n} = \map f a$
This can be extended to ordered pairs and ordered tuples, because:
:$\ds \lim_{n \mathop \to \infty} x_n = a \iff \exists N \in \N: n > N \implies x_n \in V$
where $V$ is some neighborhood of $a$.
That is:
:$n > N \implies x_n \in \map {B_\delta} a$
for some $N \in \N$ and all $\delta \in \R_{>0}$.
So:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} x_n
      | r = a
      | c = 
}}
{{eqn | lo= \land
      | l = \lim_{n \mathop \to \infty} \map f {x_n}
      | r = \map f a
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall \delta \in \R_{>0}: \exists N \in \N
      | l = n > N
      | o = \implies
      | r = \map {d_1} {x_n, x} < \delta \land \map {d_1} {\map f {x_n} \map f x} < \delta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map d {\tuple {x, \map f x} }, \tuple {x_n, \map f {x_n} }
      | o = <
      | r = \delta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \lim_{n \mathop \to \infty} \tuple {x_n, \map f {x_n} }
      | r = \tuple {x, \map f x}
      | c = 
}}
{{end-eqn}}
That is, each sequence of points $\sequence {a_n, b_n}$ such that:
:$\map f {a_n} = b_n$
converges to a point $\tuple {a, b}$ such that:
:$\map f a = b$
Hence:
:$\ds \lim_{n \mathop \to \infty} \tuple {a_n, b_n} = \tuple {a, \map f a} = \Gamma_f$
That is, $\Gamma_f$ contains all its limit points.
Hence the result by definition of closed set.
{{qed}}
Theorem: Closed Subset of Real Numbers with Lower Bound contains Infimum

Consider the real number line as a metric space under the usual metric.
Let $A \subseteq \R$ such that $A$ is closed in $\R$ and $A \ne \O$.
Let $A$ be bounded below.
Then $A$ contains its infimum.

Proof:
From Infimum of Bounded Below Set of Reals is in Closure:
:$\inf A \in \map \cl A$
From Set is Closed iff Equals Topological Closure:
:$A = \map \cl A$
Therefore $\inf A \in A$.
{{qed}}
Theorem: Set of Isolated Points of Metric Space is Disjoint from Limit Points

Let $M = \struct {A, d}$ be a metric space.
Let $H \subseteq A$ be a subset of $A$.
Let $H'$ be the set of limit points of $H$.
Let $H^i$ be the set of isolated points of $H$.
Then:
:$H' \cap H^i = \O$

Proof:
Let $a \in H_i$.
Then by definition of isolated point:
:$\exists \epsilon \in \R_{>0}: \set {x \in H: \map d {x, a} < \epsilon} = \set a$
But by {{Metric-space-axiom|1}}:
:$\map d {a, a} = 0$
and so:
:$\set {x \in H: 0 < \map d {x, a} < \epsilon} = \O$
So by definition $a$ is not a limit point of $H$.
That is:
:$a \notin H'$
or:
:$a \in \relcomp A {H'}$
It follows from Intersection with Complement is Empty iff Subset that:
:$H' \cap H^i = \O$
{{qed}}
Theorem: Subset of Metric Space is Subset of its Closure

Let $M = \struct {A, d}$ be a metric space.
Let $H \subseteq A$ be a subset of $A$.
Then:
:$H \subseteq H^-$
where $H^-$ denotes the closure of $H$.

Proof:
By definition of closure:
:$H^- = H' \cup H^i$
where:
:$H'$ denotes the set of limit points of $H$
:$H^i$ denotes the set of isolated points of $H$.
Let $a \in H$.
If $a$ is a limit point of $H$ then $a \in H'$.
Suppose $a \notin H'$.
Then by definition of limit point:
:$\neg \forall \epsilon \in \R_{>0}: \set {x \in A: 0 < \map d {x, a} < \epsilon} \ne \O$
That is:
:$\exists \epsilon \in \R_{>0}: \set {x \in A: 0 < \map d {x, a} < \epsilon} = \O$
and so as $\map d {a, a} = 0$:
:$\exists \epsilon \in \R_{>0}: \set {x \in A: \map d {x, a} < \epsilon} = \set a$
Thus, by definition, $a$ is an isolated point of $H$.
So $a \in H'$ or $a \in H^i$.
Hence by definition of set union:
:$a \in H \subseteq H^-$
By definition of subset:
:$H \subseteq H \subseteq H^-$
and hence the result by definition of closure.
{{qed}}
Theorem: Point in Closure of Subset of Metric Space iff Limit of Sequence

Let $M = \struct {A, d}$ be a metric space.
Let $H \subseteq A$ be a subset of $A$.
Let $H^-$ denote the closure of $H$.
Let $a \in A$.
Then $a \in H^-$ {{iff}} there exists a sequence $\sequence {x_n}$ of points of $H$ which converges to the limit $a$.

Proof:
From definition of closure, $H^- = H' \cup H^i$.
Suppose that $a \in H^-$.
If $a \in H^i$, then $a \in H$ and so $\sequence {a, a, \ldots}$ is a sequence in $H$ that converges to $a$.
If $a \in H'$, then by {{Defof|Limit Point (Metric Space)}} there exists a sequence in $H$ that converges to $a$.
{{qed|lemma}}
For the converse, let $\sequence {x_n}$ be a sequence in $H$ that converges to a point $a \in A$.
So let $U$ be an open set that contains $a$.
By the definition of an open set, it follows that there exists an open ball centered at $a$ such that $\map {B_\epsilon} a \subseteq U$.
But then because $\sequence {x_n}$ converges to $a$ there exists $m \in \N_{\gt 0}$ such that:
{{begin-eqn}}
{{eqn | l = \map d {x_m, a}
      | o = <
      | r = \epsilon
}}
{{eqn | ll= \leadsto
      | l = x_m
      | o = \in
      | r = \map {B_\epsilon} a
      | c = {{Defof|Open Ball}}
}}
{{eqn | ll= \leadsto
      | l = H \cap \map {B_\epsilon} a
      | o = \ne
      | r = \O
      | c = by hypothesis $\sequence {x_n}$ is sequence of points of $H$
}}
{{eqn | ll= \leadsto
      | l = H \cap U
      | o = \ne
      | r = \O
      | c = $x_m \in \map {B_\epsilon} a$ and $\map {B_\epsilon} a \subseteq U$ leads to $x_m \in U$
}}
{{end-eqn}}
Because from Set Intersection Preserves Subsets it is seen that $H \cap \map {B_\epsilon} a \subseteq H \cap U$.
It has been shown that every open set that contains $a$ also contains a point in $H$.
So by Condition for Point being in Closure, it is seen that $a \in H^-$.
{{qed}}
Theorem: Closure of Subset of Closed Set of Metric Space is Subset

Let $M = \struct {A, d}$ be a metric space.
Let $F$ be a closed set of $M$.
Let $H \subseteq F$ be a subset of $F$.
Let $H^-$ denote the closure of $H$.
Then $H^- \subseteq F$.

Proof:
From Metric Induces Topology, the topology $\tau$ induced by the metric $d$ is a topology on $M$.
From Metric Closure and Topological Closure of Subset are Equivalent, it is sufficient to show that the topological closure of $H$ is contained in $F$.
From Set is Closed in Metric Space iff Closed in Induced Topological Space:
:$F$ is closed in the topological space $\struct{A, \tau}$ induced by the metric $d$.
We have:
{{begin-eqn}}
{{eqn | l = H
      | o = \subseteq
      | r = F
}}
{{eqn | ll= \leadsto
      | l = H^-
      | o = \subseteq
      | r = F^-
      | c = Topological Closure of Subset is Subset of Topological Closure
}}
{{eqn | r = F
      | c = Set is Closed iff Equals Topological Closure
}}
{{end-eqn}}
{{qed}}
Theorem: Closure of Subset of Closed Set of Metric Space is Subset

Let $M = \struct {A, d}$ be a metric space.
Let $F$ be a closed set of $M$.
Let $H \subseteq F$ be a subset of $F$.
Let $H^-$ denote the closure of $H$.
Then $H^- \subseteq F$.

Proof:
Let $x \in H^-$.
From Point in Closure of Subset of Metric Space iff Limit of Sequence
:there exists a sequence $\sequence {a_n}$ of points of $H$ which converges to the limit $x$.
By assumption:
:$\sequence {a_n}$ is also a sequence of points of $F$
From Subset of Metric Space contains Limits of Sequences iff Closed:
:$x \in F$
Thus it has been shown:
:$H^- \subseteq F$
{{qed}}
Theorem: Closure of Subset of Metric Space is Intersection of Closed Supersets

Let $M = \struct {A, d}$ be a metric space.
Let $H \subseteq A$ be a subset of $A$.
Let $H^-$ denote the closure of $H$.
Then $H^-$ is the intersection of all closed sets of $M$ of which $H$ is a subset.

Proof:
Let $\mathbb K$ be the set of all closed sets $K$ of $M$ such that $H \subseteq K$.
From Closure of Subset of Closed Set of Metric Space is Subset:
:$\forall K \in \mathbb K: H^- \subseteq K$
From Intersection is Largest Subset:
:$\ds H^- \subseteq \bigcap \mathbb K$
{{qed|lemma}}
From Closure of Subset of Metric Space is Closed, $H^-$ is closed.
From Subset of Metric Space is Subset of its Closure, $H \subseteq H^-$.
So $H^-$ is, by definition, a closed set of $M$ which contains $H$.
But $\ds \bigcap \mathbb K$ is the intersection of '''all''' closed sets of $M$ which contain $H$.
So from Intersection is Subset it follows that:
:$\ds \bigcap \mathbb K \subseteq H^-$
{{qed|lemma}}
Finally, we have that:
:$\ds H^- \subseteq \bigcap \mathbb K$
:$\ds \bigcap \mathbb K \subseteq H^-$
So by definition of set equality:
:$\ds H^- = \bigcap \mathbb K$
which is what we needed to prove.
{{qed}}
Theorem: Rational Numbers form Metric Subspace of Real Numbers under Euclidean Metric

Let $\struct {\Q, d_\Q}$ be the set of rational numbers under the function $d_\Q: \Q \times \Q \to \R$ defined as:
:$\forall x, y \in \Q: \map {d_\Q} {x, y} = \size {x - y}$
Let $\struct {\R, d}$ denote the real number line with the usual (Euclidean) metric.
Then $\struct {\Q, d_\Q}$ is a metric subspace of $\struct {\R, d}$.

Proof:
From Rational Numbers form Subfield of Real Numbers:
:$\Q \subseteq \R$
By definition of the Euclidean metric on $\R$:
:$\forall x, y \in \R: \map d {x, y} = \size {x - y}$
and so $d_\Q$ is a restriction of $d$:
:$d_\Q = d {\restriction}_{\Q \times \Q}$
From Euclidean Metric on Real Number Line is Metric, $d$ is a metric on $\R$.
The result follows by definition of metric subspace.
{{qed}}
Theorem: Euclidean Metric on Real Number Line is Metric

The Euclidean metric on the real number line $\R$ is a metric.

Proof:
The Euclidean metric on the real number line is a special case of the Euclidean metric on the real vector space $\R^n$.
The result follows from Euclidean Metric on Real Vector Space is Metric.
{{qed}}