avewright/proofwiki-math huggingface dataset:
Theorem: Closed Linear Subspaces Closed under Intersection

Let $V$ be a topological vector space.
Let $\family {M_i}_{i \mathop \in I}$ be an $I$-indexed family of closed linear subspaces of $V$.
Then $M := \ds \bigcap_{i \mathop \in I} M_i$ is also a closed linear subspace of $V$.

Proof:
By Set of Linear Subspaces is Closed under Intersection, $M$ is a linear subspace of $V$.
By Topology Defined by Closed Sets, the intersection of closed sets is again closed.
As the $M_i$ are all closed, it follows that $M$ is closed.
Hence $M$ is a closed linear subspace of $V$.
{{qed}}
Category:Vector Subspaces
4qr0useq9yg5nggqucqyd0u0twbljkt
Theorem: Orthogonal Difference is Closed Linear Subspace

Let $H$ be a Hilbert space.
Let $M, N$ be closed linear subspaces of $H$.
Then the orthogonal difference $M \ominus N$ is also a closed linear subspace of $H$.

Proof:
By definition, $M \ominus N = M \cap N^\perp$.
By Orthocomplement is Closed Linear Subspace, $N^\perp$ is a closed linear subspace of $H$.
Hence the result, by Closed Linear Subspaces Closed under Intersection.
{{qed}}
Category:Hilbert Spaces
2lj3gg359w9cwzc1kxa4wbfnzjwhsak
Theorem: Closed Linear Subspaces Closed under Setwise Addition

Let $H$ be a Hilbert space.
Let $M, N$ be closed linear subspaces of $H$.
Then $M + N$ is also a closed linear subspace of $H$, where $+$ denotes setwise addition.

