avewright/proofwiki-math huggingface dataset:
Theorem: Banach-Steinhaus Theorem/Normed Vector Space

Let $\struct {X, \norm {\,\cdot\,}_X}$ be a Banach space.
Let $\struct {Y, \norm {\,\cdot\,}_Y}$ be a normed vector space.
Let $\family {T_\alpha: X \to Y}_{\alpha \mathop \in A}$ be an $A$-indexed family of bounded linear transformations from $X$ to $Y$.
Suppose that:
:$\ds \forall x \in X: \sup_{\alpha \mathop \in A} \norm {T_\alpha x}_Y$ is finite.
Then:
:$\ds \sup_{\alpha \mathop \in A} \norm {T_\alpha}$ is finite
where $\norm {T_\alpha}$ denotes the norm of the linear transformation $T_\alpha$.

Proof:
From Banach Space is F-Space, $\struct {X, \norm {\, \cdot \,}_X}$ can be considered as an $F$-Space.
From Normed Vector Space is Hausdorff Topological Vector Space, $\struct {Y, \norm {\, \cdot \,}_Y}$ can be considered as a topological vector space.
Let $\Gamma = \set {T_\alpha : \alpha \in A}$ and:
:$\map \Gamma x = \set {T_\alpha x : \alpha \in A}$
for each $x \in X$. 
By hypothesis, we have:
:$\ds \sup_{\alpha \in A} \norm {T_\alpha x}_Y < \infty$ for each $x \in X$. 
From Characterization of von Neumann-Boundedness in Normed Vector Space, we have that $\map \Gamma x$ is von Neumann-bounded in $\struct {Y, \norm {\, \cdot \,}_Y}$ for each $x \in X$. 
From Banach-Steinhaus Theorem: $F$-Space, $\Gamma$ is equicontinuous. 
So there exists an open neighborhood $U$ of ${\mathbf 0}_X$ such that:
:$T_\alpha \sqbrk U \subseteq \map {B_1^Y} { {\mathbf 0}_Y} \subseteq B^-_Y$ for each $\alpha \in A$.
where:
:$\map {B_1^Y} { {\mathbf 0}_Y}$ is the open ball of center ${\mathbf 0}_Y$ and radius $1$ in $\struct {Y, \norm {\, \cdot \,}_Y}$
:$B_Y^-$ is the closed unit ball of $\struct {Y, \norm {\, \cdot \,}_Y}$.
From the definition of an open set in a normed vector space, there exists $\delta > 0$ such that:
:$\map {B_\delta^X} { {\mathbf 0}_X} \subseteq U$
and so:
:$T_\alpha \sqbrk {\map {B_\epsilon^X} { {\mathbf 0}_X} } \subseteq \map {B_1^Y} { {\mathbf 0}_Y}$ for each $\alpha \in A$.
We then have:
:$\paren {\delta/2} B_X^- \subseteq \map {B_\delta^X} { {\mathbf 0}_X}$
and:
:$\map {B_1^Y} { {\mathbf 0}_Y} \subseteq B_Y^-$
where $B_X^-$ denotes the closed unit ball of $\struct {X, \norm {\, \cdot \,}_X}$. 
Hence by Image of Dilation of Set under Linear Transformation is Dilation of Image, we have: 
:$T_\alpha \sqbrk {B_X^-} \subseteq \paren {2/\delta} B_Y^-$ for each $\alpha \in A$. 
From Norm of Bounded Linear Transformation in terms of Closed Unit Ball, we have:
:$\ds \norm {T_\alpha} \le \frac 2 \delta$ for each $\alpha \in A$.
That is:
:$\ds \sup_{\alpha \in A} \norm {T_\alpha} \le \frac 2 \delta$
as required.
{{qed}}
Theorem: Banach-Steinhaus Theorem/Normed Vector Space

