avewright/proofwiki-math huggingface dataset:
Theorem: Slow g-Tower is Slowly Well-Ordered under Subset Relation

Let $M$ be a class.
Let $g: M \to M$ be a slowly progressing mapping on $M$.
Let $M$ be a slow $g$-tower.
Then $M$ is slowly well-ordered under the subset relation.

Proof:
Let $M$ be a slow $g$-tower.
By $g$-Tower is Well-Ordered under Subset Relation: Empty Set:
:$\O$ is the smallest element of $M$.
This is condition $(\text S_1)$ of the definition of slowly well-ordered class under subset relation.
By $g$-Tower is Well-Ordered under Subset Relation: Union of Limit Elements:
:Each limit element $x$ of $M$ is the union of its lower section $\bigcup x^\subset$
This is condition $(\text S_3)$ of the definition of slowly well-ordered class under subset relation.
It remains to establish condition $(\text S_2)$ of the definition of slowly well-ordered class under subset relation.
Let $x \in M$ be arbitrary.
Let $y$ be the immediate successor of $x$.
Then $x$ is not the greatest element of $M$.
Hence by $g$-Tower is Well-Ordered under Subset Relation: Successor of Non-Greatest Element:
:$y = \map g x$
Because $g$ is slowly progressing, $y$ contains at most $1$ more element than $x$.
But we also have that $y$ is the immediate successor of $x$.
Thus $x$ is a proper subset of $y$.
So $y$ contains at least $1$ more element than $x$.
Hence $y$ contains exactly $1$ element which is not in $x$.
The result follows.
{{qed}}
Theorem: Union of Slowly Well-Ordered Class under Subset Relation is Well-Orderable

Let $N$ be a class.
Let $N$ be slowly well-ordered under the subset relation.
Then $\bigcup N$ is well-orderable.

Proof:
Let $N$ be slowly well-ordered under $\subseteq$.
Let $A = \bigcup N$.
For $a \in A$, let $\map F a$ denote the smallest element of $N$ that contains $a$.
Then for $a, b \in A$, we define $a \preccurlyeq b \iff \map F a \subseteq \map F b$.
It will be shown that $\preccurlyeq$ is a well-ordering on $A$.
By Class which has Injection to Subclass of Well-Orderable Class is Well-Orderable, it is sufficient to show that $F$ is an injection.
So, let us assume that $\map F a = \map F b$ for arbitrary $a, b \in A$.
By condition $S_1$ of the definition of slowly well-ordered under $\subseteq$, $\O \in N$ is the smallest element of $N$.
We have that $a \in \map F a$ by definition.
Hence $\map F a$ cannot be the smallest element of $N$.
Suppose $\map F a$ were a limit element of $N$.
Then by condition $S_3$ of the definition of slowly well-ordered under $\subseteq$, $\map F a$ would be the union of its lower section $\map \bigcup {\paren {\map F a}^\subset}$
But no element of the lower section of $\map F a$ can contain $a$.
Hence $\map \bigcup {\paren {\map F a}^\subset}$ cannot contain $a$.
Hence $\map F a$ cannot be a limit element of $N$.
By Categories of Elements under Well-Ordering, $\map F a$ must therefore be the immediate successor element of some $x \in N$.
As $a$ is the immediate predecessor of $x$, it follows by the definition of $\map F a$ that $a \notin x$.
However, by condition $S_2$ of the definition of slowly well-ordered under $\subseteq$, $\map F a$ contains exactly $1$ more element than $x$.
Hence as $a \in \map F a$ but $a \notin x$ it must be the case that $a$ must be that $1$ more element.
Hence:
:$\map F a = x \cup \set a$
As $\map F a = \map F b$ {{hypothesis}}:
:$\map F b = x \cup \set a$
As $\map F b$ is the smallest element of $N$ that contains $b$, we have:
:$b \ne x$
Hence:
:$b \in \set a$
which means:
:$b = a$
We have shown that:
:$\map F a = \map F b \implies a = b$
and so by definition $F$ is an injection.
Thus, by Class which has Injection to Subclass of Well-Orderable Class is Well-Orderable, the result follows.
{{qed}}
The following results also hold:
Theorem: Deduction Theorem for Hilbert Proof System for Predicate Logic

