avewright/proofwiki-math huggingface dataset:
Theorem: Number of Multiples less than Given Number

Let $m, n \in \N_{\ge 1}$.
The number of multiples of $m$ not greater than $n$ is given by:
:$q = \floor {\dfrac n m}$
where $\floor {\cdot}$ denotes the floor function

Proof:
By the Division Theorem:
:$(1): \quad n = q m + r$
where $0 \le r < q$.
As $r < q$, it follows that the greatest multiple of $m$ up to $n$ is $q m$.
So all the multiples of $m$ up to $n$ are:
:$m, 2 m, 3 m, \ldots, q m$
Dividing both sides of $(1)$ by $m$:
:$(2): \quad \dfrac n m = q + \dfrac r m$
Taking the floor of $(2)$:
:$\floor {\dfrac n m} = \floor {q + \dfrac r m}$
But as $0 \le \dfrac r m < 1$:
:$\floor {q + \dfrac r m} = q$
Recall that all the multiples of $m$ up to $n$ are $m, 2 m, 3 m, \ldots, q m$.
It follows that the number of multiples of $m$ up to $n$ is:
:$q = \floor {\dfrac n m}$
{{qed}}
Theorem: Restriction of Non-Continuous Mapping on Metric Space to Subspace may be Continuous

Let $M_1 = \struct {A_1, d_1}$ and $M_2 = \struct {A_2, d_2}$ be a metric spaces.
Let $f: A_1 \to A_2$ be a mapping.
Let $Y \subseteq A_1$.
Let $f {\restriction_Y}: Y \to A_2$ be the restriction of $f$ to $Y$.
Let $f {\restriction_Y}$ be $\tuple {d_Y, d_2}$-continuous.
Then it is not necessarily the case that $f$ is also $\tuple {d_1, d_2}$-continuous.

Proof:
Proof by Counterexample:
Let $f: \R \to \R$ be given by:
:<nowiki>$\map f x = \begin {cases}
0 & : x \in \Q \\
1 & : x \in \R \setminus \Q
\end {cases}$</nowiki>
where $\Q$ is the set of rational numbers.
Then $f {\restriction_\Q}: \Q \to \R$ is the constant function $f_0$ with value $0$.
By Constant Mapping is Continuous, $f {\restriction_\Q}$ is continuous at every point.
However, $f$ is not continuous at any point on $\R$.
{{qed}}
Theorem: Supremum Metric on Bounded Real Functions on Closed Interval is Metric

Let $\closedint a b \subseteq \R$ be a closed real interval.
Let $A$ be the set of all bounded real functions $f: \closedint a b \to \R$.
Let $d: A \times A \to \R$ be the supremum metric on $A$.
Then $d$ is a metric.

Proof:
The interval is an instance of a set.
Hence Supremum Metric on Bounded Real-Valued Functions is Metric can be directly applied.
Theorem: Supremum Metric on Continuous Real Functions is Subspace of Bounded

Let $\closedint a b \subseteq \R$ be a closed real interval.
Let $\mathscr C \closedint a b$ be the set of all continuous functions $f: \closedint a b \to \R$.
Let $\map {\mathscr B} {\closedint a b, \R}$ be the set of all bounded real functions $f: \closedint a b \to \R$.
Let $d$ be the supremum metric on $\map {\mathscr B} {\closedint a b, \R}$.
Then $\struct {\mathscr C \closedint a b, d_{\mathscr C} }$ is a subspace of $\struct {\map {\mathscr B} {\closedint a b, \R}, d}$.

Proof:
Let $f \in \mathscr C \closedint a b$.
Then by Image of Closed Real Interval is Bounded, $f$ is bounded on $\closedint a b$.
Thus $f \in \map {\mathscr B} {\closedint a b, \R}$ and the result follows.
{{qed}}
Theorem: Zero Definite Integral of Nowhere Negative Function implies Zero Function

Let $\closedint a b \subseteq \R$ be a closed real interval.
Let $h: \closedint a b \to \R$ be a continuous real function such that:
:$\forall x \in \closedint a b: \map h x \ge 0$
Let:
:$\ds \int_a^b \map h x \rd x = 0$
Then:
:$\forall x \in \closedint a b: \map h x = 0$