Proof:
By Linear Subspaces Closed under Setwise Addition, $M + N$ is a linear subspace of $H$.
Now to show that it is closed.
Let $P: H \to H$ denote the orthogonal projection on $M$.
Denote by $I - P$ the complementary projection of $P$.
Define $N' := \set {n - P n: n \in N}$.
$N'$ is a closed linear subspace of $H$.
{{explain|prove the above claim}}
Observe $m + n = \paren {m + P n} + \paren {n - P n} \in M + N'$; hence, $M + N \subseteq M + N'$. 
By $m + \paren {n - P n} = \paren {m - P n} + n \in M + N$, conclude that $M + N' \subseteq M + N$, hence equality.
Furthermore, $N' \subseteq \map {\operatorname{ran} } {I - P} = \map \ker P$ by Range of Idempotent is Kernel of Complementary Idempotent.
That is, $N' \subseteq M^\perp$ by Properties of Orthogonal Projection, and hence $M \perp N'$.
Denote by $P'$ the orthogonal projection on $N'$.
Suppose now that $h \in M + N'$. Then:
{{begin-eqn}}
{{eqn | l = h
      | r = \paren {P + \paren {I - P} } h
      | c = {{Defof|Identity Operator}}
}}
{{eqn | r = \paren {P + \paren {I - P} } \paren {P' + \paren {I - P'} } h
      | c = {{Defof|Identity Operator}}
}}
{{eqn | r = P P' h + \paren {I - P} P' h + P \paren {I - P'} h \paren {I - P} \paren {I - P'} h
}}
{{eqn | r = 0 + P'h + P h + 0
}}
{{end-eqn}}
For this last equality, observe $M \perp N'$, hence $M \subseteq N'^\perp$, $N' \subseteq M^\perp$ and $\paren {M + N'}^\perp \subseteq M^\perp \cup N'^\perp$.
{{finish|link to results establishing the implications of these relations for the associated projections. These results don't exist at the moment}}
The conclusion is that every $h \in M + N'$ can be uniquely decomposed as $P' h + P h$, with $P' h \in N', P h \in M$. 
So suppose there is a sequence $h_n \to h$ in $M + N'$. Then $P h_n$ and $P' h_n$ are sequences in $M, N'$, respectively.
As those are closed linear subspaces of $H$, there are $m \in M, n \in N'$ with $P h_n \to m, P' h_n \to n$.
It follows that $h = m + n \in M + N'$.
That is, $M + N' = M + N$ is a closed linear subspace of $H$.
{{qed}}
Category:Hilbert Spaces
szvj3cehozdhdfpdtb2zqqs2fmjmy7o
Theorem: Linear Subspaces Closed under Setwise Addition

Let $V$ be a $K$-vector space.
Let $M, N$ be linear subspaces of $V$.
Then $L := M + N$ is also a linear subspace of $V$, where $+$ denotes setwise addition.

Proof:
It needs to be demonstrated that $L$ is closed under $+$ and $\circ$.
So let $m_1 + n_1, m_2 + n_2 \in L$.
Then $\paren {m_1 + n_1} + \paren {m_2 + n_2} = \paren {m_1 + m_2} + \paren {n_1 + n_2} \in L$.
It follows that $L$ is closed under $+$.
Now let $\lambda \in K, m + n \in L$.
Then $\lambda \circ \paren {m + n} = \paren {\lambda \circ m} + \paren {\lambda \circ n} \in L$.
It follows that $L$ is closed under $\circ$.
Hence the result, by definition of linear subspace.
{{qed}}
Category:Vector Subspaces
fkp9zb9z6qnfaekdo3j3vmer3oxbvlp
Theorem: Complementary Projection is Projection

Let $\HH$ be a Hilbert space.
Let $A$ be a projection.
Then the complementary projection $I - A$ is also a projection.

Proof:
By Characterization of Projections, $A$ is Hermitian.
Then $\paren {I - A}^* = I^* - A^* = I - A$ from Adjoint is Conjugate Linear.
So $I - A$ is also Hermitian.
From Complementary Idempotent is Idempotent, $I - A$ is idempotent.
Hence, applying Characterization of Projections, $I - A$ is a projection.
{{qed}}
Theorem: Direct Sum of Subspace and Orthocomplement

Let $H$ be a Hilbert space.
Let $M$ be a closed linear subspace of $H$.
Denote by $M^\perp$ its orthocomplement.
Then the direct sum $M \oplus M^\perp$ is isomorphic to $H$.

Proof:
Assert that $U: M \oplus M^\perp \to H: \left({m, m^\perp}\right) \mapsto m + m^\perp$ is an isomorphism.
According to the definition of isomorphism, it is sufficient to check that $U$ is surjective and that:
:$\left\langle{ U \left({m, m^\perp}\right), U \left({n, n^\perp}\right) }\right\rangle_H = \left\langle{ \left({m, m^\perp}\right), \left({n, n^\perp}\right) }\right\rangle_{M \oplus M^\perp}$
First the surjectivity:
Denote by $P$ the orthogonal projection on $M$.
Then for any $h \in H$, have $h = Ph + \left({h - Ph}\right)$.
By definition of $P$, $Ph \in M$.
Furthermore, by Orthogonal Projection onto Orthocomplement, $h - Ph \in M^\perp$.
It follows that $h = U \left({Ph, h - Ph}\right)$, showing that $U$ is a surjection.
It remains to check that $U$ preserves the inner product:
{{begin-eqn}}
{{eqn|l = \left\langle{ U \left({m, m^\perp}\right), U \left({n, n^\perp}\right) }\right\rangle_H
     |r = \left\langle{ m + m^\perp, n + n^\perp}\right\rangle_H
}}
{{eqn|r = \left\langle{m, n}\right\rangle_H + \left\langle{m^\perp, n}\right\rangle_H + \left\langle{m, n^\perp}\right\rangle_H + \left\langle{m^\perp, n^\perp}\right\rangle_H
     |c = Linearity of $\left\langle{\cdot, \cdot}\right\rangle_H$
}}
{{eqn|r = \left\langle{m, n}\right\rangle_H + \left\langle{m^\perp, n^\perp}\right\rangle_H
     |c = Defining property of orthocomplement
}}
{{eqn|r = \left\langle{ \left({m, m^\perp}\right), \left({n, n^\perp}\right) }\right\rangle_{M \oplus M^\perp}
     |c = Definition of $\left\langle{\cdot, \cdot}\right\rangle_{M \oplus M^\perp}$
}}
{{end-eqn}}
Hence $U$ is an isomorphism, and so $M \oplus M^\perp$ is isomorphic to $H$.
{{qed}}
Theorem: Subset of Toset is Toset

Let $\left({S, \preceq}\right)$ be a totally ordered set.
Let $T \subseteq S$.
Then $\left({T, \preceq \restriction_T}\right)$ is also a totally ordered set.
In the above, $\preceq \restriction_T$ denotes the restriction of $\preceq$ to $T$.

Proof:
As $\left({S, \preceq}\right)$ is a totally ordered set, the relation $\preceq$ is a total ordering, and is by definition:
* reflexive
* antisymmetric
* transitive
* connected
From Properties of Restriction of Relation, a restriction of a relation which has all those properties inherits them all.
Thus $\preceq \restriction_T$ is also:
* reflexive
* antisymmetric
* transitive
* connected
and so is also a total ordering.
Hence the result, by definition of totally ordered set.
{{Qed}}
Theorem: Transfinite Induction/Principle 1

Let $\On$ denote the class of all ordinals.
Let $A$ denote a class.
Suppose that:
:For all elements $x$ of $\On$, if $x$ is a subset of $A$, then $x$ is an element of $A$.
Then $\On \subseteq A$.

Proof:
{{NotZFC}}
{{AimForCont}} that $\neg \On \subseteq A$.
Then:
:$\paren {\On \setminus A} \ne \O$
From Set Difference is Subset, $\On \setminus A$ is a subclass of the ordinals.
By Epsilon Relation is Strongly Well-Founded on Ordinal Class, $\On \setminus A$ must have a strictly minimal element $y$ under $\in$.
By Element of Ordinal is Ordinal, $y$ must be a subset of $\On$, the class of all ordinals.
However, from the fact that $y$ is a strictly minimal element under $\in$ of $\On \setminus A$:
:$\paren {\On \setminus A} \cap y = \O$
So by its subsethood of $\On$:
:$\paren {\On \cap y} \setminus A = \paren {y \setminus A} = \O$
Therefore $y \subseteq A$.
However, by the hypothesis, $y$ must also be an element of $A$.
This contradicts the fact that $y$ is an element of $\On \setminus A$.
Therefore $\On \subseteq A$.
{{qed}}
{{LEM|Reductio ad Absurdum|4}}
Theorem: Transfinite Induction/Principle 1

Let $\On$ denote the class of all ordinals.
Let $A$ denote a class.
Suppose that:
:For all elements $x$ of $\On$, if $x$ is a subset of $A$, then $x$ is an element of $A$.
Then $\On \subseteq A$.

Proof:
<onlyinclude>
{{AimForCont}} $\neg \On \subseteq A$.
Then:
:$\paren {\On \setminus A} \ne \O$
From Set Difference is Subset, $\On \setminus A$ is a subclass of the ordinals.
By Class of All Ordinals is Well-Ordered by Subset Relation, $\On \setminus A$ must have a smallest element $y$.
Then every strict predecessor of $y$ must lie in $A$, so by the premise, $y$ must also be an element of $A$.
This contradicts the fact that $y$ is an element of $\On \setminus A$.
Therefore $\On \subseteq A$.
{{qed}}
{{LEM|Reductio ad Absurdum|4}}
Category:Transfinite Induction
7g74p8tq95kw7avuvsggqard03hcaq3
Theorem: Limit of Functions that Agree

Let $f$ and $g$ be real functions.
Let $f$ and $g$ agree for all $x$ in a deleted neighborhood of $c$.
Let the limit:
:$\ds \lim_{x \mathop \to c} \map f x$
exist.
Then the limit:
:$\ds \lim_{x \mathop \to c} \map g x$
also exists, and:
:$\ds \lim_{x \mathop \to c} \map f x = \lim_{x \mathop \to c} \map g x$

Proof:
By hypothesis:
:$\map f x = \map g x$
for all $x$ such that:
:$x \in \R: 0 < \size {\alpha - x} < \epsilon$
Putting $c$ for $\alpha$ and $\delta$ for $\epsilon$, this is equivalent to:
:$x \in \R: 0 < \size {x - c} < \delta$
By definition, that the limit of $\map f x$ exists is to say:
:$\exists L: \forall \epsilon \in \R_{>0}: \exists \delta \in \R_{>0}: 0 < \size {x - c} < \delta \implies \size {\map f x - L} < \epsilon$
For all $x$ relevant, we can substitute $\map f x$ with $\map g x$ and get:
:$\exists L: \forall \epsilon \in \R_{>0}: \exists \delta \in \R_{>0}: 0 < \size {x - c} < \delta \implies \size {\map g x - L} < \epsilon$
The result follows by the definition of limit.
{{qed}}
Theorem: Ordering of Reciprocals

Let $x, y \in \R$ be real numbers such that $x, y \in \openint 0 \to$ or $x, y \in \openint \gets 0$
Then:
:$x \le y \iff \dfrac 1 y \le \dfrac 1 x$

Proof:
By Reciprocal Function is Strictly Decreasing, the reciprocal function is strictly decreasing.
By Mapping from Totally Ordered Set is Dual Order Embedding iff Strictly Decreasing, the reciprocal function is a dual order embedding.
That is:
:$x \le y \iff \dfrac 1 y \le \dfrac 1 x$
{{qed}}
Theorem: Ordering of Reciprocals

Let $x, y \in \R$ be real numbers such that $x, y \in \openint 0 \to$ or $x, y \in \openint \gets 0$
Then:
:$x \le y \iff \dfrac 1 y \le \dfrac 1 x$

Proof:
By Reciprocal Function is Strictly Decreasing, the reciprocal function is strictly decreasing.
Thus 
:$x \le y \implies \dfrac 1 y \le \dfrac 1 x$
Suppose then that $\dfrac 1 y \le \dfrac 1 x$.
If $x, y > 0$, then from Reciprocal of Strictly Positive Real Number is Strictly Positive:
$\dfrac 1 y, \dfrac 1 x > 0$
Similarly, if $x, y < 0$ or $x, y > 0$, then from Reciprocal of Strictly Negative Real Number is Strictly Negative:
:$\dfrac 1 y, \dfrac 1 x < 0$
Thus we can apply the above to show that:
:$\dfrac 1 {1/x} \le \dfrac 1 {1/y}$
By Inverse of Multiplicative Inverse:
:$x \le y$
{{qed}}
Theorem: Comparison Test for Divergence

Let $\ds \sum_{n \mathop = 1}^\infty b_n$ be a divergent series of positive real numbers.
Let $\sequence {a_n}$ be a sequence in $\R$.
Let:
:$\forall n \in \N_{>0}: b_n \le a_n$
Then the series $\ds \sum_{n \mathop = 1}^\infty a_n$ diverges.

Proof:
This is the contrapositive of the Comparison Test. 
Hence the result, from the Rule of Transposition.
{{qed}}
Theorem: Axiom of Choice implies Zorn's Lemma

Let the {{Axiom-link|Choice}} be accepted.
Then Zorn's Lemma holds.

Proof:
{{AimForCont}} that for each $x \in X$ there is a $y \in X$ such that $x \prec y$.
By the Axiom of Choice, there is a mapping $f: X \to X$ such that:
:$\forall x \in X: x \prec \map f x$
Let $\CC$ be the set of all chains in $X$.
By the premise, each element of $\CC$ has an upper bound in $X$.
Thus by the Axiom of Choice, there is a mapping $g: \CC \to X$ such that for each $C \in \CC$, $\map g C$ is an upper bound of $C$.
Let $p$ be an arbitrary element of $X$.
Define a mapping $h: \On \to X$ by transfinite recursion thus:
{{begin-eqn}}
{{eqn | l = \map h 0
      | r = p
}}
{{eqn | l = \map h {\alpha^+}
      | r = \map f {\map h \alpha}
}}
{{eqn | l = \map h \lambda
      | r = \map f {\map g {h \sqbrk \lambda} }
      | c = if $\lambda$ is a limit ordinal
}}
{{end-eqn}}
when $h \sqbrk \lambda$ is the image set of $\lambda$ under $h$.
{{explain|If you're defining the mapping $h$, how can you define it in terms of itself? $\map h \lambda {{=}} \map f {\map g {h \sqbrk \lambda} }$ looks weird. Might be worth going to the Talk page to discuss.}}
Then $h$ is strictly increasing, and thus injective.
{{explain|The above statement needs to be justified.}}
Let $h'$ be the restriction of $h$ to $\On \times \map h \On$.
Then ${h'}^{-1}$ is a surjection from $\map h \On \subseteq X$ onto $\On$.
By the Axiom of Replacement, $\On$ is a set.
By the Burali-Forti Paradox, this is a contradiction.
Thus we conclude that some element of $X$ has no strict successor, and is thus maximal.
{{qed}}
Theorem: Axiom of Choice implies Zorn's Lemma

Let the {{Axiom-link|Choice}} be accepted.
Then Zorn's Lemma holds.

Proof:
We have that Axiom of Choice implies Tukey's Lemma.
Then we have Tukey's Lemma implies Zorn's Lemma.
{{qed}}
Theorem: Limit at Infinity of Real Identity Function

Let $I_\R: \R \to \R$ be the identity function on $\R$.
Then:
:$(1): \quad \ds \lim_{x \mathop \to +\infty} \map {I_\R} x = +\infty$
:$(2): \quad \ds \lim_{x \mathop \to -\infty} \map {I_\R} x = -\infty$

Proof:
We have that the Derivative of Identity Function is $1$.
Hence, by Derivative of Monotone Function, $x$ is strictly increasing.
Now, by the definition of infinite limit at infinity, the first assertion is:
:$\forall M \in \R_{>0}: \exists N \in \R_{>0}: x > N \implies \map f x > M$
For every $M$, choose $N = M$.
The second assertion is proved similarly.
{{qed}}
Category:Unbounded Mappings
Category:Identity Mappings
gleewlc3n78jwckf22jbp2o6t443yrx
Theorem: Push Theorem

Let $f$ be a real function which is continuous on the open interval $\openint a \to$, $a \in \R$, such that:
:$\ds \lim_{x \mathop \to +\infty} \map f x = +\infty$
Let $g$ be a real function defined on some open interval $\openint b \to$ such that, for sufficiently large $x$:
:$\map g x > \map f x$
Then:
:$\ds \lim_{x \mathop \to +\infty} \map g x = +\infty$

Proof:
Let $\ds \lim_{x \mathop \to +\infty} \map f x = +\infty$.
By the definition of infinite limit at infinity, this means:
:$\forall M_1 \in \R_{>0}: \exists N_1 \in \R_{>0}: x > N_1 \implies \map f x > M_1$
Now, the assertion that $\map g x \to +\infty$ is:
:$\forall M_1 \in \R_{>0}: \exists N_2 \in \R_{>0}: x > N_2 \implies \map g x > M_1$
By the premise that $\map g x > \map f x$ for sufficiently large $x$, there is an $N$ such that:
:$x > N \implies \map g x > \map f x$
Now, given $M_1$, let $N_2$ be greater than both $N_1$ and $N$.
Then since $N_2 > N$ and $N_2 > N_1$ respectively:
:$\map g x > \map f x > M_1$
whence:
:$\ds \lim_{x \mathop \to +\infty} \map g x = +\infty$
{{qed}}
Theorem: Intersection of Orthocomplements is Orthocomplement of Closed Linear Span

Let $H$ be a Hilbert space.
Let $\family {M_i}_{i \mathop \in I}$ be an $I$-indexed family of closed linear subspaces of $H$.
Then:
:$\ds \bigcap_{i \mathop \in I} M_i^\perp = \paren {\vee \set {M_i : i \in I} }^\perp$
where:
:$\perp$ denotes orthocomplementation
:$\vee$ denotes closed linear span.

Proof:
By definition of set equality, it suffices to prove the following two inclusions:
:$\ds \bigcap_{i \mathop \in I} M_i^\perp \subseteq \paren {\vee \set {M_i : i \in I} }^\perp$
:$\paren {\vee \set {M_i : i \in I} }^\perp \subseteq \ds \bigcap_{i \mathop \in I} M_i^\perp$
Theorem: Zorn's Lemma implies Axiom of Choice

Let Zorn's Lemma be accepted.
Then the Axiom of Choice holds.

Proof:
Let $X$ be a set.
Let $\FF$ be the set of partial choice functions defined as:
:<nowiki>$f \in \FF \iff \begin{cases}
\Dom f \subseteq \powerset X & \ \\
\Img f \subseteq X & \ \\
\forall A \in \Dom f: \map f A \in A & \ \end{cases}$</nowiki>
Let $\preceq$ be the relation defined on $\FF$ as:
:$\forall f_1, f_2 \in \FF: f_1 \preceq f_2 \iff f_2$ is an extension of $f_1$.
Straightforwardly, $\preceq$ is a partial ordering on $\FF$.
We can also see that the Empty Mapping is an element of $\FF$.
Let $C \subseteq \FF$ be a non-empty chain in $\FF$.
Let $U$ be the union of all domains of mappings in $C$.
Furthermore, let $f$ be the union of all graphs of mappings in $C$.
For each $x \in U$, all mappings $g \in C$ with $x \in \Dom g$ have the same value at $x$.
Thus there is a unique $y \in X$ such that $\tuple {x, y} \in f$.
Hence $f: U \rightarrow X$ is a mapping.
By construction, we also have $\map f x \in x$ for all $x \in \Dom f = U$.
That is, every non-empty chain in $\FF$ has an upper bound.
Suppose Zorn's Lemma holds.
Then there exists a maximal element of $\FF$.
{{explain|Check the chain condition (and nonemptiness of $\FF$)}}
We then show by contraposition that if $g$ is such a maximal element, then:
:$\Dom g = \powerset X \setminus \O$
In that case, we will have constructed a choice function $\powerset X \setminus \set \O \rightarrow X$.
Suppose that $\Dom g \ne \powerset X \setminus \O$.
Then there is an $A \in \paren {\powerset X \setminus \O} \setminus \Dom g$.
Let $x \in A$.
We can then define the mapping $\hat g: \set A \cup \Dom g$ by defining:
:$\forall S \in \Dom g: \forall \map {\hat g} A = x: \map {\hat g} S = \map g S$
That way, we clearly have $\hat g \ne g$ and $\hat g \preceq g$.
Thus $g$ is not maximal in $\FF$.
{{explain|How does this prove the hypothesis?}}
Theorem: Orthocomplement Reverses Subset

Let $\struct {V, \innerprod \cdot \cdot}$ be an inner product space space.
Let $A, B$ be subsets of $V$ with $A \subseteq B$.
Then: 
:$B^\perp \subseteq A^\perp$
where $\perp$ denotes orthocomplementation.

Proof:
Let: 
:$h \in B^\perp$
Then, from the definition of orthocomplement, we have:
:$h \perp b$ for each $b \in B$.
Since $A \subseteq B$, we in particular have: 
:$h \perp a$ for each $a \in A$.
So, from the definition of orthocomplement:
:$h \in A^\perp$
So:
:$h \in B^\perp$ implies $h \in A^\perp$.
So, from the definition of subset:
:$B^\perp \subseteq A^\perp$
{{qed}}
Category:Inner Product Spaces
Category:Orthocomplements
cxqts8fx2hcygfdmpx4qt42nhwpzuw6
Theorem: Limit at Infinity of x^n

Let $x \mapsto x^n$, $n \in \R$ be a real function which is continuous on the open interval $\openint 1 {+\infty}$.
Let $n > 0$.
Then $x^n \to +\infty$ as $x \to +\infty$.

Proof:
From Upper Bound of Natural Logarithm:
:$\forall n > 0: n \ln x < x^n$
which, by Multiple Rule for Continuous Real Functions, implies:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to +\infty} n \ln x
      | r = n \lim_{x \mathop \to +\infty} \ln x
}}
{{end-eqn}}
From Logarithm Tends to Infinity:
:$n \ln x \to +\infty$ as $x \to +\infty$
The result follows from the Push Theorem.
{{qed}}
Theorem: Monotonicity of Real Sequences

Let $\mathbb D$ be a subset of $\N$.
Let $\sequence {a_n}: \mathbb D \to \R$ be a real sequence.
Let $\mathbb X$ be a real interval such that $\mathbb D \subseteq \mathbb X$.
Let $f: \mathbb X \to \R, x \mapsto \map f x$ be a differentiable real function.
Suppose that for every $n \in \mathbb D$:
:$\map f n = a_n$
Then:
:If $\forall x \in \mathbb X: D_x \map f x \ge 0$, $\sequence {a_n}$ is increasing
:If $\forall x \in \mathbb X: D_x \map f x >  0$, $\sequence {a_n}$ is strictly increasing
:If $\forall x \in \mathbb X: D_x \map f x \le 0$, $\sequence {a_n}$ is decreasing
:If $\forall x \in \mathbb X: D_x \map f x < 0$, $\sequence {a_n}$ is strictly decreasing
where $D_x$ denotes differentiation {{WRT|Differentiation}} $x$.

Proof:
Consider the case where $D_x \map f x \ge 0$
Let $n \in \N$ be in the domain of $\sequence {a_n}$.
From Derivative of Monotone Function, the sign of $D_x f$ is indicative of the monotonicity of $f$.
Because Differentiable Function is Continuous and Continuous Real Function is Darboux Integrable, $D_x f$ is integrable.
Hence:
{{begin-eqn}}
{{eqn | l = \map f {n + 1} - \map f n
      | r = \int_n^{n + 1} D_x \map f x \rd x \ge 0
      | c = Fundamental Theorem of Calculus
}}
{{eqn | o = \ge
      | r = 0
      | c = Relative Sizes of Definite Integrals
}}
{{eqn | ll= \leadsto
      | l = \map f {n + 1}
      | o = \ge
      | r = \map f n
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | q = \forall n \in \mathbb D
      | l = \map f n
      | r = a_n
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | q = \forall n \in \mathbb D
      | l = a_{n + 1}
      | o = \ge
      | r = a_n
      | c = as $n \in \mathbb D$ was arbitrary
}}
{{end-eqn}}
Hence the result, by the definition of monotone.
The proofs of the other cases are similar.
{{qed}}
Theorem: Hausdorff's Maximal Principle is equivalent to Axiom of Choice

Every ordered set has a maximal chain {{iff}} the axiom of choice holds.

Proof:
* Axiom of Choice implies Hausdorff's Maximal Principle
* Hausdorff's Maximal Principle implies Zermelo's Well-Ordering Theorem
* Zermelo's Well-Ordering Theorem is Equivalent to Axiom of Choice
{{qed}}
Theorem: Young's Inequality for Products

Let $p, q \in \R_{> 0}$ be strictly positive real numbers such that:
:$\dfrac 1 p + \dfrac 1 q = 1$
Then:
:$\forall a, b \in \R_{\ge 0}: a b \le \dfrac {a^p} p + \dfrac {b^q} q$
Equality occurs {{iff}}:
:$b = a^{p - 1}$

Proof:
{{WLOG}} assume that $a^p \ge b^q$, otherwise swap $a$ with $b$ and $p$ with $q$. 
Define $f : \hointr 0 \infty \to \R$ by: 
:$\ds \map f t = \frac {t^p} p + \frac 1 q - t$
We have, from Derivative of Power and Sum Rule for Derivatives:
:$\ds \map {f'} t = t^{p - 1} - 1$
So for $t \ge 1$ we have: 
:$\ds \map {f'} t \ge 0$
So, from Real Function with Positive Derivative is Increasing, we have: 
:$f$ is increasing on $\hointr 1 \infty$. 
That is: 
:$\map f t \ge \map f 1$
for all $t \ge 1$.
Since $a^p \ge b^q$, we have: 
:$a^p b^{-q} \ge 1$
so:
:$a b^{-q/p} \ge 1$
So:
:$\map f {a b^{-q/p} } \ge \map f 1$
That is: 
:$\ds \frac {a^p b^{-q} } p + \frac 1 q - a b^{-q/p} \ge \frac 1 p + \frac 1 q - 1$
By hypothesis, we have: 
:$\ds \frac 1 p + \frac 1 q = 1$
So it follows that: 
:$\ds \frac {a^p b^{-q} } p + \frac 1 q \ge a b^{-q/p}$
So:
:$\ds \frac {a^p} p + \frac {b^q} q \ge a b^{q \paren {1 - 1/p} }$
Finally, we have: 
:$\ds 1 - \frac 1 p = \frac 1 q$
so:
:$\ds q \paren {1 - \frac 1 p} = 1$
giving: 
:$\ds \frac {a^p} p + \frac {b^q} q \ge a b$
For the equality case, note that: 
:$\map {f'} t > 0$
for $t > 1$.
So, from Real Function with Strictly Positive Derivative is Strictly Increasing, we have: 
:$f$ is strictly increasing for $t > 1$.
So: 
:$\map f {a b^{-q/p} } = \map f 1$
that is: 
:$\ds a b = \frac {a^p} p + \frac {b^q} q$
{{iff}}: 
:$a b^{-q/p} = 1$ 
That is:
:$b = a^{p/q}$
We have:
:$\ds \frac 1 p + \frac 1 q = 1$
and so:
:$\ds 1 + \frac p q = p$
giving:
:$\ds \frac p q = p - 1$
So we have:
:$b = a^{p - 1}$
as required.
{{qed}}