avewright/proofwiki-math huggingface dataset:
Theorem: Negative of Complex Modulus

Let $z \in \C$ be a complex number.
Then:
:$-\cmod z \le \cmod z$
where $\cmod z$ denotes the complex modulus of $z$.
The equality holds {{iff}} $z = 0$.

Proof:
Let $z = x + i y$.
By definition of complex modulus:
:$\cmod z = \sqrt {x^2 + y^2}$
and so:
:$\cmod z \ge 0$
Thus:
:$-\cmod z\le 0$
Hence the result.
{{qed}}
Theorem: Limit of Function by Convergent Sequences/Corollary

Let $\openint a b$ be an open real interval.
Let $f: \openint a b \to \R$ be a real function.
Let $l \in \R$.
Then:
:$(1): \quad \ds \lim_{x \mathop \to a^+} \map f x = l \iff \forall \sequence {x_n} \subseteq \openint a b: \lim_{n \mathop \to \infty} x_n = a \implies \lim_{n \mathop \to \infty} \map f {x_n} = l$
:$(2): \quad \ds \lim_{x \mathop \to b^-} \map f x = l \iff \forall \sequence {x_n} \subseteq \openint a b: \lim_{n \mathop \to \infty} x_n = b \implies \lim_{n \mathop \to \infty} \map f {x_n} = l$
where:
:$\ds \lim_{x \mathop \to a^+} \map f x$ denotes the limit of $f$ from the right
:$\ds \lim_{x \mathop \to b^-} \map f x$ denotes the limit of $f$ from the left.

Proof:
We have that $\struct {\R, d}$ is a metric space, where $d$ is the Euclidean metric on $\R$.
Thus the theorem follows immediately from Limit of Real Function by Convergent Sequences.
{{qed}}
{{ACC|Limit of Real Function by Convergent Sequences}}
Theorem: Infinite Set in Compact Space has Omega-Accumulation Point

Let $\struct {X, \tau}$ be a compact topological space.
Let $A \subseteq X$ be infinite.
Then $A$ has an $\omega$-accumulation point in $X$.

Proof:
{{AimForCont}} $A$ has no $\omega$-accumulation points in $X$.
Then for any $x \in X$, there exists some open set $U_x$ such that $U_x$ only contains a finite number of points in $A$.
The collection of all such open sets $\CC = \set {U_x: x \in X}$ is an open cover for $X$.
Since $X$ is compact, $\CC$ has a finite subcover $\CC'$.
$\CC'$ contains a finite number of sets in $\CC$, and each of those sets contain a finite number of points in $A$.
Therefore $\bigcup \CC'$ contains a finite number of points in $A$.
However by definition of a subcover, $A \subseteq X \subseteq \bigcup \CC'$.
Thus $\bigcup \CC'$ contains all points in $A$, of which there are infinite.
This is a contradiction.
Therefore $A$ must have an $\omega$-accumulation point in $X$.
{{qed}}
Category:Compact Topological Spaces
Category:Omega-Accumulation Points
7nlncat76iugwj8fojjqjc1c1ivrhgt
Theorem: Half-Open Real Interval is not Open Set

Let $\R$ be the real number line considered as an Euclidean space.
Let $\hointr a b \subset \R$ be a half-open interval of $\R$.
Then $\hointr a b$ is not an open set of $\R$.
Similarly, the half-open interval $\hointl a b \subset \R$ is not an open set of $\R$.

Proof:
Let $\epsilon \in \R_{>0}$.
Let $\map {B_\epsilon} a$ be the open $\epsilon$-ball of $a$.
We have that $a - \epsilon < a$ and so $\map {B_\epsilon} a = \openint {a - \epsilon} {a + \epsilon}$ does not lie entirely in $\hointr a b$.
Thus $\hointr a b$ is not a neighborhood $a$.
It follows that $\hointr a b$ is not an open set of $\R$.
the argument also shows, {{mutatis}}, that $\hointl a b \subset \R$ is not an open set of $\R$.
{{qed}}
Theorem: Empty Set is Open in Metric Space

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