Let $\struct {X, \norm {\,\cdot\,}_X}$ be a Banach space.
Let $\struct {Y, \norm {\,\cdot\,}_Y}$ be a normed vector space.
Let $\family {T_\alpha: X \to Y}_{\alpha \mathop \in A}$ be an $A$-indexed family of bounded linear transformations from $X$ to $Y$.
Suppose that:
:$\ds \forall x \in X: \sup_{\alpha \mathop \in A} \norm {T_\alpha x}_Y$ is finite.
Then:
:$\ds \sup_{\alpha \mathop \in A} \norm {T_\alpha}$ is finite
where $\norm {T_\alpha}$ denotes the norm of the linear transformation $T_\alpha$.

Proof:
It suffices to show that there exist an $x_0 \in X$ and an $r \in \R_{>0}$ such that:
:$\ds K : = \sup_{x \mathop \in \map {B_r} {x_0} } \sup_{\alpha \mathop \in A} \norm {T_\alpha x}_Y$ is finite
where $\map {B_r} {x_0}$ is the open $r$-ball of $x_0$.
Indeed, then we have for all $x \in X \setminus \set 0$:
{{begin-eqn}}
{{eqn | l = \frac{r}{2} \frac {\norm {T_\alpha x}_Y}{\norm x_X}
      | r = \norm {\map {T_\alpha} {x_0 + \frac{r}{2 \norm x_X} x } - T_\alpha x_0 }_Y
}}
{{eqn | o = \le
      | r = \norm {\map {T_\alpha} {\underbrace {x_0 + \frac{r}{2 \norm x_X} x}_{\in \map {B_r} {x_0} } } }_Y + \norm {\T_\alpha \underbrace {x_0}_{\in \map {B_r} {x_0} } }_Y
}}
{{eqn | o = \le
      | r = 2 K
}}
{{end-eqn}}
That is:
:$\ds \norm {T_\alpha} = \sup_{x \mathop \in X \setminus \set 0} \frac {\norm {T_\alpha x}_Y}{\norm x_X} \le \frac {4 K} r$
{{qed|lemma}}
{{AimForCont}} that for all $x_0 \in X$ and $r \in \R_{>0}$:
:$\ds \sup_{x \mathop \in \map {B_r} {x_0} } \sup_{\alpha \mathop \in A} \norm {T_\alpha x}_Y = + \infty$
Then we can choose:
:$\map {B_{r_1} } {x_1} \supseteq \map {B_{r_2} } {x_2} \supseteq \cdots$
and:
:$\alpha_1, \alpha_2, \ldots \in A$
such that:
:$\ds \inf _{x \mathop \in \map {B_{r_k} } {x_k} } \norm {T_{\alpha_k} x}_Y \ge k$
and:
:$0 < r_k < \frac 1 k$
Indeed, let $r_0 \in \R_{>0}$ and $x_0 \in X$ be fixed.
Then, for $k = 1, 2, \ldots$, we have:
:$\exists x_k \in \map {B_{r_{k-1} } } {x_{k-1} } \exists \alpha_k \in A : \norm {T_{\alpha_k} {x_k} }_Y > k$
Furthermore, as $T_{\alpha_k}$ is continuous, $\exists r_k \in \openint 0 {\frac 1 k}$ such that:
:$\map {B_{r_{k-1} } } {x_{k-1} } \supseteq \map {B_{r_k} } {x_k}$
and:
:$\ds \inf _{x \mathop \in \map {B_{r_k} } {x_k} } \norm {T_{\alpha_k} x}_Y \ge k$
{{qed|lemma}}
Then $\sequence {x_k}$ is a Cauchy sequence in $X$, since for each $N \in \N_{>0}$:
:$k, l \ge N \implies \norm {x_k - x_l}_X \le \norm {\underbrace {x_k - x_N}_{\in \map {B_{r_N} } {x_N} } }_X + \norm {\underbrace {x_l - x_N}_{\in \map {B_{r_N} } {x_N} } }_X\le 2 \, r_N \le \frac 2 N$
As $X$ is a Banach space, there exists:
:$\ds z := \lim_{k \mathop \to +\infty} x_k$
Observe that:
:$\ds z \in \bigcap_{k \in \N_{>0} } \map {\overline {B_{r_k} } } {x_k}$
where $\map {\overline  {B_{r_k} } } {x_k}$ is the $r_k$-closed ball of $x_k$.
In particular:
:$\forall k \in \N_{>0} : \norm {T_{\alpha_k} z}_Y \ge k$
Thus:
:$\ds \sup_{\alpha \mathop \in A} \norm {T_\alpha z}_Y = + \infty$
This is a contradiction.
{{qed}}
Theorem: Minkowski's Inequality for Sums/Index Greater than 1

