avewright/proofwiki-math huggingface dataset:
Theorem: Intersection of Image with Subset of Codomain

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Let $A \subseteq S$ and $B \subseteq T$.
Then:
:$f \sqbrk {A \cap f^{-1} \sqbrk B} = f \sqbrk A \cap B$

Proof:
{{begin-eqn}}
{{eqn | l = f \sqbrk {A \cap f^{-1} \sqbrk B}
      | r = \set {\map f x: x \in A \cap f^{-1} \sqbrk B}
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{eqn | r = \set {\map f x: x \in A \land x \in f^{-1} \sqbrk B}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | r = \set {\map f x: x \in A \land \map f x \in B}
      | c = {{Defof|Preimage of Subset under Mapping}}
}}
{{eqn | r = \set {\map f x: x \in A} \cap \set {\map f x: \map f x \in B}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | r = f \sqbrk A \cap B
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{end-eqn}}
{{qed}}
Theorem: Projection is Injection iff Factor is Singleton

Let $S_1, S_2, \ldots, S_n$ be non-empty sets.
Let $\ds S = \prod_{i \mathop = 1}^n S_i$ be the cartesian product of $S_1, S_2, \ldots, S_n$.
Let $\pr_j: S \to S_j$ be the $j$th projection on $S$.
Then $\pr_j$ is an injection {{iff}} $S_k$ is a singleton for all $k \in \set {1, 2, \dotsc, n}$ where $k \ne j$.

Proof:
=== Sufficient Condition ===
Suppose $S_k = \set {s_k}$ for all $k \in \set {1, 2, \dotsc, n}$ where $k \ne j$.
Let $\map {\pr_j} x = \map {\pr_j} y = z$ for $x, y \in S$.
Then by definition of $j$th projection, $x, y \in S$ are given by:
:$x = \tuple {s_1, s_2, \dotsc, s_{j - 1}, z, s_{j + 1}, \dotsc, s_n}$
:$y = \tuple {s_1, s_2, \dotsc, s_{j - 1}, z, s_{j + 1}, \dotsc, s_n}$
and so $x = y$.
Thus $\pr_j$ is an injection by definition.
{{qed|lemma}}
Theorem: Preimage of Element under Projection

Let $A$ and $B$ be sets.
Let $A \times B$ be the cartesian product of $A$ and $B$.
Let $\pr_1: A \times B \to A$ be the first projection of $A \times B$.
Let $a \in A$.
Then:
:$\pr_1^{-1} \sqbrk {\set a} = \set {\tuple {a, b}: b \in B}$
that is:
:$\pr_1^{-1} \sqbrk {\set a} = \set a \times B$

Proof:
Directly apparent from the definition of cartesian product.
{{qed}}
Theorem: Divisors of Factorial

Let $n \in \N_{>0}$.
Then all natural numbers less than or equal to $n$ are divisors of $n!$:
:$\forall k \in \left\{{1, 2, \ldots, n}\right\}: n! \equiv 0 \pmod k$

Proof:
From the definition of factorial:
:$n! = 1 \times 2 \times \cdots \times \left({n-1}\right) \times n$
Thus every number less than $n$ appears as a divisor of $n!$.
The result follows from definition of congruence.
{{qed}}
Category:Factorials
Category:Divisors
3p1tjojrrsp4gejtpfuz94uxurucs8o
Theorem: Positive Difference Relation on Reals is Transitive

Let $P \subseteq \R$ be a subset of the real numbers such that:
{{begin-itemize}}
{{item|(1):|$1 \in P$}}
{{item|(2):|$a, b \in P \implies a + b \in P$}}
{{item|(3):|For all $x \in \R$, exactly one of these is true:
{{begin-itemize}}
{{item||$x \in P$}}
{{item||$x {{=}} 0$}}
{{item||$-x \in P$}}
{{end-itemize}} }}
{{end-itemize}}
Let $Q \subseteq \R \times \R$ be the relation on $\R$ defined as:
:$Q = \set {\tuple {a, b} \in \R:  a - b \in P}$
Then $Q$ is a transitive relation.

Proof:
Let $a - b \in P$ and $b - c \in P$.
By condition $(2)$:
:$\paren {a - b} + \paren {b - c} \in P$
Simplifying:
:$a - c \in P$
The result follows by definition of transitive relation.
{{qed}}
Theorem: Repeated Composition of Injection is Injection

Let $S$ be a set.
Let $f: S \to S$ be an injection.
Let the sequence of mappings:
:$f^0, f^1, f^2, \ldots, f^n, \ldots$
be defined as:
:<nowiki>$\forall n \in \N: \map {f^n} x = \begin {cases}
x & : n = 0 \\
\map f x & : n = 1 \\
\map f {\map {f^{n - 1} } x} & : n > 1
\end{cases}$</nowiki>
Then for all $n \in \N$, $f^n$ is an injection.

Proof:
Proof by induction:
For all $n \in \N_{\ge 0}$, let $\map P n$ be the proposition:
:$f^n$ is an injection.
$\map P 0$ is true, as this is the case Identity Mapping is Injection.
$\map P 1$ is true, as this is the assertion that $f$ is an injection.
Theorem: Images of Elements under Repeated Composition of Injection form Equivalence Classes

Let $S$ be a set.
Let $f: S \to S$ be an injection.
Let the sequence of mappings:
:$f^0, f^1, f^2, \ldots, f^n, \ldots$
be defined as:
:$\forall n \in \N: \map {f^n} x = \begin {cases}
x & : n = 0 \\
\map f x & : n = 1 \\
\map f {\map {f^{n - 1} } x} & : n > 1
\end {cases}$
Let $\RR \subseteq S \times S$ be the relation on $S$ defined as:
:$\RR = \set {\tuple {a, b} \in S \times S: \exists k \in \Z: b = \map {f^k} a \lor \exists j \in \Z: a = \map {f^j} b}$
Then $\RR$ is an equivalence relation.

Proof:
Checking in turn each of the criteria for equivalence:
Theorem: Composition of Repeated Compositions of Injections

Let $S$ be a set.
Let $f: S \to S$ be an injection.
Let the sequence of mappings:
:$f^0, f^1, f^2, \ldots, f^n, \ldots$
be defined as:
:$\forall n \in \N: f^n \left({x}\right) = \begin{cases}
x & : n = 0 \\
f \left({x}\right) & : n = 1 \\
f \left({f^{n-1} \left({x}\right)}\right) & : n > 1
\end{cases}$
Then:
:$\forall m, n \in \Z_{\ge 0}: f^n \circ f^m = f^{m + n}$
where $f^n \circ f^m$ denotes composition of mappings.

Proof:
Proof by induction:
Let $m \in \Z_{\ge 0}$ be given.
For all $n \in \Z_{\ge 0}$, let $P \left({n}\right)$ be the proposition:
:$f^n \circ f^m = f^{m + n}$
$P \left({0}\right)$ is true, as this is the case:
{{begin-eqn}}
{{eqn | l = f^0 \circ f^m
      | r = I_S \circ f^m
      | c = where $I_S$ is the identity mapping
}}
{{eqn | r = f^m
      | c = Identity Mapping is Left Identity
}}
{{end-eqn}}
Theorem: Derivative Function on Set of Functions induces Equivalence Relation

Let $X$ be the set of real functions $f: \R \to \R$ which possess continuous derivatives.
Let $\RR \subseteq X \times X$ be the relation on $X$ defined as:
:$\RR = \set {\tuple {f, g} \in X \times X: D f = D g}$
where $D f$ denotes the first derivative of $f$.
Then $\RR$ is an equivalence relation.

Proof:
Checking in turn each of the criteria for equivalence:
Theorem: Factorial Divides Product of Successive Numbers

Let $m, n \in \N_{\ge 1}$ be natural numbers
Let $m^{\overline n}$ be $m$ to the power of $n$ rising.
Then:
:$m^{\overline n} \equiv 0 \bmod n!$
That is, the factorial of $n$ divides the product of $n$ successive numbers.

Proof:
{{questionable|This is not enough. It might superficially be that e.g. the factors of $2$ and $6$ coincide. Effectively this argument reduces to the theorem; it's almost circular}}
Let $m \in \N_{\ge 1}$.
Consider the set:
:$S = \set{m, m + 1, m + 2, \ldots, m + n - 1}$
Note $S$ has $n$ elements.
By Set of Successive Numbers contains Unique Multiple:
:$\set m$ contains a factor of $1$
:$\set {m, m + 1}$ contains a factor of $2$
and in general:
:$\set {m, m + 1, \ldots, m + j - 1}$ contains a factor of $j$.
It follows that $S$ contains factors of $1, 2, 3, \ldots, n$.
Multiplying all elements of $S$ gives:
{{begin-eqn}}
{{eqn | l = m \paren {m + 1} \dotsm \paren {m + n - 1}
      | r = k_1 2 k_2 3 k_3 \dotsm \paren {n - 1} k_{n - 1} n k_n
      | c = for some $k_1, k_2, \ldots, k_n \in N$
}}
{{eqn | r = \paren {k_1 k_2 \dotsm k_{n - 1} k_n} \paren {1 \times 2 \times \dotsm \times \paren {n - 1} \times n}
}}
{{eqn | ll= \leadsto
      | l = m^{\overline n}
      | r = K n!
      | c = for some $K \in \N$
}}
{{eqn | ll= \leadsto
      | l = m^{\overline n}
      | o = \equiv
      | r = 0 \bmod n!
}}
{{end-eqn}}
{{qed}}
Category:Number Theory
Category:Factorials
6zif3tkz964uvv9aufcznrwio2mdac8
Theorem: Binomial Coefficient is Integer

Let $\dbinom n k$ be a binomial coefficient.
Then $\dbinom n k$ is an integer.

Proof:
If it is not the case that $0 \le k \le n$, then the result holds trivially.
So let $0 \le k \le n$.
By the definition of binomial coefficients:
{{begin-eqn}}
{{eqn | l = \binom n k
      | r = \frac {n!} {k! \paren {n - k}!}
}}
{{eqn | r = \frac {n \paren {n - 1} \paren {n - 2} \cdots \paren {n - k + 1} } {k!}
}}
{{end-eqn}}
The numerator is a product of $k$ successive integers.
From Factorial Divides Product of Successive Numbers, $k!$ divides it.
{{qed}}
Theorem: Binomial Coefficient is Integer

Let $\dbinom n k$ be a binomial coefficient.
Then $\dbinom n k$ is an integer.

Proof:
The result follows by Pascal's Rule and Integer Addition is Closed.
{{qed}}
Theorem: Equivalence Classes induced by Derivative Function on Set of Functions

Let $X$ be the set of real functions $f: \R \to \R$ which possess continuous derivatives.
Let $\RR \subseteq X \times X$ be the equivalence relation on $X$ defined as:
:$\RR = \set {\tuple {f, g} \in X \times X: D f = D g}$
where $D f$ denotes the first derivative of $f$.
Then the equivalence classes of $\RR$ are defined as:
:$\map {\eqclass f \RR} x = \set {g \in X: \exists c \in \R: \forall x \in \R: \map g x = \map f x + c}$
That is, it consists of the set of all real functions $f \in X$ which differ by a real constant.

Proof:
Follows directly from Derivative Function on Set of Functions induces Equivalence Relation.
{{qed}}
Theorem: Set of Mappings which map to Same Element induces Equivalence Relation

Let $X$ and $Y$ be sets.
Let $E$ be the set of all mappings from $X$ to $Y$.
Let $b \in X$.
Let $\RR \subseteq E \times E$ be the relation on $E$ defined as:
:$\RR := \set {\tuple {f, g} \in \RR: \map f b = \map g b}$
Then $\RR$ is an equivalence relation.

Proof:
Checking in turn each of the criteria for equivalence:
Theorem: Renaming Mapping from Set of Mappings on Single Element

Let $X$ and $Y$ be sets.
Let $E$ be the set of all mappings from $X$ to $Y$.
Let $b \in X$.
Let $\RR \subseteq E \times E$ be the relation on $E$ defined as:
:$\RR := \set {\tuple {f, g} \in \RR: \map f b = \map g b}$
Let $e_b: E / \RR \to Y$ be the renaming mapping induced by $\RR$.
Then $e_b$ is a bijection.

Proof:
This is an instance of Renaming Mapping is Bijection.
{{qed}}
Theorem: Equivalence of Definitions of Inverse Mapping

Let $S$ and $T$ be sets.
{{TFAE|def = Inverse Mapping}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $f^{-1}: T \to S$ be an inverse mapping of $f: S \to T$ by definition 1.
From Mapping is Injection and Surjection iff Inverse is Mapping it follows that $f^{-1}$ is a bijection.
By Composite of Bijection with Inverse is Identity Mapping:
: $f^{-1} \circ f = I_S$
: $f \circ f^{-1} = I_T$
Thus $f^{-1}: T \to S$ is an inverse mapping of $f: S \to T$ by definition 2.
{{qed|lemma}}
Theorem: Inverse Mapping is Bijection

Let $S$ and $T$ be sets.
Let $f: S \to T$ and $g: T \to S$ be inverse mappings of each other.
Then $f$ and $g$ are bijections.

Proof:
From Inverse is Mapping implies Mapping is Injection and Surjection:
:$f$ is both an injection and a surjection.
Again from Inverse is Mapping implies Mapping is Injection and Surjection:
:$g$ is both an injection and a surjection.
The result follows by definition of bijection.
{{qed}}
Theorem: Mapping is Injection and Surjection iff Inverse is Mapping/Proof 2

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Then:
: $f: S \to T$ can be defined as a bijection in the sense that:
::$(1): \quad f$ is an injection
::$(2): \quad f$ is a surjection.
{{iff}}:
:the inverse $f^{-1}$ of $f$ is such that:
::for each $y \in T$, the preimage $\map {f^{-1} } y$ has exactly one element.
:That is, such that $f^{-1} \subseteq T \times S$ is itself a mapping.

Proof:
=== Necessary Condition ===
{{:Inverse of Injective and Surjective Mapping is Mapping/Proof 2}}{{qed|lemma}}
=== Sufficient Condition ===
Let $f^{-1}: T \to S$ be a mapping.
By Inverse Mapping is Bijection, both $f$ and $f^{-1}$ are bijections.
Hence, in particular, $f$ is a bijection.
{{qed}}
Theorem: Mapping is Extension iff Composite with Inclusion

Let $S$ and $T$ be sets.
Let $A \subseteq S$.
Let $f: S \to T$ and $g: A \to T$ be mappings.
Then $f$ is an extension of $g$ {{iff}}:
:$f = g \circ i_A$
where $i_A$ is the inclusion mapping on $A$.
This can be illustrated using a commutative diagram as follows:
::<nowiki>$\begin {xy} \xymatrix@L + 2mu@ + 1em {
 A \ar[r]^*{i_A}
     \ar@{-->}[rd]_*{f = g \circ i_A}
&
 S \ar[d]^*{g}
\\
&
 T
} \end {xy}$</nowiki>

Proof:
=== Necessary Condition ===
Let $f: S \to T$ be an extension of $g: A \to T$.
Then by definition:
{{begin-eqn}}
{{eqn | q = \forall x \in A
      | l = \map f x
      | r = \map g x
      | c = 
}}
{{eqn | r = \map g {\map {i_A} x}
      | c = {{Defof|Inclusion Mapping}}
}}
{{eqn | r = \map {\paren {g \circ i_A} } x
      | c = {{Defof|Composition of Mappings}}
}}
{{end-eqn}}
That is:
:$f = g \circ i_A$
{{qed|lemma}}
Theorem: Cardinality of Set of Restrictions of Mapping

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Let the cardinality of $S$ be $n$.
Let $F$ be the set of restrictions of $f$ to a subset of $S$.
Then there are $2^n$ elements of $F$.

Proof:
Let $A \subseteq S$ be a subset of $S$.
Let $g: A \to T$ be the restriction of $f$ to $A$.
By definition of restriction of mapping:
:$\forall x \in A: \map g x = \map f x$
and hence there is one mapping $g: A \to T$ such that $g$ is a restriction of $f$.
Therefore for each subset of $S$ there exists a unique restriction of $f$ to that subset.
Therefore there are as many restriction of $f$ as there are subsets of $S$.
That is, by definition of power set, the same as the number of elements of the power set of $S$.
From Cardinality of Power Set of Finite Set, that is $2^n$.
{{qed}}
Theorem: Projection is Surjection/Family of Sets

Let $\family {S_\alpha}_{\alpha \mathop \in I}$ be a family of sets.
Let $\ds \prod_{\alpha \mathop \in I} S_\alpha$ be the Cartesian product of $\family {S_\alpha}_{\alpha \mathop \in I}$.
Let each of $S_\alpha$ be non-empty.
For each $\beta \in I$, let $\ds \pr_\beta: \prod_{\alpha \mathop \in I} S_\alpha \to S_\beta$ be the $\beta$th projection on $\ds S = \prod_{\alpha \mathop \in I} S_\alpha$.
Then $\pr_\beta$ is a surjection.

Proof:
Consider the $\beta$th projection.
Let $x_\beta \in S_\beta$.
Let $\map x \beta = x_\beta$
Suppose $\gamma \in I: \gamma \ne \beta$.
As $S_\gamma \ne \O$ it is possible to use the axiom of choice to choose $\map x \gamma \in S_\gamma$.
Then:
:$\ds x \in \prod_{\alpha \mathop \in I} S_\alpha$
and:
:$\map {\pr_\beta} x = \map x \beta$
Hence the result.
{{qed}}
Theorem: Taxicab Metric on Real Vector Space is Metric

The taxicab metric on the real vector space $\R^n$ is a metric.

Proof:
This is an instance of the taxicab metric on the cartesian product of $A_{1'}, A_{2'}, \ldots, A_{n'}$.
This is proved in Taxicab Metric is Metric.
{{qed}}
Theorem: Taxicab Metric on Real Vector Space is Metric

The taxicab metric on the real vector space $\R^n$ is a metric.

Proof:
The taxicab metric on $\R^n$ is:
:$\ds \map {d_1} {x, y} = \sum_{i \mathop = 1}^n \size {x_i - y_i}$
for $x = \tuple {x_1, x_2, \ldots, x_n}, y = \tuple {y_1, y_2, \ldots, y_n} \in \R^n$.
=== Proof of {{Metric-space-axiom|1|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map {d_1} {x, x}
      | r = \sum_{i \mathop = 1}^n \size {x_i - x_i}
      | c = Definition of $d_1$
}}
{{eqn | r = \sum_{i \mathop = 1}^n 0
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
So {{Metric-space-axiom|1}} holds for $d_1$.
{{qed|lemma}}
=== Proof of {{Metric-space-axiom|2|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map {d_1} {x, y} + \map {d_1} {y, z}
      | r = \sum_{i \mathop = 1}^n \size {x_i - y_i} + \sum_{i \mathop = 1}^n \size {y_i - z_i}
      | c = Definition of $d_1$
}}
{{eqn | r = \sum_{i \mathop = 1}^n \paren {\size {x_i - y_i} + \size {y_i - z_i} }
      | c = 
}}
{{eqn | o = \ge
      | r = \sum_{i \mathop = 1}^n \size {x_i - z_i}
      | c = Triangle Inequality for Real Numbers
}}
{{eqn | r = \map {d_1} {x, z}
      | c = Definition of $d_1$
}}
{{end-eqn}}
So {{Metric-space-axiom|2}} holds for $d_1$.
{{qed|lemma}}
=== Proof of {{Metric-space-axiom|3|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map {d_1} {x, y}
      | r = \sum_{i \mathop = 1}^n \size {x_i - y_i}
}}
{{eqn | r = \sum_{i \mathop = 1}^n \size {y_i - x_i}
      | c = 
}}
{{eqn | r = \map {d_1} {y, x}
      | c = Definition of $d_1$
}}
{{end-eqn}}
So {{Metric-space-axiom|3}} holds for $d_1$.
{{qed|lemma}}
=== Proof of {{Metric-space-axiom|4|nolink}} ===
{{begin-eqn}}
{{eqn | l = x
      | o = \ne
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists i \in \set {1, 2, \ldots, n}
      | l = x_i
      | o = \ne
      | r = y_i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \size {x_i - y_i}
      | o = >
      | r = 0
      | c = {{Defof|Absolute Value}}
}}
{{eqn | ll= \leadsto
      | l = \sum_{i \mathop = 1}^n \size {x_i - y_i}
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {d_1} {x, y}
      | o = >
      | r = 0
      | c = Definition of $d_1$
}}
{{end-eqn}}
So {{Metric-space-axiom|4}} holds for $d_1$.
{{qed}}
Theorem: Chebyshev Distance on Real Vector Space is Metric

The Chebyshev distance on $\R^n$:
:$\ds \forall x, y \in \R^n: \map {d_\infty} {x, y}:= \max_{i \mathop = 1}^n {\size {x_i - y_i} }$
is a metric.

Proof:
This is an instance of the Chebyshev distance on the cartesian product of metric spaces $A_1, A_2, \ldots, A_3$.
This is proved in Chebyshev Distance is Metric.
{{qed}}
Theorem: Chebyshev Distance on Real Vector Space is Metric

The Chebyshev distance on $\R^n$:
:$\ds \forall x, y \in \R^n: \map {d_\infty} {x, y}:= \max_{i \mathop = 1}^n {\size {x_i - y_i} }$
is a metric.

Proof:
=== Proof of {{Metric-space-axiom|1|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map {d_\infty} {x, x}
      | r = \max_{i \mathop = 1}^n \size {x_i - x_i}
      | c = Definition of $d_\infty$
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
So {{Metric-space-axiom|1}} holds for $d_\infty$.
{{qed|lemma}}
=== Proof of {{Metric-space-axiom|2|nolink}} ===
Let $k \in \closedint 1 n$ such that:
{{begin-eqn}}
{{eqn | l = \size {x_k - z_k}
      | r = \max_{i \mathop = 1}^n \size {x_i - z_i}
      | c = 
}}
{{eqn | r = \map {d_\infty} {x, z}
      | c = 
}}
{{end-eqn}}
Then by the Triangle Inequality for Real Numbers:
:$\size {x_k - z_k} \le \size {x_k - y_k} + \size {y_k - z_k}$
But by the nature of the $\max$ operation:
:$\ds \size {x_k - y_k} \le \max_{i \mathop = 1}^n \size {x_i - y_i}$
and:
:$\ds \size {y_k - z_k} \le \max_{i \mathop = 1}^n \size {y_i - z_i}$
Thus:
:$\ds \size {x_k - y_k} + \size {y_k - z_k} \le \max_{i \mathop = 1}^n \size {x_i - y_i} + \max_{i \mathop = 1}^n \size {y_i - z_i}$
Hence:
:$\map {d_\infty} {x, z} \le \map {d_\infty} {x, y} + \map {d_\infty} {y, z}$
So {{Metric-space-axiom|2}} holds for $d_\infty$.
{{qed|lemma}}
=== Proof of {{Metric-space-axiom|3|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map {d_\infty} {x, y}
      | r = \max_{i \mathop = 1}^n \size {x_i - y_i}
      | c = Definition of $d_\infty$
}}
{{eqn | r = \max_{i \mathop = 1}^n \size {y_i - x_i}
      | c = {{Defof|Absolute Value}}
}}
{{eqn | r = \map {d_\infty} {y, x}
      | c = Definition of $d_\infty$
}}
{{end-eqn}}
So {{Metric-space-axiom|3}} holds for $d_\infty$.
{{qed|lemma}}
=== Proof of {{Metric-space-axiom|4|nolink}} ===
Let $x = \tuple {x_1, x_2, \ldots, x_n}$ and $y = \tuple {y_1, y_2, \ldots, y_n}$.
{{begin-eqn}}
{{eqn | l = x
      | o = \ne
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists k \in \closedint 1 n
      | l = x_k
      | o = \ne
      | r = y_k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \size {x_k - y_k}
      | o = >
      | r = 0
      | c = {{Defof|Absolute Value}}
}}
{{eqn | ll= \leadsto
      | l = \max_{i \mathop = 1}^n \size {x_i - y_i}
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {d_\infty} {x, y}
      | o = >
      | r = 0
      | c = Definition of $d_\infty$
}}
{{end-eqn}}
So {{Metric-space-axiom|4}} holds for $d_\infty$.
{{qed}}
Theorem: Chebyshev Distance is Metric

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$.
Then $d_\infty$ is a metric.

Proof:
=== Proof of {{Metric-space-axiom|1|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map {d_\infty} {x, x}
      | r = \max_{i \mathop = 1}^n \set {\map {d_i} {x_i, x_i} }
      | c = Definition of $d_\infty$
}}
{{eqn | r = 0
      | c = as $d_i$ fulfills {{Metric-space-axiom|1}}
}}
{{end-eqn}}
So {{Metric-space-axiom|1}} holds for $d_\infty$.
{{qed|lemma}}
Theorem: Positive Multiple of Metric is Metric

Let $M = \struct {A, d}$ be a metric space.
Let $k \in \R_{>0}$ be a (strictly) positive real number.
Let $d_k: A \times A \to \R$ be the function defined as:
:$\forall \tuple {x, y} \in A: \map {d_k} {x, y} = k \cdot \map d {x, y}$
Then $M_k = \struct {A, d_k}$ is a metric space.

Proof:
=== {{Metric-space-axiom|1|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map {d_k} {x, x}
      | r = k \cdot \map d {x, x}
      | c = Definition of $d_k$
}}
{{eqn | r = 0
      | c = as $d$ fulfils {{Metric-space-axiom|1}}
}}
{{end-eqn}}
So {{Metric-space-axiom|1}} holds for $d_k$.
{{qed|lemma}}
Theorem: Set of Successive Numbers contains Unique Multiple

Let $m \in \Z_{\ge 1}$.
Then $\set {m, m + 1, \ldots, m + n - 1}$ contains a unique integer that is a multiple of $n$.
That is, in any set containing $n$ successive integers, $n$ divides exactly one of those integers.

Proof:
Let $S_m = \set {m, m + 1, \ldots, m + n - 1}$ be a set containing $n$ successive integers.
The proof proceeds by induction on $m$, the smallest number in $S_m$.
Theorem: Taxicab Metric is Topologically Equivalent to Chebyshev Distance on Real Vector Space

For $n \in \N$, let $\R^n$ be a real vector space.
Let $d_1$ be the taxicab metric on $\R^n$.
Let $d_\infty$ be the Chebyshev distance on $\R^n$.
Then
:$\forall x, y \in \R^n: \map {d_\infty} {x, y} \le \map {d_1} {x, y} \le n \cdot \map {d_\infty} {x, y}$
It follows that $d_1$ and $d_\infty$ are Lipschitz equivalent.

Proof:
By definition of the Chebyshev distance on $\R^n$, we have:
:$\ds \map {d_\infty} {x, y} = \max_{i \mathop = 1}^n {\size {x_i - y_i} }$
where $x = \tuple {x_1, x_2, \ldots, x_n}$ and $y = \tuple {y_1, y_2, \ldots, y_n}$.
Let $j$ be chosen so that:
:$\ds \size {x_j - y_j} = \max_{i \mathop = 1}^n {\size {x_i - y_i} }$
Then:
{{begin-eqn}}
{{eqn | l = \map {d_\infty} {x, y}
      | r = \size {x_j - y_j}
      | c = {{Defof|Chebyshev Distance on Real Vector Space}}
}}
{{eqn | o = \le
      | r = \sum_{i \mathop = 1}^n \size {x_i - y_i}
}}
{{eqn | r = \map {d_1} {x, y}
}}
{{eqn | o = \le
      | r = n \size {x_j - y_j}
}}
{{eqn | r = n \cdot \map {d_\infty} {x, y}
}}
{{end-eqn}}
{{qed}}
Theorem: L1 Metric on Closed Real Interval is Metric

Let $S$ be the set of all real functions which are continuous on the closed interval $\closedint a b$.
Let $d: S \times S \to \R$ be the $L^1$ metric on $\closedint a b$:
:$\ds \forall f, g \in S: \map d {f, g} := \int_a^b \size {\map f t - \map g t} \rd t$
Then $d$ is a metric.

Proof:
=== {{Metric-space-axiom|1|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map d {f, f}
      | r = \int_a^b \size {\map f t - \map f t} \rd t
      | c = Definition of $d$
}}
{{eqn | r = \int_a^b 0 \rd t
      | c = {{Defof|Absolute Value}}
}}
{{eqn | r = 0
      | c = Definite Integral of Constant
}}
{{end-eqn}}
So {{Metric-space-axiom|1}} holds for $d$.
{{qed|lemma}}
Theorem: Euclidean Metric is Metric

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'}$.
The Euclidean metric on $\AA$ is a metric.

Proof:
The Euclidean metric on $\AA$ is a special case of the $p$-product metric.
The result follows from $p$-Product Metric is Metric.
{{qed}}
Theorem: Euclidean Space is Normed Vector Space

The real Euclidean space $\R^n$ is a normed vector space.

Proof:
Let $\norm {\, \cdot \,}$ denote the Euclidean norm on $\R^n$.
We prove that $\norm {\, \cdot \,}$ is indeed a norm on $\R^n$ by proving it fulfils the norm axioms.