Let $\mathscr H$ be instance 1 of a Hilbert proof system for predicate logic.
Then the deduction rule:
::$\dfrac{U,\mathbf A \vdash \mathbf B}{U \vdash \mathbf A \implies \mathbf B}$
is a derived rule for provable consequences in $\mathscr H$.

Proof:
For any proof of $U, \mathbf A \vdash \mathbf B$, we indicate how to transform it into a proof of $U \vdash \mathbf A \implies \mathbf B$ without using the deduction rule.
This is done by applying the Second Principle of Mathematical Induction to the length $n$ of the proof of $U,\mathbf A \vdash \mathbf B$.
By definition of $\mathscr H$, then one of the following must occur:
* $\mathbf B \in U$
* $\mathbf B$ is an axiom of $\mathscr H$
* $\mathbf B = \mathbf A$
* $\mathbf B$ is derived from Modus Ponens
In the first two cases, we can craft the following proof of $U \vdash \mathbf A \implies \mathbf B$:
{{BeginTableau|U \vdash \mathbf A \implies \mathbf B|nohead = true}}
{{TableauLine
| n    = 1
| pool = 
| f    = \mathbf B
| rlnk = Definition:Axiom (Formal Systems)
| rtxt = Axiom of $\map {\mathscr H} U$
| dep  = (None)
| c    = By definition of provable consequence
}}
{{TableauLine
| n    = 2
| pool = 
| f    = \mathbf B \implies \paren{ \mathbf A \implies \mathbf B }
| rlnk = Definition:Hilbert Proof System Instance 1 for Predicate Logic
| rtxt = Axiom 1
| dep  = (None)
| c    = True Statement is Implied by Every Statement
}}
{{ModusPonens|3||\mathbf A \implies \mathbf B|1|2}}
{{EndTableau}}
{{qed|lemma}}
Next, if $\mathbf B = \mathbf A$, then $\mathbf A \implies \mathbf B$ is a tautology, and hence satisfies axiom 1 of $\mathscr H$.
{{qed|lemma}}
Lastly, suppose that $\mathbf B$ is derived from Modus Ponens, so that we have $\mathbf B'$ and $\mathbf B' \implies \mathbf B$ as provable consequences of $U, \mathbf A$.
By the induction hypothesis, we have proofs of $U \vdash \mathbf A \implies \mathbf B'$ and $U \vdash \mathbf A \implies \paren{ \mathbf B' \implies \mathbf B }$.
Then, expanding upon these proofs:
{{BeginTableau|U \vdash \mathbf A \implies \mathbf B|nohead = true}}
{{TableauLine
| n    = 1
| pool = 
| f    = \mathbf A \implies \mathbf B'
| rlnk = Definition:Induction Hypothesis
| rtxt = Induction Hypothesis
| dep  = (None)
| c    = 
}}
{{TableauLine
| n    = 2
| pool = 
| f    = \mathbf A \implies \paren{ \mathbf B' \implies \mathbf B }
| rlnk = Definition:Induction Hypothesis
| rtxt = Induction Hypothesis
| dep  = (None)
| c    = 
}}
{{TableauLine
| n    = 3
| pool = 
| f    = \mathbf A \implies \paren{ \mathbf B' \implies \mathbf B } \implies \paren{ \paren{ \mathbf A \implies \mathbf B' } \implies \paren{ \mathbf A \implies \mathbf B } }
| rlnk = Definition:Hilbert Proof System Instance 1 for Predicate Logic
| rtxt = Axiom 1
| dep  = (None)
| c    = Self-Distributive Law for Conditional
}}
{{ModusPonens|4||\paren{ \mathbf A \implies \mathbf B' } \implies \paren{ \mathbf A \implies \mathbf B }|2|3}}
{{ModusPonens|5||\mathbf A \implies \mathbf B|1|4}}
{{EndTableau}}
{{qed|lemma}}
Hence the result by the Second Principle of Mathematical Induction.
{{qed}}
Theorem: Union of Slow g-Tower is Well-Orderable

Let $M$ be a class.
Let $g: M \to M$ be a slowly progressing mapping on $M$.
Let $M$ be a slow $g$-tower.
Then $\ds \bigcup M$ is well-orderable.

Proof:
Let $M$ be a slow $g$-tower.
From Slow $g$-Tower is Slowly Well-Ordered under Subset Relation we have that $M$ is slowly well-ordered under $\subseteq$.
The result follows from Union of Slowly Well-Ordered Class under Subset Relation is Well-Orderable.
{{qed}}
Theorem: Measure is countably subadditive

Let $\left({X, \Sigma, \mu}\right)$ be a measure space.
Then $\mu$ is $\sigma$-subadditive, that is:
:$\ds\forall \sequence {A_n} _{n \in \N} \subseteq \Sigma: \map \mu {\bigcup _{n \in \N} A_n} \le \sum _{n \in \N} \map \mu {A_n}$

Proof:
For each $n\in\N$, let:
:$\ds A'_n := A_n \setminus \bigcup _{i=0} ^{n-1} A_i$
Then, by (SA3) and (SA2'):
:$\forall n\in\N : A'_n \in \Sigma$
Furthermore, by construction:
:$\bigcup _{n \in \N} A'_n = \bigcup _{n \in \N} A_n$
:$\sequence {A'_n} _{n \in \N}$ are pairwise disjoint
:$\forall n\in\N : A' _n\subseteq A_n$
Therefore:
{{begin-eqn}}
{{eqn | l = \map \mu {\bigcup _{n \in \N} A_n}
      | r = \map \mu {\bigcup _{n \in \N} A'_n} }}
{{eqn | r = \sum _{n \in \N} \map \mu {A' _n}
      | c = (2) of definition of measure}}
{{eqn | r = \sum _{n \in \N} \map \mu {A_n}
      | o = \le
      | c = Measure is Monotone}}
{{end-eqn}}
{{qed}}
Category:Measures
eqsbj7cr45gfz8118t9rtg2v439hy5f
Theorem: Set with Slowly Progressing Mapping on Power Set with Self as Fixed Point is Well-Orderable

Let $S$ be a set of sets.
Let there exist a slowly progressing mapping $g: \powerset S \to \powerset S$, where $\powerset S$ denotes the power set of $S$.
Let $g$ have exactly one fixed point $S$.
Then $S$ is well-orderable.

Proof:
Let the hypothesis be assumed.
We have that:
:$\O \in \powerset S$
:$\powerset S$ is closed under $g$
:$\powerset S$ is closed under chain unions.
Hence $\powerset S$ is superinductive under $g$.
Let $M$ be the intersection of all subsets of $S$ that are superinductive under $g$.
From:
:Intersection of Set whose Every Element is Closed under Mapping is also Closed under Mapping
:Intersection of Set whose Every Element is Closed under Chain Unions is also Closed under Chain Unions
it follows by definition that $M$ is minimally superinductive under $g$.
Hence by definition $M$ is a slow $g$-tower.
By Union of $g$-Tower is Greatest Element and Unique Fixed Point:
:$\ds \bigcup M \in M$ and $\ds \bigcup M$ is a fixed point of $g$.
But $S$ is the only fixed point of $g$.
Hence:
:$\ds \bigcup M = S$
From Union of Slow $g$-Tower is Well-Orderable, it follows that $S$ is well-orderable.
{{qed}}
Theorem: L-Infinity Norm is Well-Defined

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\map {\LL^\infty} {X, \Sigma, \mu}$ be the Lebesgue $\infty$-space for $\struct {X, \Sigma, \mu}$.
Let $\sim$ be the $\mu$-almost-everywhere equality relation on $\map {\LL^\infty} {X, \Sigma, \mu}$.
Let $\map {L^\infty} {X, \Sigma, \mu}$ be the $L^\infty$ space on $\struct {X, \Sigma, \mu}$.
Let $\eqclass f \sim \in \map {L^\infty} {X, \Sigma, \mu}$. 
Then the $L^\infty$ norm: 
:$\ds \norm {\eqclass f \sim}_\infty = \norm f_\infty$
is well-defined.

Proof:
We show that for $E \in \map {L^\infty} {X, \Sigma, \mu}$, $\norm E_\infty$ is independent of the representative chosen for $E$.
Let:
:$E = \eqclass f \sim = \eqclass g \sim$
for $\eqclass f \sim, \eqclass g \sim \in \map {L^\infty} {X, \Sigma, \mu}$.
We show that: 
:$\norm f_\infty = \norm g_\infty$
From Equivalence Class Equivalent Statements, we have: 
:$f \sim g$
So, from the definition of the almost-everywhere equality relation, we have: 
:$\map f x = \map g x$ for $\mu$-almost all $x \in X$.
That is, there exists a $\mu$-null set $N$ such that: 
:if $\map f x \ne \map g x$ then $x \in N$.
We show that: 
:$\map \mu {\set {x \in X : \size {\map f x} \ge c} } = \map \mu {\set {x \in X : \size {\map g x} \ge c} }$ 
From this it will follow that: 
:$\inf \set {c > 0 : \map \mu {\set {x \in X : \size {\map f x} \ge c} } = 0} = \inf \set {c > 0 : \map \mu {\set {x \in X : \size {\map g x} \ge c} } = 0}$
That is: 
:$\norm f_\infty = \norm g_\infty$
Clearly: 
:$\set {x \in N : \size {\map f x} \ge c} \subseteq N$
So, from Null Sets Closed under Subset:
:$\map \mu {\set {x \in N : \size {\map f x} \ge c} } = 0$
Swapping $f$ for $g$, we also obtain: 
:$\map \mu {\set {x \in N : \size {\map g x} \ge c} } = 0$
Since: 
:$\set {x \in N : \size {\map f x} \ge c} \subseteq N$
and:
:$\set {x \in X \setminus N : \size {\map f x} \ge c} \subseteq X \setminus N$
we have that: 
:$\set {x \in N : \size {\map f x} \ge c}$ and $\set {x \in X \setminus N : \size {\map f x} \ge c}$ are disjoint for all real numbers $c > 0$. 
Then:
{{begin-eqn}}
{{eqn | l = \map \mu {\set {x \in X : \size {\map f x} \ge c} }
      | r = \map \mu {\set {x \in N : \size {\map f x} \ge c} \cup \set {x \in X \setminus N : \size {\map f x} \ge c} }
}}
{{eqn | r = \map \mu {\set {x \in N : \size {\map f x} \ge c} } + \map \mu {\set {x \in X \setminus N : \size {\map f x} \ge c} }
      | c = from the countable additivity of $\mu$
}}
{{eqn | r = \map \mu {\set {x \in X \setminus N : \size {\map f x} \ge c} }
}}
{{eqn | r = \map \mu {\set {x \in X \setminus N : \size {\map g x} \ge c} }
      | c = since $\map f x = \map g x$ for all $x \in X \setminus N$
}}
{{eqn | r = \map \mu {\set {x \in N : \size {\map g x} \ge c} } + \map \mu {\set {x \in X \setminus N : \size {\map g x} \ge c} }
}}
{{eqn | r = \map \mu {\set {x \in N : \size {\map g x} \ge c} \cup \set {x \in X \setminus N : \size {\map g x} \ge c} }
      | c = using the countable additivity of $\mu$
}}
{{eqn | r = \map \mu {\set {x \in X : \size {\map g x} \ge c} }
}}
{{end-eqn}}
as required.
{{qed}}
Category:L-Infinity Norm
7xzv0hgaysk8o37vk6it5ckgxe568hc
Theorem: L-Infinity Norm is Norm

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\map {L^\infty} {X, \Sigma, \mu}$ be the $L^\infty$ vector space on $\struct {X, \Sigma, \mu}$.
Let $\norm \cdot_\infty$ be the $L^\infty$ norm.
Then $\norm \cdot_\infty$ is a norm on $\map {L^\infty} {X, \Sigma, \mu}$.

Proof:
{{MissingLinks}}
Let $\map {\LL^\infty} {X, \Sigma, \mu}$ be the Lebesgue $\infty$-space. 
Let $\sim$ be the $\mu$-almost everywhere equality relation on $\map {\LL^\infty} {X, \Sigma, \mu}$.
Let $\eqclass f \sim \in \map {L^\infty} {X, \Sigma, \mu}$. 
Then, we have by the definition of the $L^\infty$ norm we have: 
:$\norm {\eqclass f \sim}_\infty = \norm f_\infty$
From P-Seminorm is Seminorm, (in the case $p = \infty$) we have: 
:$\norm f_\infty \ge 0$
so:
:$\norm {\eqclass f \sim}_\infty \ge 0$ 
So $\norm \cdot_\infty$ is a map from $\map {L^\infty} {X, \Sigma, \mu}$ to the non-negative real numbers.
It remains to verify the norm axioms.
Theorem: Set with Choice Function is Well-Orderable

Let $S$ be a set.
Let there exist a choice function for $S$.
Then $S$ is well-orderable.

Proof:
Let us define the notation:
:$\map {\PP_{\ne \O} } S := \powerset S \setminus \set \O$
for the power set of $S$ without the empty set.
Let $C: \map {\PP_{\ne \O} } S \to S$ be a choice function for $S$.
Let $x \subseteq S$ be a subset of $S$.
From Subset is Element of Power Set we have:
:$x \subseteq S \iff x \in \powerset S$
Let us define $g: \powerset S \to \powerset S$ as follows:
:$\forall x \in \powerset S: \map g x := \begin {cases} x \cup \paren {\map C {S \setminus x} } & : x \ne S \\ S & : x = S \end {cases}$
where $S \setminus x$ denotes the difference between $S$ and $x$.
We note that:
:$x \ne S \iff S \setminus x \ne \O$
hence $\map C {S \setminus x}$ is always defined in the above.
Thus:
:$\map g S = S$
and for an arbitrary proper subset $x$ of $S$, $\map g x$ adds to $x$ exactly $1$ element of $S$ which is not in $x$.
That is:
:$g$ is a slowly progressing mapping
and:
:$S$ is the unique fixed point of $g$.
Hence $S$ fulfils the assumptions of Set with Slowly Progressing Mapping on Power Set with Self as Fixed Point is Well-Orderable.
The result follows.
{{qed}}
Theorem: P-Seminorm of Function Zero iff A.E. Zero

Let $\struct {X, \Sigma, \mu}$ be a measure space and let $p \in \closedint 1 \infty$.
Let $\map {\LL^p} {X, \Sigma, \mu}$ be the Lebesgue $p$-space. 
Let $f \in \map {\LL^p} {X, \Sigma, \mu}$.
Then:
:$\norm f_p = 0$ {{iff}} $f = 0$ $\mu$-almost everywhere
where $\norm \cdot_p$ is the $p$-seminorm.

Proof:
=== Case 1: $1 \le p < \infty$ ===
We have that: 
:$\norm f_p = 0$ {{iff}} $\norm f_p^p = 0$. 
That is, $\norm f_p = 0$ {{iff}}:
:$\ds \int \size f^p \rd \mu = 0$ 
From Measurable Function Zero A.E. iff Absolute Value has Zero Integral, this is equivalent to:
:$\size f^p = 0$ almost everywhere.
From Pointwise Exponentiation preserves A.E. Equality, we have: 
:$\size f = 0$ almost everywhere.
So:
:$f = 0$ almost everywhere.
{{qed|lemma}}
Theorem: Pointwise Exponentiation preserves A.E. Equality

Let $\struct {X, \Sigma, \mu}$ be a measure space and let $p \in \hointr 0 \infty$. 
Let $f, g : X \to \R$ be real-valued $\Sigma$-measurable functions such that: 
:$\size f = \size g$ $\mu$-almost everywhere. 
Then: 
:$\size f^p = \size g^p$ $\mu$-almost everywhere.

Proof:
Since: 
:$\size f = \size g$ $\mu$-almost everywhere
there exists a $\mu$-null set $N$ such that: 
:if $\size {\map f x} \ne \size {\map g x}$ then $x \in N$. 
If $\size {\map f x} = \size {\map g x}$, then $\size {\map f x}^p = \size {\map g x}^p$.
So by the Rule of Transposition, we have if $\size {\map f x}^p \ne \size {\map g x}^p$ then $\size {\map f x} \ne \size {\map g x}$.
So, if $x \in X$ has $\size {\map f x}^p \ne \size {\map g x}^p$ then $x \in N$. 
So:
:$\size f^p = \size g^p$ $\mu$-almost everywhere.
{{qed}}
Category:Almost-Everywhere Equality Relation
9hv47ng8kq2vf0oe9n5qw8hpur8modg
Theorem: Integral on L-1 Space is Well-Defined

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\map {L^1} {X, \Sigma, \mu}$ be the $L^1$ space of $\struct {X, \Sigma, \mu}$.
Let $E \in \map {L^1} {X, \Sigma, \mu}$. 
Then the $\mu$-integral of $E$ is well-defined.

Proof:
Let $E = \eqclass f \sim$.
We first establish that:
:$\ds \int f \rd \mu$
is a well-understood real number.
We then will show that the $\mu$-integral of $E$ is independent of the choice of representative for $E$.
Since $E \in \map {L^1} {X, \Sigma, \mu}$, we have that $f \in \map {\LL^1} {X, \Sigma, \mu}$. 
Then: 
:$\ds \int \size f \rd \mu < \infty$
So, from Characterization of Integrable Functions, we have: 
:$\ds \int f \rd \mu$ is well-defined and exists as a finite number. 
Suppose now that $\eqclass f \sim = \eqclass g \sim$. 
From Equivalence Class Equivalent Statements:
:$f = g$ $\mu$-almost everywhere
from the definition of the $\mu$-almost everywhere relation.
From A.E. Equal Positive Measurable Functions have Equal Integrals: Corollary 1, we have: 
:$\ds \int f \rd \mu = \int g \rd \mu$
So:
:$\ds \int E \rd \mu$
is independent of the choice of representative for $E$.
{{qed}}
Category:Lp Spaces
9zyxdqgmn3js2kczyz5qx9ih036vr6a
Theorem: Riemann Integral Operator is Continuous Linear Transformation

Let $\struct {C \closedint a b, \norm {\, \cdot \,}_\infty}$ be the normed vector space of real-valued functions continuous on $\closedint a b \subseteq \R$ equipped with the supremum norm.
Let $T : C \closedint a b \to \R$ be the Riemann integral operator:
:$\ds \forall \mathbf x \in C \closedint a b : \map T {\mathbf x} = \int_a^b \map {\mathbf x} t \rd t$
Then $T$ is a continuous mapping.

Proof:
We have that Integral Operator is Linear.
Furthermore:
{{begin-eqn}}
{{eqn | l = \size {T \mathbf x}
      | r = \size {\int_a^b \map {\mathbf x} t \rd t}
}}
{{eqn | o = \le
      | r = \int_a^b \size {\map {\mathbf x} t} \rd t 
}}
{{eqn | o = \le
      | r = \int_a^b \norm {\map {\mathbf x} t}_\infty \rd t
      | c = Definition:Supremum Norm on Space of Continuous on Closed Interval Real-Valued Functions
}}
{{eqn | r = \paren {b - a} \norm {\mathbf x}_\infty 
}}
{{end-eqn}}
By Continuity of Linear Transformation between Normed Vector Spaces, $T$ is continuous.
{{qed}}
Theorem: Zermelo's Well-Ordering Theorem/Converse

Let it be supposed that every set is well-orderable.
Then the Axiom of Choice holds.

Proof:
Let $S$ be an arbitrary set.
By assumption $S$ is well-orderable.
From Well-Orderable Set has Choice Function, $S$ has a choice function.
As $S$ is arbitrary, the result follows.
{{qed}}
Theorem: Zermelo's Well-Ordering Theorem/Converse

Let it be supposed that every set is well-orderable.
Then the Axiom of Choice holds.

Proof:
Let $\FF$ be an arbitrary collection of sets.
By assumption all sets can be well-ordered.
Hence the set $\bigcup \FF$ of all elements of sets contained in $\FF$ is well-ordered by some ordering $\preceq$.
By definition then, every subset of $\ds \bigcup \FF$ has a smallest element under $\preceq$.
Also, note that each set in $\FF$ is a subset of $\bigcup \FF$.
Thus, we may define the choice function $C$:
:$C: \FF \to \bigcup \FF, \map C X = \min X$
where $\min X$ is the smallest element of $X$ under $\preceq$.
{{qed}}
Theorem: L-2 Inner Product is Well-Defined

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\map {\LL^2} {X, \Sigma, \mu}$ be the Lebesgue $2$-space of $\struct {X, \Sigma, \mu}$. 
Let $\sim$ be the $\mu$-almost-everywhere equality relation on $\map {\LL^2} {X, \Sigma, \mu}$.
Let $\map {L^2} {X, \Sigma, \mu}$ be the $L^p$ space on $\struct {X, \Sigma, \mu}$.
Let $E, F \in \map {L^2} {X, \Sigma, \mu}$. 
Then the $L^2$ inner product $\innerprod E F$ is well-defined.

Proof:
Let $E = \eqclass f \sim$ and $F = \eqclass g \sim$ where $\sim$ is the $\mu$-almost everywhere equality relation.
We aim to show that: 
:$\ds \int \paren {f \cdot g} \rd \mu$ 
exists as a real number and is independent of the choice of representatives $f$ and $g$ of $E$ and $F$.
From the definition of the $L^2$ space, we have $f, g \in \map {\LL^2} {X, \Sigma, \mu}$.
From Hölder's Inequality for Integrals, we have:
:$f \cdot g \in \map {\LL^1} {X, \Sigma, \mu}$
So the $\mu$-integral of $f \cdot g$ is well-defined and exists as a real number.
Now suppose that: 
:$\eqclass {f_1} \sim = \eqclass {f_2} \sim = E$
and:
:$\eqclass {g_1} \sim = \eqclass {g_2} \sim = F$
From Equivalence Class Equivalent Statements, we have: 
:$f_1 \sim f_2$
and:
:$g_1 \sim g_2$
That is: 
:$f_1 = f_2$ $\mu$-almost everywhere
and:
:$g_1 = g_2$ $\mu$-almost everywhere.
From Pointwise Multiplication preserves A.E. Equality, we have: 
:$f_1 \cdot g_1 = f_2 \cdot g_2$ $\mu$-almost everywhere.
From A.E. Equal Positive Measurable Functions have Equal Integrals, we have: 
:$\ds \int \paren {f_1 \cdot g_1} \rd \mu = \int \paren {f_2 \cdot g_2} \rd \mu$
as desired.
{{qed}}
Category:Lp Spaces
hzh2vu7gy8a1oo7pk2cy3gvokjw21gl
Theorem: L-2 Inner Product is Inner Product

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\map {\mathcal L^2} {X, \Sigma, \mu}$ be the Lebesgue $2$-space of $\struct {X, \Sigma, \mu}$.
Let $\map {L^2} {X, \Sigma, \mu}$ be the $L^2$ space of $\struct {X, \Sigma, \mu}$.
Let $\innerprod \cdot \cdot$ be the $L^2$ inner product.
Then $\innerprod \cdot \cdot$ is an inner product on $\map {L^2} {X, \Sigma, \mu}$.

Proof:
=== Proof of Symmetry ===
Let $E, F \in \map {L^2} {X, \Sigma, \mu}$.
Let:
:$E = \eqclass f \sim$ 
and:
:$F = \eqclass g \sim$
where $\eqclass f \sim$ and $\eqclass g \sim$ are the equivalence class of $f, g \in \map {\LL^2} {X, \Sigma, \mu}$ under the $\mu$-almost everywhere equality relation. 
Then: 
{{begin-eqn}}
{{eqn	| l = \innerprod E F
		| r = \int \paren {f \cdot g} \rd \mu
        | c = {{Defof|L-2 Inner Product}}
}}
{{eqn	| r = \int \paren {g \cdot f} \rd \mu
		| c = Real Multiplication is Commutative
}}
{{eqn	| r = \innerprod F E
        | c = {{Defof|L-2 Inner Product}}
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Norm on Vector Space is Quasinorm

Let $\struct {R, +, \circ}$ be a division ring with norm $\norm {\,\cdot\,}_R$.
Let $V$ be a vector space over $R$.
Let $\norm \cdot$ be a norm on $V$.
Then $\norm \cdot$ is a quasinorm on $V$.

Proof:
{{improve|In order to make it completely clear what is being proven here, especially with the labels identifying the axioms, I have started a style in which those axioms are repeated at the top of the question: "Recall what we are to prove" or however to word it. This is made easier if the axioms are in a separately transcluded subpage, then all you need to do is use the transclusion mechanism.}}
Theorem: Well-Orderable Set has Choice Function

Let $S$ be a well-orderable set.
Then $S$ has a choice function.

Proof:
Let $\preccurlyeq$ be a well-ordering on $S$.
Let $T \subseteq S$ be an arbitrary non-empty subset of $S$.
As $S$ is a well-ordered set, $T$ has a unique smallest element by $\preccurlyeq$.
Thus, we may define the choice function $C: \powerset S \setminus \set \O \to S$ as:
:$\forall T \in \powerset S \setminus \set \O: \map C T$ is the smallest element of $T$ under $\preccurlyeq$
This is the choice function we require.
{{qed}}
Theorem: Countable Set has Choice Function

Let $S$ be a countable set.
Let $\mathbb S = \powerset S \setminus \set \O$ be the power set of $S$ excluding the empty set $\O$.
Then there exists a  choice function $C$ for $S$:
:$\forall x \in \mathbb S: \map C x \in x$

Proof:
From Countable Set is Well-Orderable, we have that $S$ is a well-orderable set.
The result follows from Well-Orderable Set has Choice Function.
{{qed}}