Let $a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_n \in \R_{\ge 0}$ be non-negative real numbers.
Let $p \in \R$ be a real number such that $p > 1$.
Then:
:$\ds \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^p}^{1 / p} \le \paren {\sum_{k \mathop = 1}^n {a_k}^p}^{1 / p} + \paren {\sum_{k \mathop = 1}^n {b_k}^p}^{1 / p}$

Proof:
Define:
:$q = \dfrac p {p - 1}$
Then:
:$\dfrac 1 p + \dfrac 1 q = \dfrac 1 p + \dfrac {p - 1} p = 1$
It follows that:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \paren {a_k + b_k}^p
      | r = \sum_{k \mathop = 1}^n a_k \paren {a_k + b_k}^{p - 1} + \sum_{k \mathop = 1}^n b_k \paren {a_k + b_k}^{p - 1}
      | c = 
}}
{{eqn | o = \le
      | r = \paren {\sum_{k \mathop = 1}^n {a_k}^p}^{1 / p} \paren {\sum_{k \mathop = 1}^n \paren {\paren {a_k + b_k}^{p - 1} }^q}^{1 / q} + \paren {\sum_{k \mathop = 1}^n {b_k}^p}^{1 / p} \paren {\sum_{k \mathop = 1}^n \paren {\paren {a_k + b_k}^{p - 1} }^q}^{1 / q}
      | c = Hölder's Inequality for Sums (twice)
}}
{{eqn | r = \paren {\sum_{k \mathop = 1}^n {a_k}^p}^{1 / p} \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^p}^{1 / q} + \paren {\sum_{k \mathop = 1}^n {b_k}^p}^{1 / p} \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^p}^{1 / q}
      | c = Power of Power, and {{hypothesis}}: $\paren {p - 1} q = p$
}}
{{eqn | r = \paren {\paren {\sum_{k \mathop = 1}^n {a_k}^p}^{1 / p} + \paren {\sum_{k \mathop = 1}^n {b_k}^p}^{1 / p} } \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^p}^{1 / q}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^p}^{1 - 1 / q}
      | o = \le
      | r = \paren {\sum_{k \mathop = 1}^n {a_k}^p}^{1 / p} + \paren {\sum_{k \mathop = 1}^n {b_k}^p}^{1 / p}
      | c = dividing by $\ds \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^p}^{1 / q}$
}}
{{eqn | ll= \leadsto
      | l = \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^p}^{1 / p}
      | o = \le
      | r = \paren {\sum_{k \mathop = 1}^n {a_k}^p}^{1 / p} + \paren {\sum_{k \mathop = 1}^n {b_k}^p}^{1 / p}
      | c = as $1 - \dfrac 1 q = p$
}}
{{end-eqn}}
Theorem: Minkowski's Inequality for Sums/Index Greater than 1

Let $a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_n \in \R_{\ge 0}$ be non-negative real numbers.
Let $p \in \R$ be a real number such that $p > 1$.
Then:
:$\ds \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^p}^{1 / p} \le \paren {\sum_{k \mathop = 1}^n {a_k}^p}^{1 / p} + \paren {\sum_{k \mathop = 1}^n {b_k}^p}^{1 / p}$