Proof:
{{AimForCont}} that:
:$\exists c \in \closedint a b: \map h c > 0$
As $h$ is continuous, there exists some closed real interval $\closedint r s \subseteq \closedint a b$ where $r < s$ such that:
:$\exists \epsilon \in \R_{>0}: \forall x \in \closedint r s: \map h x > \dfrac {\map h c} 2$
From Sign of Function Matches Sign of Definite Integral:
:$\ds \int_r^s \map h x \rd x > 0$
This makes a strictly positive contribution to the integral.
$h$ is still continuous on $\closedint a r$ and $\closedint s b$.
So, again from Sign of Function Matches Sign of Definite Integral:
:$\forall x \in \closedint a r: \map f x \ge 0 \implies \ds \int_a^r \map f x \rd x \ge 0$
:$\forall x \in \closedint s b: \map f x \ge 0 \implies \ds \int_s^b \map f x \rd x \ge 0$
Thus as:
:$\ds \int_a^b \map h x \rd x = \int_a^r \map f x \rd x + \int_r^s \map f x \rd x + \int_s^b \map f x \rd x$
it follows that:
:$\ds \int_a^b \map h x \rd x > 0$
But by hypothesis:
:$\ds \int_a^b \map h x \rd x = 0$
Thus by contradiction, there can be no $c \in \closedint a b$ such that $\map h c > 0$.
Hence the result.
{{qed}}
Theorem: L2 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_2: S \times S \to \R$ be the $L^2$ metric on $\closedint a b$:
:$\ds \forall f, g \in S: \map {d_2} {f, g} := \paren {\int_a^b \paren {\map f t - \map g t}^2 \rd t}^{\frac 1 2}$
Then $d_2$ is a metric.

Proof:
=== Proof of {{Metric-space-axiom|1|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map {d_2} {f, f}
      | r = \paren {\int_a^b \paren {\map f t - \map f t}^2 \rd t}^{\frac 1 2}
      | c = Definition of $d_2$
}}
{{eqn | r = \paren {\int_a^b 0^2 \rd t}^{\frac 1 2}
      | c = {{Defof|Absolute Value}}
}}
{{eqn | r = 0
      | c = Definite Integral of Constant
}}
{{end-eqn}}
So {{Metric-space-axiom|1}} holds for $d_2$.
{{qed|lemma}}
Theorem: Element in Bounded Metric Space has Bound