Proof:
By definition, an open set $S \subseteq A$ is one where every point inside it is an element of an open ball contained entirely within that set.
That is, there are no points in $S$ which have an open ball some of whose elements are not in $S$.
As there are no elements in $\O$, the result follows vacuously.
{{qed}}
Theorem: Metric Space is Open in Itself

Let $M = \struct {A, d}$ be a metric space.
Then the set $A$ is an open set of $M$.

Proof:
By definition, an open set $S \subseteq A$ is one where every point inside it is an element of an open ball contained entirely within that set.
Let $x \in A$.
An open ball of $x$ in $M$ is by definition a subset of $A$.
Hence the result.
{{qed}}
Theorem: Subset of Standard Discrete Metric Space is Open

Let $M = \struct {A, d}$ be a standard discrete metric space.
Let $S \subseteq A$ be a subset of $A$.
Then $S$ is an open set of $M$.

Proof:
From the definition of standard discrete metric:
:$\forall x, y \in A: \map d {x, y} = \begin {cases} 0 & : x = y \\ 1 & : x \ne y \end {cases}$
Let $\epsilon \in \R_{>0}$ be such that $0 < \epsilon \le 1$.
Let $x \in S$.
Let $\map {B_\epsilon} x$ be the open $\epsilon$-ball of $x$.
Then by definition of $\epsilon$ and $d$:
:$\map {B_\epsilon} x = \set x$
Thus:
:$\forall x \in S: \map {B_\epsilon} x \subseteq S$
Hence the result by definition of open set.
{{qed}}
Theorem: Image of Open Set under Continuous Mapping in Metric Space may not be Open

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 $\tuple {d_1, d_2}$-continuous mapping from $A_1$ to $A_2$.
Let $U \subseteq A_1$ be an open set of $M_1$.
Then it is not necessarily the case that $f \sqbrk U$ is an open set of $M_2$.

Proof:
Consider the constant mapping $f_0: \R^2 \to \R$ defined as:
:$\forall \tuple {x, y} \in \R^2: \map f {x, y} = 0$
Then by Constant Mapping is Continuous $f$ is a continuous mapping.
But consider any open set $U \subseteq A_1$ of $M_1$ such that $U \ne \O$.
Then $f \sqbrk U = \set 0 = \closedint 0 0$ which is a closed interval of $\R$.
The result follows from Closed Real Interval is not Open Set.
{{qed}}
Theorem: Infinite Intersection of Open Sets of Metric Space may not be Open

Let $M = \struct {A, d}$ be a metric space.
Let $\sequence {U_n}_{n \mathop \in \N}$ be an infinite sequence of open sets of $M$.
Then it is not necessarily the case that $\ds \bigcap_{n \mathop \in \N} U_n$ is itself an open set of $M$.

Proof:
Consider the open real interval $\openint {-\dfrac 1 n} {\dfrac 1 n} \subseteq \R$.
From Open Real Interval is Open Set, $\openint {-\dfrac 1 n} {\dfrac 1 n}$  is open in $\R$ for all $n \in \N_{> 0}$.
But:
:$\ds \bigcap_{n \mathop \in \N_{> 0}} \openint {-\dfrac 1 n} {\dfrac 1 n} = \set 0 = \closedint 0 0$
which is a closed interval of $\R$.
The result follows from Closed Real Interval is not Open Set.
{{qed}}
Theorem: Equivalence of Definitions of Adherent Point of Set

Let $T = \struct {S, \tau}$ be a topological space.
Let $H \subseteq S$.
{{TFAE|def = Adherent Point of Set|view = adherent point of $H$}}
=== Definition by Open Neighborhood ===
{{:Definition:Adherent Point of Set/Definition by Open Neighborhood}}
=== Definition by Closure ===
{{:Definition:Adherent Point of Set/Definition by Closure}}
=== Definition by Neighborhood ===
{{:Definition:Adherent Point of Set/Definition by Neighborhood}}

Proof:
=== Definition by Open Neighborhood is equivalent to Definition by Closure ===
This is shown in Condition for Point being in Closure.
{{qed|lemma}}
Theorem: Metric Space is Compact iff Countably Compact

A metric space is compact {{iff}} it is countably compact.