Proof:
Let $\mathbf a$ and $\mathbf b$ be real finite sequences:
{{begin-eqn}}
{{eqn | l = \mathbf a
      | r = \sequence {a_k}_{1 \mathop \le k \mathop \le n}
}}
{{eqn | l = \mathbf b
      | r = \sequence {b_k}_{1 \mathop \le k \mathop \le n}
}}
{{end-eqn}}
Let $\norm {\mathbf a}_p$ denote the $p$-norm of $\mathbf a$:
:$\norm {\mathbf a}_p := \paren {\ds \sum_{k \mathop = 1}^n {a_k}^p}^{1 / p}$
Define:
:$q = \dfrac p {p - 1}$
Then:
:$\dfrac 1 p + \dfrac 1 q = \dfrac 1 p + \dfrac {p - 1} p = 1$
Then:
{{begin-eqn}}
{{eqn | l = \paren {\norm {\mathbf a + \mathbf b}_p}^p
      | r = \norm {\paren {\mathbf a + \mathbf b}^p}_1
}}
{{eqn | r = \norm {\mathbf a \paren {\mathbf a + \mathbf b}^{p - 1} + \mathbf b \paren {\mathbf a + \mathbf b}^{p - 1} }_1
}}
{{eqn | r = \norm {\mathbf a \paren {\mathbf a + \mathbf b}^{p - 1} }_1 + \norm {\mathbf b \paren {\mathbf a + \mathbf b}^{p - 1} }_1
}}
{{eqn | o = \le
      | r = \norm {\mathbf a}_p \norm {\paren {\mathbf a + \mathbf b}^{p - 1} }_q + \norm {\mathbf b}_p \norm {\paren {\mathbf a + \mathbf b}^{p - 1} }_q
      | c = Hölder's Inequality for Sums (twice)
}}
{{eqn | r = \paren {\norm {\mathbf a}_p + \norm {\mathbf b}_p} \norm {\paren {\mathbf a + \mathbf b}^{p - 1} }_q
      | c = simplifying
}}
{{eqn | r = \paren {\norm {\mathbf a}_p + \norm {\mathbf b}_p} \norm {\paren {\mathbf a + \mathbf b}^{p - 1} }_{p / \paren {p - 1} }
      | c = {{hypothesis}}: $\dfrac p {p - 1} = q$
}}
{{eqn | r = \paren {\norm {\mathbf a}_p + \norm {\mathbf b}_p} \paren {\norm {\mathbf a + \mathbf b}_p}^{p - 1}
      | c = Transformation of P-Norm
}}
{{eqn | ll= \leadsto
      | l = \norm {\mathbf a + \mathbf b}_p
      | o = \le
      | r = \norm {\mathbf a}_p + \norm {\mathbf b}_p
      | c = dividing both sides by $\paren {\norm {\mathbf a + \mathbf b}_p}^{p - 1}$
}}
{{end-eqn}}
{{qed}}
Theorem: Minkowski's Inequality for Sums/Index Less than 1

Let $a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_n \in \R_{\ge 0}$ be non-negative real numbers.
Let $p \in \R$ be a real number.
If $p < 0$, then we require that $a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_n$ be strictly positive.
If $p < 1$, $p \ne 0$, then:
:$\ds \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^p}^{1/p} \ge \paren {\sum_{k \mathop = 1}^n a_k^p}^{1/p} + \paren {\sum_{k \mathop = 1}^n b_k^p}^{1/p}$

Proof:
In this case, $p$ and $q$ have opposite sign.
The proof then follows the same lines as the proof for $p > 1$, except that the Reverse Hölder's Inequality for Sums is applied instead.
Theorem: Monotone Real Function is Darboux Integrable

Let $\closedint a b$ be a closed real interval, where $a < b$.
Let $f: \closedint a b \to \R$ be a monotone real function.
Then $f$ is Darboux integrable over $\closedint a b$.