Let $M = \struct {X, d}$ be a metric space.
Let $M' = \struct {Y, d_Y}$ be a subspace of $M$.
Let $M'$ be bounded in $M$.
Then:
:$\forall a' \in X: \exists K' \in \R: \forall x \in Y: \map d {x, a'} \le K'$
That is, if there is one element of $X$ which satisfies the condition for $Y$ to be bounded in $M$, they ''all'' do.

Proof:
Let $a \in X$ such that $\exists K \in \R: \forall x \in Y: \map d {x, a} \le K$.
Let $a' \in X$.
{{begin-eqn}}
{{eqn | l = \map d {x, a'}
      | o = \le
      | r = \map d {x, a} + \map d {a, a'}
      | c = {{Metric-space-axiom|2}}
}}
{{eqn | o = \le
      | r = K + \map d {a, a'}
      | c = by hypothesis
}}
{{eqn | r = K'
      | c = where $K' = K + \map d {a, a'}$
}}
{{end-eqn}}
{{qed}}
Theorem: Convergence of Square of Linear Combination of Sequences whose Squares Converge

Let $\sequence {x_i}$ and $\sequence {y_i}$ be real sequences such that the series $\ds \sum_{i \mathop \ge 0} {x_i}^2$ and $\ds \sum_{i \mathop \ge 0} {y_i}^2$ are convergent.
Let $\lambda, \mu \in \R$ be real numbers.
Then $\ds \sum_{i \mathop \ge 0} \paren {\lambda x_i + \mu y_i}^2$ is convergent.

Proof:
Let $n \in \N$.
Then:
:$\ds \sum_{i \mathop = 1}^n \paren {\lambda x_i + \mu y_i}^2 = \lambda^2 \sum_{i \mathop = 1}^n {x_i}^2 + \mu^2 \sum_{i \mathop = 1}^n {y_i}^2 + 2 \lambda \mu \sum_{i \mathop = 1}^n x_i y_i$
By Cauchy's Inequality:
:$\ds \sum_{i \mathop = 1}^n x_i y_i \le \paren {\sum_{i \mathop = 1}^n {x_i}^2}^{\frac 1 2} \paren {\sum_{i \mathop = 1}^n {y_i}^2}^{\frac 1 2}$
Hence:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^n \paren {\lambda x_i + \mu y_i}^2
      | o = \le
      | r = \lambda^2 \sum_{i \mathop = 1}^n {x_i}^2 + \mu^2 \sum_{i \mathop = 1}^n {y_i}^2 + 2 \size {\lambda \mu} \sum_{i \mathop = 1}^n x_i y_i
      | c = 
}}
{{eqn | o = \le
      | r = \lambda^2 \sum_{i \mathop = 1}^n {x_i}^2 + \mu^2 \sum_{i \mathop = 1}^n {y_i}^2 + 2 \size {\lambda \mu} \paren {\sum_{i \mathop = 1}^n {x_i}^2}^{\frac 1 2} \paren {\sum_{i \mathop = 1}^n {y_i}^2}^{\frac 1 2}
}}
{{eqn | r = \paren {\size \lambda \paren {\sum_{i \mathop = 1}^n {x_i}^2}^{\frac 1 2} + \size \mu \paren {\sum_{i \mathop = 1}^n {y_i}^2}^{\frac 1 2} }^2
      | c = 
}}
{{eqn | o = \le
      | r = \paren {\size \lambda \paren {\sum_{i \mathop \ge 0} {x_i}^2}^{\frac 1 2} + \size \mu \paren {\sum_{i \mathop \ge 0} {y_i}^2}^{\frac 1 2} }^2
      | c = 
}}
{{end-eqn}}
Thus the sequence of partial sums $\ds \sum_{i \mathop = 1}^n \paren {\lambda x_i + \mu y_i}^2$ is bounded above.
We also have that $\ds \sum_{i \mathop = 1}^n \paren {\lambda x_i + \mu y_i}^2$ is also increasing.
So by the Monotone Convergence Theorem, $\ds \sum_{i \mathop = 1}^n \paren {\lambda x_i + \mu y_i}^2$ is convergent.
{{qed}}
Theorem: Hilbert Sequence Space is Metric Space

Let $A$ be the set of all real sequences $\sequence {x_i}$ such that the series $\ds \sum_{i \mathop \ge 0} {x_i}^2$ is convergent.
Let $\ell^2 = \struct {A, d_2}$ be the Hilbert sequence space on $\R$.
Then $\ell^2$ is a metric space.

Proof:
$\ell^2$ is a particular instance of the general $p$-sequence space $\ell^p$.
Hence $p$-Sequence Space of Real Sequences is Metric Space can be applied directly.
{{qed}}
Theorem: Hilbert Sequence Space is Metric Space

Let $A$ be the set of all real sequences $\sequence {x_i}$ such that the series $\ds \sum_{i \mathop \ge 0} {x_i}^2$ is convergent.
Let $\ell^2 = \struct {A, d_2}$ be the Hilbert sequence space on $\R$.
Then $\ell^2$ is a metric space.

Proof:
By definition of the Hilbert sequence space on $\R$:
Let $A$ be the set of all real sequences $\sequence {x_i}$ such that the series $\ds \sum_{i \mathop \ge 0} {x_i}^2$ is convergent.
Then $\ell^2 := \struct {A, d_2}$ where $d_2: A \times A: \to \R$ is the real-valued function defined as:
:$\ds \forall x = \sequence {x_i}, y = \sequence {y_i} \in A: \map {d_2} {x, y} := \paren {\sum_{k \mathop \ge 0} \paren {x_k - y_k}^2}^{\frac 1 2}$
From Convergence of Square of Linear Combination of Sequences whose Squares Converge we have that $\ds \sum_{k \mathop \ge 0} \paren {x_k - y_k}^2$ does actually converge.
=== Proof of {{Metric-space-axiom|1|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map {d_2} {x, x}
      | r = \paren {\sum_{k \mathop \ge 0} \paren {x_k - x_k}^2}^{\frac 1 2}
      | c = Definition of $d_2$
}}
{{eqn | r = \paren {\sum_{k \mathop \ge 0} 0^2}^{\frac 1 2}
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
So {{Metric-space-axiom|1}} holds for $d_2$.
{{qed|lemma}}
=== Proof of {{Metric-space-axiom|2|nolink}} ===
Let $z = \sequence {z_i} \in A$.
{{MissingLinks|Minkowski's inequality currently only applies to finite sums}}
{{begin-eqn}}
{{eqn | l = \map {d_2} {x, y} + \map {d_2} {y, z}
      | r = \paren {\sum_{k \mathop \ge 0} \paren {x_k - y_k}^2}^{\frac 1 2} + \paren {\sum_{k \mathop \ge 0} \paren {y_k - z_k}^2}^{\frac 1 2}
      | c = Definition of $d_2$
}}
{{eqn | o = \ge
      | r = \paren {\sum_{k \mathop \ge 0} \paren {x_k - z_k}^2}^{\frac 1 2}
      | c = Minkowski's Inequality for Sums: index $2$
}}
{{eqn | r = \map {d_2} {x, z}
      | c = Definition of $d_2$
}}
{{end-eqn}}
So {{Metric-space-axiom|2}} holds for $d_2$.
{{qed|lemma}}
=== Proof of {{Metric-space-axiom|3|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map {d_2} {x, y}
      | r = \paren {\sum_{k \mathop \ge 0} \paren {x_k - y_k}^2}^{\frac 1 2}
      | c = Definition of $d_2$
}}
{{eqn | r = \paren {\sum_{k \mathop \ge 0} \paren {y_k - x_k}^2}^{\frac 1 2}
      | c = {{Defof|Absolute Value}}
}}
{{eqn | r = \map {d_2} {y, x}
      | c = Definition of $d_2$
}}
{{end-eqn}}
So {{Metric-space-axiom|3}} holds for $d_2$.
{{qed|lemma}}
=== Proof of {{Metric-space-axiom|4|nolink}} ===
{{begin-eqn}}
{{eqn | l = x
      | o = \ne
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists k \in \N
      | l = x_k
      | o = \ne
      | r = y_k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x_k - y_k}^2
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {\sum_{k \mathop \ge 0} \paren {x_k - y_k}^2}^{\frac 1 2}
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {d_2} {x, y}
      | o = >
      | r = 0
      | c = Definition of $d_2$
}}
{{end-eqn}}
So {{Metric-space-axiom|4}} holds for $d_2$.
{{qed}}
Theorem: Supremum Metric on Bounded Real-Valued Functions is Metric

Let $X$ be a set.
Let $A$ be the set of all bounded real-valued functions $f: X \to \R$.
Let $d: A \times A \to \R$ be the supremum metric on $A$.
Then $d$ is a metric.

Proof:
We have that the supremum metric on $A \times A$ is defined as:
:$\ds \forall f, g \in A: \map d {f, g} := \sup_{x \mathop \in X} \size {\map f x - \map g x}$
where $f$ and $g$ are bounded real-valued functions.
From Real Number Line is Metric Space, the real numbers $\R$ together with the absolute value function form a metric space.
The result follows by Supremum Metric is Metric.
{{qed}}
Theorem: Supremum Metric on Bounded Real Sequences is Metric

Let $A$ be the set of all bounded real sequences.
Let $d: A \times A \to \R$ be the supremum metric on $A$.
Then $d$ is a metric.

Proof:
By definition, a real sequence is a mapping from the natural numbers $\N$ to the real numbers $\R$.
Thus a bounded real sequence is a bounded real-valued function.
The result follows from Supremum Metric on Bounded Real-Valued Functions is Metric.
{{qed}}
Theorem: Supremum Metric is Metric

Let $S$ be a set.
Let $M = \struct {A', d'}$ be a metric space.
Let $A$ be the set of all bounded mappings $f: S \to M$.
Let $d: A \times A \to \R$ be the supremum metric on $A$.
Then $d$ is a metric.

Proof:
We have that the supremum metric on $A \times A$ is defined as:
:$\ds \forall f, g \in A: \map d {f, g} := \sup_{x \mathop \in S} \map {d'} {\map f x, \map g x}$
where $f$ and $g$ are bounded mappings.
First note that we have:
{{begin-eqn}}
{{eqn | l = \size {\map f x - \map g x}
      | r = \size {\map f x + \paren {-\map g x} }
      | c = 
}}
{{eqn | o = \le
      | r = \size {\map f x} + \size {\paren {-\map g x} }
      | c = Triangle Inequality for Real Numbers
}}
{{eqn | r = \size {\map f x} + \size {\map g x}
      | c = {{Defof|Absolute Value}}
}}
{{eqn | o = \le
      | r = K + L
      | c = 
}}
{{end-eqn}}
and so the {{RHS}} exists.
Theorem: Supremum Metric on Bounded Continuous Mappings is Metric

Let $M_1 = \struct {A_1, d_1}$ and $M_2 = \struct {A_2, d_2}$ be metric spaces.
Let $A$ be the set of all continuous mappings $f: M_1 \to M_2$ which are also bounded.
Let $d: A \times A \to \R$ be the supremum metric on $A$.
Then $d$ is a metric.

Proof:
The set $A$ is a subset of the set $A'$ of all bounded mappings $f: M_1 \to M_2$.
Let $d': A' \times A' \to \R$ be the supremum metric on $A'$.
From Supremum Metric is Metric, $\struct {A', d'}$ is a metric space. 
By definition, $A$ is a metric subspace of $A'$.
Hence the result.
{{qed}}
Theorem: Harmonic Number is not Integer

Let $H_n$ be the $n$th harmonic number.
Then $H_n$ is not an integer for $n \ge 2$.
That is, the only harmonic numbers that are integers are $H_0$ and $H_1$.

Proof:
{{AimForCont}}:
:$(\text P): \quad \exists m \in \N: H_m \in \Z$
By the definition of the harmonic numbers:
:$1 + \dfrac 1 2 + \dfrac 1 3 + \cdots +\dfrac 1 m = H_m$
$m$ is either prime or composite.
If $m$ is prime, we have that:
{{begin-eqn}}
{{eqn | l = 1 + \frac 1 2 + \frac 1 3 + \dots + \frac 1 m
      | r = H_m
}}
{{eqn | l = m! + \frac {m!} 2 + \frac {m!} 3 + \cdots + \paren {m - 1}!
      | r = m!\cdot H_m
      | c = multiplying by $m!$
}}
{{end-eqn}}
If $k \le n$, then $k$ divides $n!$, so all terms are integers.
Every term on the {{LHS}} is divisible by $m$ except for one, namely $\paren {m - 1}!$.
Hence, the {{LHS}} is not divisible by $m$.
But the {{RHS}} is divisible by $m$, so this is a contradiction.
If $m$ is composite, let $p$ be the largest prime which is less than $m$.
Then we have:
{{begin-eqn}}
{{eqn | l = 1 + \frac 1 2 + \frac 1 3 + \dots + \frac 1 p + \cdots + \frac 1 m
      | r = H_m
}}
{{eqn | l = m! + \frac {m!} 2 + \frac {m!} 3 + \cdots \frac {m!} p + \cdots + \paren {m - 1}!
      | r = m! \cdot H_m
      | c = multiplying by $m!$
}}
{{end-eqn}}
For $k < p$, we have that $m!$ is divisible by $p$ and $k$ is not.
So from Euclid's Lemma, every term $\dfrac {m!} k$ is an integer divisible by $p$.
{{AimForCont}} there exists $k \in \Z$, with $p< k< m$ such that $\dfrac {m!} k$ is not divisible by $p$.
Because $m!$ is divisible by $p$ and $\dfrac{m!} k$ is not, it follows from Euclid's Lemma that $k$ is a multiple of $p$.
Since $k$ is a multiple of $p$ which is greater than $p$:
:$2 p \le k$
Thus:
:$p < 2 p \le k < m$
From Bertrand's Postulate, there exists a prime $q$ such that $p < q < 2 p$.
Hence:
:$p < q <m $
This contradicts the fact that $p$ is the largest prime less than $m$.
Hence, the assumption that there exists $k \in \Z$ with $p < k < m$ such that $\dfrac {m!} k$ is not divisible by $p$ is false.
Therefore, every term of the {{LHS}}, except perhaps $\dfrac{m!} p$, is a multiple of $p$.
From above:
:$p < m < 2 p$
so $p$ is the only positive integer less than $m$ which is divisible by $p$.
Since $m!$ is the product of positive integer less than or equal to $m$, it follows that $m!$ is divisible by $p$ only once.
Therefore, $\dfrac {m!} p$ is not divisible by $p$.
Because every term of the {{LHS}} is divisible by $p$ except for one, it follows that the {{LHS}} is not divisible by $p$.
Because the {{RHS}} is a multiple of $m!$, and hence a multiple of $p$, this is a contradiction.
So the assumption that there exists $m \in \N: H_m \in \Z$ is false.
{{qed}}
Theorem: Supremum Metric on Continuous Real Functions is Metric

Let $\closedint a b \subseteq \R$ be a closed real interval.
Let $\mathscr C \closedint a b$ be the set of all continuous functions $f: \closedint a b \to \R$.
Let $d$ be the supremum metric on  $\mathscr C \closedint a b$.
Then $d$ is a metric.

Proof:
Let $\map {\mathscr B} {\closedint a b, \R}$ be the set of all bounded real functions $f: \closedint a b \to \R$.
From Supremum Metric on Continuous Real Functions is Subspace of Bounded, $\struct {\mathscr C \closedint a b, d_{\mathscr C} }$ is a (metric) subspace of $\struct {\map {\mathscr B} {\closedint a b, \R}, d}$.
The result follows from Subspace of Metric Space is Metric Space.
{{qed}}
Theorem: Supremum Metric on Continuous Real Functions is Metric

Let $\closedint a b \subseteq \R$ be a closed real interval.
Let $\mathscr C \closedint a b$ be the set of all continuous functions $f: \closedint a b \to \R$.
Let $d$ be the supremum metric on  $\mathscr C \closedint a b$.
Then $d$ is a metric.

Proof:
Let $A := \mathscr D^r \closedint a b$ be the set of all continuous functions $f: \closedint a b \to \R$ which are of differentiability class $r$.
Let $d_r: A \times A \to \R$ be the supremum metric on $A$, defined as:
:$\ds \forall f, g \in A: \map d {f, g} := \sup_{\substack {x \mathop \in \closedint a b \\ i \mathop \in \set {0, 1, 2, \ldots, r} } } \size {\map {f^{\paren i} } x - \map {g^{\paren i} } x}$
where:
:$f$ and $g$ are continuous functions on $\closedint a b$ which are $r$ times differentiable
:$r \in \N$ is a natural number.
From Supremum Metric on Differentiability Class is Metric, $d_r$ is a metric on $A$.
By definition, real functions which are continuous on $\closedint a b$ are of differentiability class $0$.
Thus setting $r = 0$ it follows that $\mathscr C \closedint a b$ is $\mathscr D^0 \closedint a b$.
The result follows.
{{qed}}
Theorem: Subspace of Metric Space is Metric Space

Let $M = \struct {A, d}$ be a metric space.
Let $H \subseteq A$.
Let $d_H: H \times H \to \R$ be the restriction $d \restriction_{H \times H}$ of $d$ to $H$.
Let $\struct {H, d_H}$ be a metric subspace of $\struct {A, d}$.
Then $d_H$ is a metric on $H$.

Proof:
By definition of restriction:
:$\forall x, y \in H: \map {d_H} {x, y} = \map d {x, y}$
As $d$ is a metric, the metric space axioms are all fulfilled by all $x, y \in A$ under $d$.
As $H \subseteq A$, by definition of subset, all $x, y \in H$ are also elements of $A$.
Therefore the metric space axioms are all fulfilled by all $x, y \in H$ under $d_H$.
{{qed}}
Theorem: Lp 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 $p \in \R_{\ge 1}$.
Let $d_p: S \times S \to \R$ be the $L^p$ metric on $\closedint a b$:
:$\ds \forall f, g \in S: \map {d_p} {f, g} := \paren {\int_a^b \size {\map f t - \map g t}^p \rd t}^{\frac 1 p}$
Then $d_p$ is a metric.

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

Let $A$ be the set of all real sequences $\sequence {x_i}$ such that the series $\ds \sum_{i \mathop \ge 0} x_i^2$ is convergent.
Let $d_p$ be the $p$-sequence metric on $\R$.
Then $\ell^p := \struct {A, d_p}$ is a metric space.

Proof:
By definition of the $p$-sequence metric on $\R$:
Let $A$ be the set of all real sequences $\sequence {x_i}$ such that the series $\ds \sum_{i \mathop \ge 0} x_i^2$ is convergent.
Then $\ell^p := \struct {A, d_2}$ where $d_p: A \times A: \to \R$ is the real-valued function defined as:
:$\ds \forall x = \sequence {x_i}, y = \sequence {y_i} \in A: \map {d_p} {x, y} := \paren {\sum_{k \mathop \ge 0} \size {x_k - y_k}^p}^{\frac 1 p}$
Theorem: Peano Structure is Unique

Let $\struct {P, s, 0}$ and $\struct {P', s', 0'}$ be Peano structures.
Then there is a unique bijection $f: P \to P'$ such that:
{{begin-eqn}}
{{eqn | l = \map f 0
      | r = 0'
}}
{{eqn | q = \forall n \in P
      | l = \map f {\map s n}
      | r = \map {s'} {\map f n}
}}
{{end-eqn}}

Proof:
First to establish uniqueness of $f$.
Suppose that $f, g: P \to P'$ both satisfy the conditions.
Define $A \subseteq P$ as:
:$A := \set {n \in P: \map f n = \map g n}$
Then the first condition implies that $0 \in A$.
Now suppose that $n \in A$. Then:
{{begin-eqn}}
{{eqn| l = \map f {\map s n}
     | r = \map {s'} {\map f n}
     | c = Assumption on $f$
}}
{{eqn| r = \map {s'} {\map g n}
     | c = {{hypothesis}}
}}
{{eqn| r = \map g {\map s n}
     | c = Assumption on $g$
}}
{{end-eqn}}
Hence $\map s n \in A$.
Since $P$ is a Peano structure, it follows that $A = P$.
Hence by Equality of Mappings, $f = g$.
For the existence of such an $f$, we apply the Principle of Recursive Definition with $0' \in P'$ and $s': P' \to P'$.
Lastly, it is to be established that the $f$ so obtained is a bijection.
Let $A' \subseteq P$ be defined as:
:$A' := \set {n \in P: \forall m \in P: \map f n = \map f m \implies n = m}$
It follows from Axiom $(P4)$ that $\map f n = 0'$ implies $n = 0$.
Hence $0 \in A'$.
Suppose now that $n \in A'$, but $\map s n \notin A'$.
Then, since $\map f {\map s n} \ne 0'$, there exists some $m \in P, m \ne n$ such that:
:$\map f {\map s n} = \map f {\map s m}$
That is, such that:
:$\map {s'} {\map f n} = \map {s'} {\map f m}$
But by Axiom $(P3)$, $s'$ is injective.
Hence $\map f n = \map f m$, contradicting the assumption that $n \in A'$.
Therefore $\map s n \in A'$, so that $A' = P$ by Axiom $(P5)$.
That is, $f$ is an injection.
Next, define $A'' \subseteq P'$ as:
:$A'' := \set {n' \in P': \exists n \in P: \map f n = n'}$
Since $\map f 0 = 0'$, we have $0' \in A''$.
Suppose now that $n' \in A''$, and let $\map f n = n'$.
Then:
{{begin-eqn}}
{{eqn|l = \map f {\map s n}
     |r = \map {s'} {\map f n}
     |c = Definition of $f$
}}
{{eqn|r = \map {s'} {n'}
     |c = Definition of $n$
}}
{{end-eqn}}
meaning $\map {s'} {n'} \in A''$.
Hence by Axiom $(P5)$, $A'' = P'$.
That is, $f$ is surjective.
It follows that $f$ is the sought bijection.
{{qed}}
Category:Abstract Algebra
7tp7kcaim0zexvo5cobokzqjwpo89h5
Theorem: P-adic Metric is Metric

Let $p \in \N$ be a prime.
Let $\norm {\,\cdot\,}_p: \Q \to \R_{\ge 0}$ be the $p$-adic norm on $\Q$.
Let $d_p$ be the $p$-adic metric on $\Q$:
:$\forall x, y \in \Q: \map {d_p} {x, y} = \norm{x - y}_p$
Then $d_p$ is a metric.

Proof:
The $p$-adic metric on $\Q$ is defined as the metric induced by the $p$-adic norm on $\Q$.
It follows from Metric Induced by Norm is Metric that $d_p$ is a metric.
{{qed}}
Category:P-adic Metrics
rtedwfl78zmjc7ub1o34icmintipy67