Proof:
Follows directly from:
:Compact Space is Countably Compact
:Countably Compact Metric Space is Compact
{{qed}}
{{ACC|Countably Compact Metric Space is Compact}}
Theorem: Countably Compact Metric Space is Sequentially Compact

Let $M$ be a countably compact metric space.
Then $M$ is sequentially compact.

Proof:
This follows directly from the results:
:Metric Space is First-Countable
:Countably Compact First-Countable Space is Sequentially Compact
{{qed}}
Theorem: Countably Infinite Set in Countably Compact Space has Omega-Accumulation Point

Let $\struct {X, \tau}$ be a countably compact topological space.
Let $A \subseteq X$ be countably infinite.
Then $A$ has an $\omega$-accumulation point in $X$.

Proof:
;Proof by Contradiction
{{AimForCont}} that $A$ does not have an $\omega$-accumulation point in $X$.
Let $\SS \subseteq \powerset A$ be the set of all finite subsets of $A$.
By Set of Finite Subsets of Countable Set is Countable, we have that $\SS$ is countable.
For all (finite) $F \in \SS$, define:
:$U_F = \paren {F \cup \paren {X \setminus A} }^\circ$
where ${}^\circ$ denotes the interior.
By Image of Countable Set under Mapping is Countable, we have that $\CC = \set {U_F: F \in \SS}$ is countable.
By the definition of an $\omega$-accumulation point, it follows that:
:$\forall x \in X: \exists U \in \tau: x \in U: \exists F \in \SS: U \cap A = F$
By Set Difference Union Intersection, we have:
:$U = \paren {U \cap A} \cup \paren {U \setminus A} \subseteq F \cup \paren {X \setminus A}$
By Set Interior is Largest Open Set, it follows that $\CC$ is a countable open cover for $X$.
Hence, by the definition of a countably compact space, there exists a finite subcover $\CC'$ of $\CC$ for $X$.
By the Principle of Finite Choice, there exists an indexed family $\family {G_V}_{V \mathop \in \CC'}$ of elements of $\SS$ such that:
:$\forall V \in \CC': V = U_{G_V} = \paren {G_V \cup \paren {X \setminus A} }^\circ$
Define:
:$\ds B = \bigcup_{V \mathop \in \CC'} G_V \subseteq A$
By Union of Finite Sets is Finite, it follows that $B$ is finite.
We can use the definition of a cover to conclude that:
:$X \subseteq B \cup \paren {X \setminus A}$
By Relative Complement inverts Subsets, it follows that:
:$\paren {X \setminus B} \cap A = \O$
Hence, $A \subseteq B$.
But then by Subset of Finite Set is Finite, it follows that $A$ is finite, a contradiction.
Theorem: First-Countable Space is Sequentially Compact iff Countably Compact

A first-countable topological space is sequentially compact {{iff}} it is countably compact.

Proof:
Follows directly from:
:Sequentially Compact Space is Countably Compact
:Countably Compact First-Countable Space is Sequentially Compact
{{qed}}
{{ACC|Sequentially Compact Space is Countably Compact}}
Theorem: Accumulation Point of Infinite Sequence in First-Countable Space is Subsequential Limit

Let $\struct {X, \tau}$ be a first-countable topological space.
Let $\sequence {x_n}_{n \mathop \in \N}$ be an infinite sequence in $X$.
Let $x$ be an accumulation point of $\sequence {x_n}$.
Then $x$ is a subsequential limit of $\sequence {x_n}$.

Proof:
By the definition of a first-countable space, there exists a countable local basis $\BB$ at $x$.
By Surjection from Natural Numbers iff Countable, there exists a surjection $\phi: \N \to \BB$.
For all $n \in \N$, define the set:
:$\ds U_n = \bigcap_{k \mathop = 0}^n \map \phi k$
By General Intersection Property of Topological Space, it follows that $U_n$ is an open neighborhood of $x$.
{{explain|What is the exact connection with PoRD?}}
Using the Principle of Recursive Definition, we construct a strictly increasing sequence $\sequence {n_k}_{k \mathop \in \N}$ in $\N$.
By the definition of an accumulation point, we can choose $n_0 \in \N$ such that $x_{n_0} \in U_0$.
For all $k \in \N$, let $n_{k + 1} > n_k$ be the (unique) smallest natural number such that $x_{n_{k + 1} } \in U_{k + 1}$.
Such an $n_{k + 1}$ exists by the definition of an accumulation point, and by the well-ordering principle.
We now show that $x$ is a limit of $\sequence {x_{n_k} }$.
Let $U$ be an open neighborhood of $x$.
By the definition of a local basis, there exists an $H \in \BB$ such that $H \subseteq U$.
By the definition of a surjection, there exists a natural number $m$ such that $H = \map \phi m$.
By construction, we have:
:$\forall k \in \N: k > m \implies x_{n_k} \in U_k \subseteq \map \phi m = H$
Hence the result, by the definition of a limit point.
{{qed}}
Category:First-Countable Spaces
Category:Sequences
9hboo7v45z18z9ktjutracrprir75xw
Theorem: Sequentially Compact Metric Space is Totally Bounded

Let $M = \struct {A, d}$ be a metric space.
Let $M$ be sequentially compact.
Then $M$ is totally bounded.

Proof:
We have {{hypothesis}} that $M$ is a sequentially compact space.
So {{afortiori}} every infinite sequence in $M$ has a subsequence which converges to a point in $A$.
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
By definition, $M$ is totally bounded {{iff}} there exists a finite $\epsilon$-net for $M$.
{{AimForCont}} there exists no finite $\epsilon$-net for $M$.
The aim is to construct an infinite sequence $\sequence {x_n} _{n \mathop \in \N}$ in $A$ that has no convergent subsequence.
Suppose that $x_0, x_1, \ldots, x_r \in A$ have been defined such that:
:$\forall m, n \in \set {0, 1, \ldots, r} : m \ne n \implies \map d {x_m, x_n} \ge \epsilon$
That is, any two distinct elements of $\set {x_0, x_1, \ldots, x_r}$ are at least $\epsilon$ apart.
We have {{hypothesis}} that there exists no finite $\epsilon$-net for $M$.
Specifically, $\set {x_0, x_1, \ldots, x_r}$ is therefore not an $\epsilon$-net for $M$.
So, by definition of a $\epsilon$-net:
:$\ds A \nsubseteq \bigcup_{i \mathop = 0}^r \map {B_\epsilon} {x_i}$
where $\map {B_\epsilon} {x_i}$ denotes the open $\epsilon$-ball of $x_i$ in $M$.
Thus there must exist $x_{r + 1} \in A$ such that:
:$\ds x_{r + 1} \notin \bigcup_{i \mathop = 0}^r \map {B_\epsilon} {x_i}$
That is:
:$\exists x_{r + 1} \in A: \forall m, n \in \set {0, 1, \ldots, r, r + 1} : m \ne n \implies \map d {x_m, x_n} \ge \epsilon$
Thus, by induction, the infinite sequence $\sequence {x_n}$ in $A$ has been constructed such that:
:$\forall m, n \in \N: m \ne n \implies \map d {x_m, x_n} \ge \epsilon$
Thus $\sequence {x_n}$ has no Cauchy subsequence.
From Convergent Sequence in Metric Space is Cauchy Sequence, $\sequence {x_n}$ has no convergent subsequence either. 
Thus, by definition, $M$ is not sequentially compact.
But {{hypothesis}} $M$ is sequentially compact.
Hence by Proof by Contradiction there exists a finite $\epsilon$-net for $M$.
Hence {{afortiori}} $M$ is totally bounded.
{{qed}}
Theorem: Separable Metric Space is Second-Countable

Let $M = \struct {A, d}$ be a metric space.
Let $M$ be separable.
Then $M$ is second-countable.

Proof:
{{Recall|Second-Countable Space|second-countable space}}
{{:Definition:Second-Countable Space}}
By the definition of separability, we can choose a subset $S \subseteq A$ that is countable and everywhere dense.
Define:
:$\BB = \set {\map {B_{1/n} } x: x \in S, \, n \in \N_{>0} }$
where $\map {B_\epsilon } x$ denotes the open $\epsilon$-ball of $x$ in $M$.
We have that Cartesian Product of Countable Sets is Countable.
Hence, by Image of Countable Set under Mapping is Countable, it follows that $\BB$ is countable.
Let $\tau$ denote the topology on $A$ induced by the metric $d$.
It suffices to show that $\BB$ is an analytic basis for $\tau$.
From Open Ball of Metric Space is Open Set, we have that $\BB \subseteq \tau$.
We use Equivalence of Definitions of Analytic Basis.
Let $y \in U \in \tau$.
By the definition of an open set, there exists a strictly positive real number $\epsilon$ such that $\map {B_\epsilon} y \subseteq U$.
By the Axiom of Archimedes, there exists a natural number $n > \dfrac 2 \epsilon$.
That is:
:$\dfrac 2 n < \epsilon$
and so:
:$\map {B_{2/n} } y \subseteq \map {B_\epsilon} y$.
From Subset Relation is Transitive, we have $\map {B_{2/n} } y \subseteq U$.
By the definition of everywhere denseness, and by Equivalence of Definitions of Adherent Point of Set, there exists an $x \in S \cap \map {B_{1/n} } y$.
By {{Metric-space-axiom|3}}, it follows that $y \in \map {B_{1/n} } x$.
For all $z \in \map {B_{1/n} } x$, we have:
{{begin-eqn}}
{{eqn | l = \map d {z, y}
      | o = \le
      | r = \map d {z, x} + \map d {x, y}
      | c = {{Metric-space-axiom|2}}
}}
{{eqn | r = \map d {z, x} + \map d {y, x}
      | c = {{Metric-space-axiom|3}}
}}
{{eqn | o = <
      | r = \frac 2 n
}}
{{end-eqn}}
That is:
:$\map {B_{1/n} } x \subseteq \map {B_{2/n} } y$
From Subset Relation is Transitive, we have:
:$y \in \map {B_{1/n} } x \subseteq U$
Hence the result.
{{qed}}
Theorem: Lipschitz Equivalence is Equivalence Relation

Let $A$ be a set.
Let $\DD$ be the set of all metrics on $A$.
Let $\sim$ be the relation on $\DD$ defined as:
:$\forall d_1, d_2 \in \DD: d_1 \sim d_2 \iff d_1$ is Lipschitz equivalent to $d_2$
Then $\sim$ is an equivalence relation.

Proof:
Let $A$ be a set and let $\DD$ be the set of all metrics on $A$.
In the following, let $d_1, d_2, d_3 \subseteq \DD$ be arbitrary.
Checking in turn each of the criteria for equivalence:
Theorem: Local Membership of Equalizer

Let $\mathbf C$ be a metacategory.
Let $e: E \to C$ be the equalizer of $f, g : C \to D$.
Then a variable element $z: Z \to C$ is a local member of $e$ {{iff}} $f \circ z = g \circ z$:
:$z \in_C e \iff f \circ z = g \circ z$

Proof:
Firstly, note that by Equalizer is Monomorphism, local membership of $e$ is defined.
Theorem: Sequentially Compact Metric Space is Separable

A sequentially compact metric space is separable.

Proof:
This follows directly from:
* Sequentially Compact Metric Space is Totally Bounded
* Totally Bounded Metric Space is Separable.
{{qed}}
{{ACC|Totally Bounded Metric Space is Separable}}
Category:Separable Spaces
Category:Metric Spaces
Category:Sequentially Compact Spaces
5ngsevn0ih6kfj87bntzl2pno8t3wip
Theorem: Sequentially Compact Metric Space is Second-Countable

A sequentially compact metric space is second-countable.

Proof:
This follows directly from:
: Sequentially Compact Metric Space is Separable
: Separable Metric Space is Second-Countable.
{{qed}}
{{ACC|Sequentially Compact Metric Space is Separable}}
Category:Second-Countable Spaces
Category:Metric Spaces
Category:Sequentially Compact Spaces
au7mekk5yhl715pl6nvwpjyl5tw6cpe
Theorem: Topological Equivalence is Equivalence Relation

Let $A$ be a set.
Let $\DD$ be the set of all metrics on $A$.
Let $\sim$ be the relation on $\DD$ defined as:
:$\forall d_1, d_2 \in \DD: d_1 \sim d_2 \iff d_1$ is topologically equivalent to $d_2$
Then $\sim$ is an equivalence relation.

Proof:
Let $A$ be a set and let $\DD$ be the set of all metrics on $A$.
In the following, let $d_1, d_2, d_3 \subseteq \DD$ be arbitrary.
Checking in turn each of the criteria for equivalence:
Theorem: Lipschitz Equivalent Metrics are Topologically Equivalent

Let $M_1 = \struct {A, d_1}$ and $M_2 = \struct {A, d_2}$ be metric spaces on the same underlying set $A$.
Let $d_1$ and $d_2$ be Lipschitz equivalent.
Then $d_1$ and $d_2$ are topologically equivalent.

Proof:
Consider the identity mapping:
: $f: A \to A: \forall x \in A: f \left({x}\right) = x$
Then $f: \left({A, d_1}\right) \to \left({A, d_2}\right)$ can be considered as a Lipschitz equivalence.
The result then follows from Lipschitz Equivalent Metric Spaces are Homeomorphic.
{{qed}}
Theorem: Lipschitz Equivalent Metrics are Topologically Equivalent

Let $M_1 = \struct {A, d_1}$ and $M_2 = \struct {A, d_2}$ be metric spaces on the same underlying set $A$.
Let $d_1$ and $d_2$ be Lipschitz equivalent.
Then $d_1$ and $d_2$ are topologically equivalent.

Proof:
By definition of Lipschitz equivalence:
:$\forall x, y \in A: h \map {d_2} {x, y} \le \map {d_1} {x, y} \le k \map {d_2} {x, y}$
for some $h, k \in \R_{>0}$.
Let $x \in A$.
Let $\epsilon \in \R_{>0}$.
Let $\map {B_{h \epsilon} } {x; d_1}$ denote the open $h \epsilon$-ball with respect to $d_1$ of $x \in A$.
Then:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \map {B_{h \epsilon} } {x; d_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {d_1} {x, y}
      | o = <
      | r = h \epsilon
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {d_2} {x, y}
      | o = \le
      | r = \frac {\map {d_1} {x, y} } h
      | c = 
}}
{{eqn | o = <
      | r = \epsilon
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = \map {B_\epsilon} {x; d_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {B_{h \epsilon} } {x; d_1}
      | o = \subseteq
      | r = \map {B_\epsilon} {x; d_2}
      | c = 
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \map {B_{\epsilon / k} } {x; d_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {d_2} {x, y}
      | o = <
      | r = \frac \epsilon k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {d_1} {x, y}
      | o = \le
      | r = k \frac {\map {d_2} {x, y} } h
      | c = 
}}
{{eqn | o = <
      | r = \epsilon
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = \map {B_\epsilon} {x; d_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {B_{\epsilon / k} } {x; d_2}
      | o = \subseteq
      | r = \map {B_\epsilon} {x; d_1}
      | c = 
}}
{{end-eqn}}
Now suppose $U \subseteq A$ is $d_1$-open.
Let $x \in U$.
Then:
:$\exists \epsilon \in \R_{>0}: \map {B_\epsilon} {x; d_1} \subseteq U$
Thus:
:$\map {B_{\epsilon / k} } {x; d_2} \subseteq \map {B_\epsilon} {x; d_1} \subseteq U$
and so $U$ is $d_2$-open.
And {{mutatis}}, if $U \subseteq A$ is $d_2$-open, it follows that $U$ is $d_1$-open.
{{qed}}
Theorem: Lipschitz Equivalent Metrics are Topologically Equivalent

Let $M_1 = \struct {A, d_1}$ and $M_2 = \struct {A, d_2}$ be metric spaces on the same underlying set $A$.
Let $d_1$ and $d_2$ be Lipschitz equivalent.
Then $d_1$ and $d_2$ are topologically equivalent.

Proof:
By definition of Lipschitz equivalence:
$\exists K_1, K_2 \in \R_{>0}$ such that:
:$(1): \quad \forall x, y \in A: \map {d_2} {x, y} \le K_1 \map {d_1} {x, y}$
:$(2): \quad \forall x, y \in A: \map {d_1} {x, y} \le K_2 \map {d_2} {x, y}$
By Identity Mapping between Metrics separated by Scale Factor is Continuous:
:the identity mapping from $M_1$ to $M_2$ is continuous
:the identity mapping from $M_2$ to $M_1$ is continuous.
Hence the result by definition of topological equivalence.
{{qed}}
Theorem: Compact Metric Space is Complete

A compact metric space is complete.

Proof:
Follows directly from:
:Compact Space is Countably Compact
:Countably Compact Metric Space is Sequentially Compact
:Sequentially Compact Metric Space is Complete
{{qed}}
Theorem: Pullback as Equalizer

Let $\mathbf C$ be a metacategory with binary products.
Suppose that the following diagram commutes (possibly except for the square):
$\quad\quad \begin{xy}\xymatrix@+1em{
P
\ar@/^/[rrd]^*+{p_1}
\ar@/_/[ddr]_*+{p_2}
\ar[rd]^*+{e}
\\
&
A \times B
\ar[r]_*+{\pi_1}
\ar[d]^*+{\pi_2}
&
A
\ar[d]^*+{f}
\\
&
B
\ar[r]_*+{g}
&
C
}\end{xy}$
where $A \times B$ is the binary product of $A$ and $B$, and $\pi_1, \pi_2$ are the associated projections.
Then the border of the diagram, i.e.:
$\quad\quad \begin{xy}\xymatrix{
P
\ar[r]^*+{p_1}
\ar[d]_*+{p_2}
&
A
\ar[d]^*+{f}
\\
B
\ar[r]_*+{g}
&
C
}\end{xy}$
is a pullback of $f$ and $g$ {{iff}} $e: P \to A \times B$ is the equalizer of $f \circ \pi_1$ and $g \circ \pi_2$.

Proof:
Compare the pullback UMP:
:::<nowiki>$\begin{xy}\xymatrix{
Q
\ar@/^/[rrd]^*+{q_1}
\ar@/_/[ddr]_*+{q_2}
\ar@{.>}[dr]^*+{u}
\\
&
P
\ar[r]_*+{p_1}
\ar[d]^*+{p_2}
&
A
\ar[d]^*+{f}
\\
&
B
\ar[r]_*+{g}
&
C
}\end{xy}$</nowiki>
with the equalizer UMP:
:::<nowiki>$\begin{xy}\xymatrix{
 P 
  \ar[r]^*{\family{p_1, p_2}}
&
 A\times B
  \ar[r]<2pt>^*{f\pi_1}
  \ar[r]<-2pt>_*{g\pi_2} 
&
 C
\\
 Q
   \ar@{.>}[u]^*{u}
   \ar[ur]<-2pt>_*{\family{q_1, q_2}}
}\end{xy}$</nowiki>
{{proof wanted|Still need to look for a nice formulation}}
Theorem: Minkowski's Inequality for Sums/Index 2

Let $a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_n \ge 0$ be non-negative real numbers.
Then:
:$\ds \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^2}^{1 / 2} \le \paren {\sum_{k \mathop = 1}^n a_k^2}^{1 / 2} + \paren {\sum_{k \mathop = 1}^n b_k^2}^{1 / 2}$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \paren {a_k + b_k}^2
      | r = \sum_{k \mathop = 1}^n \paren {a_k^2 + 2 a_k b_k + b_k^2}
}}
{{eqn | r = \sum_{k \mathop = 1}^n a_k^2 + 2 \sum_{k \mathop = 1}^n a_k b_k + \sum_{k \mathop = 1}^n b_k^2
}}
{{eqn | o = \le
      | r = \sum_{k \mathop = 1}^n a_k^2 + 2 \paren {\sum_{k \mathop = 1}^n a_k^2}^{1 / 2} \paren {\sum_{k \mathop = 1}^n b_k^2}^{1 / 2} + \sum_{k \mathop = 1}^n b_k^2
      | c = Cauchy's Inequality
}}
{{eqn | r = \paren {\paren {\sum_{k \mathop = 1}^n a_k^2}^{1 / 2} + \paren {\sum_{k \mathop = 1}^n b_k^2}^{1 / 2} }^2
}}
{{end-eqn}}
The result follows from Order is Preserved on Positive Reals by Squaring.