Proof:
We consider the case where $f$ is increasing; the case where $f$ is decreasing is handled similarly.
Let $\epsilon \in \R_{>0}$ be a (strictly) positive real number.
By the Axiom of Archimedes, there exists a natural number $n$ such that:
:$n > \dfrac {\paren {b - a} \paren {\map f b - \map f a} } \epsilon$
For $k \in \set {0, 1, 2, \ldots, n}$, define:
:$x_k = a + k \dfrac {b - a} n$
Then:
:$a = x_0 < x_1 < \cdots < x_n = b$
and hence $P = \set {x_0, x_1, \ldots, x_n}$ is a subdivision of $\closedint a b$.
The lower Darboux sum and upper Darboux sum of $f$ belonging to the subdivision $P$ are, respectively:
{{begin-eqn}}
{{eqn | l = \map L P
      | m = \sum_{k \mathop = 1}^n \map f {x_{k - 1} } \paren {x_k - x_{k - 1} }
      | mo= =
      | r = \frac {b - a} n \sum_{k \mathop = 1}^n \map f {x_{k - 1} }
}}
{{eqn | l = \map U P
      | m = \sum_{k \mathop = 1}^n \map f {x_k} \paren {x_k - x_{k - 1} }
      | mo= =
      | r = \frac {b - a} n \sum_{k \mathop = 1}^n \map f {x_k}
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = 0
      | o = \le
      | r = \overline {\int_a^b} \map f x \rd x - \underline {\int_a^b} \map f x \rd x
      | c = Darboux's Theorem
}}
{{eqn | o = \le
      | r = \map U P - \map L P
      | c = 
}}
{{eqn | r = \frac {\paren {b - a} \paren {\map f b - \map f a} } n
      | c = 
}}
{{eqn | o = <
      | r = \epsilon
      | c = 
}}
{{end-eqn}}
Since $\epsilon \in \R_{>0}$ is arbitrary, the result follows.
{{qed}}
Theorem: Topologies are not necessarily Comparable by Coarseness

Let $S$ be a set with at least $2$ elements.
Let $\mathbb T$ be the set of all topologies on $S$.
For two topologies $\tau_a, \tau_b \in \mathbb T$, let $\tau_a \le \tau_b$ denote that $\tau_a$ is coarser than $\tau_b$.
Then there exist $\tau_1, \tau_2 \in \mathbb T$ such that neither:
:$\tau_1 \le \tau_2$
nor:
:$\tau_2 \le \tau_1$
That is, there are always topologies on $S$ which are non-comparable.

Proof:
Let $a, b \in S$.
Let:
:$\tau_a$ be the particular point topology with respect to $a$ on $S$
:$\tau_b$ be the particular point topology with respect to $b$ on $S$
From Homeomorphic Non-Comparable Particular Point Topologies:
:neither $\tau_a \le \tau_b$ nor $\tau_b \le \tau_a$.
Hence the result.
{{qed}}
Theorem: Euclidean Plane is Abstract Geometry

The Euclidean plane $\struct {\R^2, L_E}$ is an abstract geometry.

Proof:
We will show that the axioms for an abstract geometry hold.
Theorem: Pullback of Subset Inclusion

Denote with $\mathbf{Set}$ the category of sets.
Let $A, B$ be sets, and let $f: A \to B$ be a mapping.
Let $V \subseteq B$ be a subset of $B$.
Denote with $i: V \to B$ the inclusion mapping.
Let $f^{-1} \left({V}\right) \subseteq A$ be the preimage of $V$ under $f$.
Denote with $j: f^{-1} \left({V}\right) \to A$ the inclusion mapping.
Denote with $\bar f = f \restriction_{f^{-1} \left({V}\right)}$ the restriction of $f$ to $f^{-1} \left({V}\right)$.
Then:
$\quad\quad \begin{xy}\xymatrix{
f^{-1} \left({V}\right)
\ar[r]^*+{\bar f}
\ar[d]_*+{j}
&
V
\ar[d]^*+{i}
\\
A
\ar[r]_*+{f}
&
B
}\end{xy}$
is a pullback diagram in $\mathbf{Set}$.

Proof:
From the definition of pullback, given a commutative diagram:
$\quad\quad \begin{xy}\xymatrix{
Q
\ar[r]^*+{q_1}
\ar[d]_*+{q_2}
&
V
\ar[d]^*+{i}
\\
A
\ar[r]_*+{f}
&
B
}\end{xy}$
we need to find a mapping $u: Q \to \map {f^{-1}} V$ such that $\bar f \circ u = q_1$ and $j \circ u = q_2$.
Let $x \in Q$; then $\map {q_1} x \in V \subseteq B$.
Note that the commutativity of the diagram implies that $\map {q_1} x = \map f {\map {q_2} x}$ since $i$ is an inclusion.
Hence also $\map f {\map {q_2} x} \in V$.
It follows by definition of preimage that $\map {q_2} x \in \map {f^{-1}} V$.
Thus define $u: Q \to \map {f^{-1}} V$ by restriction of $q_2$:
:$\map u x := \map {q_2 \restriction_{Q \times \map {f^{-1}} V}} x$
Then we have:
:$\map {\paren {j \circ u}} x = \map u x = \map {q_2} x$
since $j$ is an inclusion mapping.
Hence $q_2 = j \circ u$ by Equality of Mappings.
Furthermore:
:$\map {\bar f \circ u} x = \map {\bar f \circ q_2} x = \map f {\map {q_2} x} = \map {q_1} x$
since $\bar f$ and $u$ are restrictions of $f$ and $q_2$, respectively.
Hence $\bar f \circ u = q_1$ by Equality of Mappings.
Observe that any $u': Q \to \map {f^{-1}} V$ must satisfy:
:$j \circ u' = q_2 = j \circ u$
By Inclusion Mapping is Injection, $j$ is an injection.
From Injection iff Monomorphism in Category of Sets, we conclude $j$ is a monomorphism, and so $u = u'$.
This establishes that $u: Q \to \map {f^{-1}} V$ is unique.
Therefore, we have established that:
$\quad\quad \begin{xy}\xymatrix{
\map {f^{-1}} V
\ar[r]^*+{\bar f}
\ar[d]_*+{j}
&
V
\ar[d]^*+{i}
\\
A
\ar[r]_*+{f}
&
B
}\end{xy}$
is a pullback diagram in $\mathbf{Set}$.
{{qed}}
Theorem: Poincaré Plane is Abstract Geometry

The Poincaré plane $\struct {\H, L_H}$ is an abstract geometry.

Proof:
We will show that the axioms for an abstract geometry hold.
Theorem: Strong Separation Theorem

Let $C \subset \R^\ell$ be closed and convex.
Let $D = \set {\mathbf v} \subset C^c$.
Then $C$ and $D$ can be strongly separated.

Proof:
=== Lemma 1 ===
For any $\mathbf y \ne 0$ and any $\mathbf z \in \map {H_{\mathbf y}^<} r$, $r = \mathbf y \mathbf y$, the line segment joining $\mathbf y$ and $\mathbf z$ contains points with lengths strictly less than $\mathbf y$.
{{explain|Because of the loose use of commas to separate clauses, it is unclear what the above is supposed to mean. Is $r {{=}} \mathbf y \mathbf y$ part of the premise or conclusion? That is, should it be taken to mean "the line segment joining $\mathbf y$ and $\mathbf z$? (If so, then perhaps it ought to be $r {{=}} \mathbf y \mathbf z$.) Or is it one of the conditions on $\mathbf y$ and $\mathbf z$ which needs to be fulfilled in order for the conclusion to follow? (In that case, its meaning needs to be explained.}}
{{explain|What is the domain of $\mathbf y$? Presumably it is a vector of some kind, in which case the nature of $0$ also needs to be defined.}}
{{explain|$\map {H_{\mathbf y}^<} r$}}
Theorem: Carathéodory's Theorem (Convex Analysis)

Let $E \subset \R^l$.
Let $\mathbb x \in \map {\operatorname {conv} } E$, where $\map {\operatorname {conv} } E$ denotes the convex hull of $E$.
Then $\mathbf x$ is a convex combination of affinely independent points of $E$. 
In particular, $\mathbf x$ is a convex combination of at most $l + 1$ points of $E$.

Proof:
Since $\mathbb x \in \map {\operatorname {conv} } E$, $\mathbf x$ is a convex combination of points in $E$.
From the definition of convex combination:
:$\ds \mathbf x = \sum_{i \mathop = 1}^k \gamma_i \mathbf y_i$
with:
:$\gamma_i \ge 0$
:$\ds \sum_{i \mathop = 1}^k \gamma_i = 1$
and:
:$\mathbf y_i \in E$
Let $K \subset \N$ be the set of all possible $k$ such that $\mathbf x$ is a convex combination of $k$ elements of $E$.
By the Well-Ordering Principle, $K$ is well-ordered. 
$K$ has a smallest element $k_s$ by the definition of well-ordered sets.
Suppose that the set $\set {\mathbf y_i: i \le k_s}$ is affinely dependent.
From the condition for affinely dependent set, there exists a set $\set {\alpha_i: i \le k_s}$ such that for some $\alpha_i > 0$:
:$\ds \sum_{i \mathop = 1}^{k_s} \alpha_i \mathbf y_i = 0$
and:
:$\ds \sum_{i \mathop = 1}^{k_s} \alpha_i = 0$
Pick the smallest $\dfrac {\gamma_j} {\alpha_j} > 0$.
Then:
:$\ds \mathbf x = \paren {\sum_{i \mathop = 1}^{k_s} \gamma_i \mathbf y_i} + 0 = \paren {\sum_{i \mathop = 1}^{k_s} \gamma_i \mathbf y_i} - \paren {\frac {\gamma_j} {\alpha_j} \sum_{i \mathop = 1}^{k_s} \alpha_i \mathbf y_i}$ 
Rearrange to get:
:$\ds \mathbf x = \paren {\sum_{i \mathop = 1}^{k_s} \paren {\gamma_i - \frac {\gamma_j} {\alpha_j} \alpha_i} \mathbf y_i}$
Since $\gamma_j > 0$ is made the smallest and $\alpha_j > 0$ is made the greatest:
:$\dfrac {\alpha_i} {\alpha_j} \gamma_j \le \gamma_j \le \gamma_i$
for all $i \le k_s$.
Thus:
:$\paren {\gamma_i - \dfrac {\gamma_j} {\alpha_j} \alpha_i} \ge 0$
For $i = j$:
:$\paren {\gamma_i - \dfrac {\gamma_j} {\alpha_j} \alpha_i} = 0$
For $i \ne j$, let:
:$\gamma'_{i'} \equiv \gamma_i - \dfrac {\gamma_j} {\alpha_j} \alpha_i$
We can express:
:$\ds x = \sum_{i' \mathop = 1}^{k_s-1} \gamma'_{i'} \mathbf y_i$
which contradicts the assumption that $k_s = \min K$.
{{finish|It seems to intend to prove $k_s \le l + 1$ with affine independence of $\set {\mathbf y_i: i \le k_s}$.}}
{{qed}}
{{Namedfor|Constantin Carathéodory|cat = Carathéodory}}
Theorem: Limit of Sinc Function at Zero/Corollary

:$\ds \lim_{x \mathop \to 0} \frac x {\sin x} = 1$

Proof:
From the Sine Inequality, we have:
:$\size {\sin x} \le \size x$
From Sine of Zero is Zero, equality occurs at $x = 0$.
From the Tangent Inequality, we have:
:$x < \tan x$
From Tangent of Zero, equality occurs at $x = 0$.
Putting the two inequalities together, we obtain:
:$\sin x \le x \le \tan x$
Therefore, dividing through by $\map \sin x$, we have the inequality:
:$1 \le \dfrac \theta {\sin \theta} \le \dfrac 1 {\cos \theta}$
for all $\theta \in \openint {-\dfrac \pi 2} 0 \cup \openint 0 {\dfrac \pi 2}$.
Taking the limit of the leftmost term and the rightmost term :
:$\ds \lim_{\theta \mathop \to 0} \ 1 = 1$
:$\ds \lim_{\theta \mathop \to 0} \frac 1 {\cos \theta} = 1$
So by the Squeeze Theorem:
:$\ds \lim_{\theta \mathop \to 0} \frac \theta {\sin \theta} = 1$
{{qed}}
Category:Limit of Sinc Function at Zero
Category:Sinc Function
etqcglisj4c3n25xsfznqvmi3y28ga1
Theorem: Dicyclic Group is Non-Abelian Group/Corollary

The quaternion group $Q_4$ is a non-abelian group.

Proof:
The quaternion group $Q_4$ is an example of the dicyclic group with $4$ elements.
The result follows from Dicyclic Group is Non-Abelian Group.
{{qed}}
Theorem: Integral of Constant/Definite

:$\ds \int_a^b c \rd x = c \paren {b - a}$

Proof:
Let $f_c: \R \to \R$ be the constant function.
By definition:
:$\forall x \in \R: \map {f_c} x = c$
Thus:
:$\map \sup {f_c} = \map \inf {f_c} = c$
So from Darboux's Theorem, we have:
:$\ds c \paren {b - a} \le \int_a^b c \rd x \le c \paren {b - a}$
Hence the result.
{{qed}}
Theorem: Primitive of Constant

:$\ds \int c \rd x = c x + C$ where $C$ is an arbitrary constant.

Proof:
Let:
:$\ds \map F x = \int c \rd x$
From the definition of primitive:
:$\map {F'} x = c$
From Derivative of Function of Constant Multiple:
:$\map {\dfrac \d {\d x} } {c x} = c$
From Primitives which Differ by Constant:
:$\map {\dfrac \d {\d x} } {c x + C} = c$
Hence the result.
{{qed}}
Theorem: Primitive of Constant

:$\ds \int c \rd x = c x + C$ where $C$ is an arbitrary constant.

Proof:
From Linear Combination of Primitives:
:$\ds \int \paren {\lambda \map f x + \mu \map g x} \rd x = \lambda \int \map f x \rd x + \mu \int \map g x \rd x$
The result follows by setting $\lambda = c$ and $\mu = 0$.
{{qed}}
Theorem: Primitive of Constant

:$\ds \int c \rd x = c x + C$ where $C$ is an arbitrary constant.

Proof:
From Derivative of Constant Multiple:
:$\map {\dfrac \d {\d x} } {c \map f x} = c \map {\dfrac \d {\d x} } {\map f x}$
The result follows from the definition of primitive.
Theorem: Unbounded Set of Real Numbers is not Compact

Let $\R$ be the set of real numbers considered as a Euclidean space.
Let $S \subseteq \R$ be unbounded in $\R$.
Then $S$ is not a compact subspace of $\R$.

Proof:
By the rule of transposition, it suffices to show that if $S$ is a compact subspace of $\R$, then $S$ is bounded.
Let $\CC$ be the set of all open $\epsilon$-balls of $0$ in $\R$:
:$\CC = \set {\map {B_\epsilon} 0: \epsilon \in \R_{>0}}$
We have that:
:$\ds \bigcup \CC = \R \supseteq S$
From Open Ball of Metric Space is Open Set, it follows that $\CC$ is an open cover for $S$.
Let $\FF$ be a finite subcover of $\CC$ for $S$.
Then $\ds \bigcup \FF$ is the largest open $\epsilon$-ball in $\FF$.
Thus:
:$S \subseteq \ds \bigcup \FF \in \CC$
Hence, $S$ is bounded.
{{qed}}
Theorem: Unbounded Set of Real Numbers is not Compact

Let $\R$ be the set of real numbers considered as a Euclidean space.
Let $S \subseteq \R$ be unbounded in $\R$.
Then $S$ is not a compact subspace of $\R$.

Proof:
From:
* Real Number Line is Metric Space
* Compact Metric Space is Totally Bounded
* Totally Bounded Metric Space is Bounded
the result follows by the rule of transposition.
{{qed}}
Theorem: Continuous Mapping is Sequentially Continuous

Let $X$ and $Y$ be topological spaces.
Let $x \in X$.
Let $f: X \to Y$ be a mapping that is continuous at $x$.
Then $f$ is sequentially continuous at $x$.

Proof:
Let $\sequence {x_n}_{n \mathop \ge 1}$ be a sequence in $X$ converging to $x$.
Let $V$ be a neighborhood of $\map f x$ in $Y$.
We are required to show that there exists $N \in \N$ such that $\map f {x_n} \in V$ for all $n \ge N$.
By continuity of $f$, choose a neighborhood $U$ of $x$ in $X$ such that $\map f U \subseteq V$.
Since $\sequence {x_n}_{n \mathop \ge 1}$ converges, there exists $N \in \N$ such that $x_n \in U$ for all $n \ge N$.
Therefore we must have that $\map f {x_n} \in \map f U \subseteq V$ for all $n \ge N$, as required.
{{qed}}
Category:Continuous Mappings
Category:Sequential Continuity
9coxaixayer00g4m9nm2acfehfj8502