avewright/proofwiki-math huggingface dataset:
Theorem: Closed Subspace of Lindelöf Space is Lindelöf Space

Let $T = \struct {S, \tau}$ be a Lindelöf space.
Let $C = \struct {H, \tau_H}$ be a subspace of $T$.
Let $C$ be closed in $T$.
Then $\struct {H, \tau}$ is Lindelöf space.
That is, the property of being Lindelöf is weakly hereditary.

Proof:
Let $T$ be a Lindelöf space.
Let $C$ be a closed subspace of $T$.
Let $\UU$ be an open cover of $H$.
We have that $H$ is closed in $T$.
It follows by definition of closed that $H \setminus C$ is open in $T$.
So if we add $S \setminus H$ to $\UU$, we see that:
:$\UU \cup \set {S \setminus H}$ 
is also an open cover of $S$.
As $T$ is compact, there exists a countable subcover of $\UU \cup \set {S \setminus H}$, that is:
:$\VV = \set {U_1, U_2, \ldots}$
This covers $H$ by the fact that it covers $S$.
Suppose $S \setminus H$ is an element of $\VV$.
Then $S \setminus H$ may be removed from $\VV$, and the rest of $\VV$ still covers $H$.
Thus we have a countable subcover of $\UU$ which covers $H$.
Hence $C$ is a Lindelöf space.
{{qed}}
Theorem: Bounded Real-Valued Linear Functional is Real Part of Unique Bounded Complex-Valued Linear Functional

Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space over $\C$.
Let $\struct {X_\R, \norm {\, \cdot \,}_\R}$ be the realification of $X$ equipped with the restricted norm.  
Let $f : X_\R \to \R$ be a bounded linear functional.
Then there exists a unique bounded linear functional $g : X \to \C$ such that: 
:$\map f x = \map \Re {\map g x}$
for each $x \in X$.

Proof:
Let $M > 0$ be such that: 
:$\cmod {\map f x} \le M \norm x$
for each $x \in X$. 
From Linear Functional on Complex Vector Space is Uniquely Determined by Real Part, there exists a unique linear functional $g : X \to \C$ such that: 
:$\map f x = \map \Re {\map g x}$ 
for each $x \in X$, given by: 
:$\map g x = \map f x - i \map f {i x}$ 
for each $x \in X$.
We just need to show that $g$ is bounded. 
Then we have, for each $x \in X$:
{{begin-eqn}}
{{eqn	| l = \cmod {\map g x}^2
		| r = \size {\map f x}^2 + \size {\map f {i x} }^2
}}
{{eqn	| o = \le
		| r = M^2 \norm x^2 + M^2 \norm {i x}^2
}}
{{eqn	| r = 2 M^2 \norm x^2
		| c = {{NormAxiomVector|2}}
}}
{{end-eqn}}
so that: 
:$\cmod {\map g x} \le M \sqrt 2 \norm x$
for each $x \in X$.
So $g$ is a bounded linear functional as required.
{{qed}}
Category:Bounded Linear Functionals
2w53yuj1pyme2ag4azstr0yahkat2ru
Theorem: Hahn-Banach Separation Theorem/Normed Vector Space/Complex Case/Open Convex Set and Convex Set

Let $A \subseteq X$ be an open convex set.
Let $B \subseteq X$ be a convex set disjoint from $A$. 
Then there exists $f \in X^\ast$ and $c \in \R$ such that: 
:$A \subseteq \set {x \in X : \map \Re {\map f x} < c}$
and:
:$B \subseteq \set {x \in X : \map \Re {\map f x} \ge c}$
That is: 
:there exists $f \in X^\ast$ and $c \in \R$ such that $\map \Re {\map f a} < c \le \map \Re {\map f b}$ for each $a \in A$ and $b \in B$.

Proof:
Let $\struct {X_\R, \norm {\, \cdot \,}_\R}$ be the realification of $X$ equipped with the restricted norm.  
Applying Hahn-Banach Separation Theorem: Real Case: Open Convex Set and Convex Set to $\struct {X_\R, \norm {\, \cdot \,}_\R}$, there exists a bounded linear functional $g : X_\R \to \R$ and $c \in \R$ such that: 
:$A \subseteq \set {x \in X : \map g x < c}$
and:
:$B \subseteq \set {x \in X : \map g x \ge c}$
From Bounded Real-Valued Linear Functional is Real Part of Unique Bounded Complex-Valued Linear Functional, there exists $f \in X^\ast$ such that: 
:$\map g x = \map \Re {\map f x}$ 
for each $x \in X$. 
Then $f \in X^\ast$ satisfies: 
:$A \subseteq \set {x \in X : \map \Re {\map f x} < c}$
and:
:$B \subseteq \set {x \in X : \map \Re {\map f x} \ge c}$
as desired.
{{qed}}
Category:Hahn-Banach Separation Theorem
ctzcpbve65xmjvn6qknrz5c6vwniqfx
Theorem: Hahn-Banach Separation Theorem/Normed Vector Space/Complex Case/Compact Convex Set and Closed Convex Set

Let $A$ be a compact convex set.
Let $B$ be a closed convex set disjoint from $A$.
Then there exists $f \in X^\ast$, $c \in \R$ and $\epsilon > 0$ such that: 
:$A \subseteq \set {x \in X : \map \Re {\map f x} \le c - \epsilon}$
and:
:$B \subseteq \set {x \in X : \map \Re {\map f x} \ge c + \epsilon}$
That is: 
:there exists $f \in X^\ast$, $c \in \R$ and $\epsilon > 0$ such that $\map \Re {\map f a} \le c - \epsilon < c + \epsilon \le \map \Re {\map f b}$ for $a \in A$ and $b \in B$.

Proof:
Let $\struct {X_\R, \norm {\, \cdot \,}_\R}$ be the realification of $X$ equipped with the restricted norm.  
Applying Hahn-Banach Separation Theorem: Real Case: Open Convex Set and Convex Set to $\struct {X_\R, \norm {\, \cdot \,}_\R}$, there exists a bounded linear functional $g : X_\R \to \R$, $c \in \R$ and $\epsilon > 0$ such that: 
:$A \subseteq \set {x \in X : \map g x < c - \epsilon}$
and:
:$B \subseteq \set {x \in X : \map g x \ge c + \epsilon}$
From Bounded Real-Valued Linear Functional is Real Part of Unique Bounded Complex-Valued Linear Functional, there exists $f \in X^\ast$ such that: 
:$\map g x = \map \Re {\map f x}$ 
for each $x \in X$. 
Then $f \in X^\ast$ satisfies: 
:$A \subseteq \set {x \in X : \map \Re {\map f x} < c - \epsilon}$
and:
:$B \subseteq \set {x \in X : \map \Re {\map f x} \ge c + \epsilon}$
as desired.
{{qed}}
Category:Hahn-Banach Separation Theorem
9if5hrs0do8335npivl46lyv0lni97t
Theorem: Sum of Consecutive Odd Index Fibonacci Numbers

{{begin-eqn}}
{{eqn | l = F_{2 k - 1} + F_{2 k + 1}
      | r = \phi^{2 k} + \phi^{-2 k}
      | c = 
}}
{{end-eqn}}
where:
:$F_k$ denotes the $k$th Fibonacci number
:$\phi$ denotes the golden mean.

Proof:
{{begin-eqn}}
{{eqn | l = F_{2 k - 1} + F_{2 k + 1}
      | r = \paren {\phi^{2 k} - F_{2 k} \phi } + \paren {\phi^{2 k + 2} - F_{2 k + 2} \phi }
      | c = Fibonacci Number by Golden Mean plus Fibonacci Number of Index One Less
}}
{{eqn | r = \phi^{2 k} + F_{-2 k} \phi + \paren {\phi^{2 k + 2} - F_{2 k + 2} \phi }
      | c = Fibonacci Number with Negative Index
}}
{{eqn | r = \phi^{2 k} + F_{-2 k} \phi + \paren {\paren {F_{2 k + 2} \phi + F_{2 k + 1} } - F_{2 k + 2} \phi }
      | c = Fibonacci Number by Golden Mean plus Fibonacci Number of Index One Less
}}
{{eqn | r = \phi^{2 k} + \paren {F_{-2 k} \phi + F_{-2 k - 1} }
      | c = Fibonacci Number with Negative Index
}}
{{eqn | r = \phi^{2 k} + \phi^{-2 k}
      | c = Fibonacci Number by Golden Mean plus Fibonacci Number of Index One Less
}}
{{end-eqn}}
{{qed}}
Category:Fibonacci Numbers
Category:Golden Mean
q6fya97ce54zvzo3dbvglotwd0y73db
Theorem: Continuous Linear Transformation Algebra has Two-Sided Identity

Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space.
Let $\map {CL} X := \map {CL} {X, X}$ be a continuous linear transformation space.
Let $\struct {\map {CL} X, *}$ be an associative algebra.
Then there exists an identity element $I \in \map {CL} X$ such that:
:$\forall x \in X : \map I x = x$

Proof:
{{ProofWanted}}
{{tidy|the usual}}
Let $X$ be normed vector space over $K$.
Let $\map \LL {X, X}$ denote the set of all linear transformations from $X$ to itself.
Let $\map C {X, X}$ denote the continuous mapping space from $X$ to itself.
Suppose:
:$\map {CL} X := \map {CL} {X, X}$
Since $\struct {\map {CL} X, *}$ is an associative algebra, by definition of the continuous linear transformation space from $X$ to itself, $\map {CL} {X, X}$, we have:
:$\map {CL} {X, X} := \map C {X, X} \cap \map \LL {X, X}$
By Identity Mapping is Continuous, we have that $I \in \map C {X, X}$.
By Identity Mapping on Normed Vector Space is Bounded Linear Operator, we have that $I \in \map \LL {X, X}$.
Hence $I \in \map {CL} X $ by definition of identity element.
Theorem: Continuous Linear Transformation Algebra with Supremum Operator Norm is Normed Algebra

Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space.
Let $\map {CL} X := \map {CL} {X, X}$ be a continuous linear transformation space.
Let $\struct {\map {CL} X, *}$ be an associative algebra.
Let $\norm {\, \cdot \,}$ be the supremum operator norm.
Then $\struct {\struct {\map {CL} X, *}, \norm {\, \cdot \,}}$ is a normed algebra.

Proof:
We need to show:
$\norm {a \ast b} \le \norm a \norm b$
{{questionable|Is this really true for any associative bilinear $\ast$? }}
{{ProofWanted}}
Theorem: Equation of Wavefront of Plane Wave/Direction Cosine Form

Let $\phi$ be a plane wave.
Let an arbitrary wavefront of $\phi$ be denoted $P$.
Let the direction of propagation of $\phi$ be expressed as:
:$x : y : z = l : m : n$
where $l$, $m$ and $n$ are the direction cosines of the normal to $P$.
{{explain|The notation needs to be explained. This will be done on the Definition:Direction Cosines page. $3$D analytic / coordinate geometry still woefully lacking on {{ProofWiki}}.}}
Then:
:$l x + m y + n z = K$
where $K$ is constant for a given plane wave $\phi$.

Proof:
{{ProofWanted|More background needed on $3$D analytic / coordinate geometry. I need to crack on with that.}}
Theorem: Equation of Plane Wave/Direction Cosine Form

Let $\phi$ be a plane wave propagated with velocity $c$.
Let the direction of propagation of $\phi$ be expressed as:
:$x : y : z = l : m : n$
where $l$, $m$ and $n$ are the '''direction cosines''' of the normal to $P$.
Then $\phi$ can be expressed as:
:$\map \phi {x, y, z, t} = \map f {l x + m y + n z - c t}$

Proof:
By Equation of Wavefront of Plane Wave, the equation of the wavefront of $\phi$ is given by:
:$l x + m y + n z = K$
Hence it is clear that:
:$\map \phi {x, y, z, t} = \map f {l x + m y + n z - c t}$
is a function which fulfils all the requirements to be a plane wave.
{{handwaving|"It is clear that"}}
Hence $\phi$ as defined represents a plane wave propagated with velocity $c$ in the direction given.
Theorem: T3 Lindelöf Space is T4

Let $T = \struct {S, \tau}$ be a $T_3$ Lindelöf topological space.
Then $T$ is a $T_4$ space.

Proof:
Let $A$ and $B$ be disjoint closed subsets of $T$.
Let $\UU = \set {U \in \tau : U^- \cap B = \O}$.
From Characterization of T3 Space:
:$\forall a \in A : \exists U_a \in \tau: a \in U_a : U_a^- \cap B = \O$
By definition of open cover:
:$\UU$ is an open cover of $A$
From Closed Subspace of Lindelöf Space is Lindelöf Space:
:$\struct {A, \tau_A}$ is a Lindelöf subspace
where $\tau_A$ is the subspace topology on $A$.
By definition of Lindelöf space:
:there exists a countable subcover $\family {U_n}_{n \mathop \in \N}$ of $\UU$ for $A$
Let $\VV = \set {V \in \tau : V^- \cap A = \O}$.
Similar to $A$ above, there exists a countable subcover $\family {V_n}_{n \mathop \in \N}$ of $\VV$ for $B$.
From Countable Open Covers Condition for Separated Sets:
:$A$ and $B$ can be separated in $T$
By definition of separated:
:$\exists U, V \in \tau : A \subseteq U, B \subseteq V, U \cap V = \O$.
Since $A$ and $B$ were arbitrary:
:$\forall A, B \in \map \complement \tau, A \cap B = \O: \exists U, V \in \tau: A \subseteq U, B \subseteq V, U \cap V = \O$ 
Hence, by definition, $T$ is a $T_4$ space.
{{qed}}
Theorem: T3 Lindelöf Space is T4

Let $T = \struct {S, \tau}$ be a $T_3$ Lindelöf topological space.
Then $T$ is a $T_4$ space.

Proof:
From $T_3$ Lindelöf Space is Fully $T_4$:
:$T$ is a fully $T_4$ space.
From Fully $T_4$ Space is $T_4$:
:$T$ is a $T_4$ space.
{{qed}}
Theorem: T3 Lindelöf Space is Fully T4

Let $T = \struct {S, \tau}$ be a $T_3$ Lindelöf topological space.
Then $T$ is a fully $T_4$ space.

Proof:
From $T_3$ Lindelöf Space is Paracompact:
:$T$ is a paracompact space
From $T_3$ Space is Fully $T_4$ iff Paracompact:
:$T$ is a fully $T_4$ space
{{qed}}
Theorem: Mazur's Theorem

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,} } $ be a normed vector space over $\GF$ with weak topology $w$. 
Let $C \subseteq X$ be a convex subset of $X$. 
Then: 
:$\map {\cl_w} C = \map \cl C$
where $\cl_w$ denotes the weak closure.

Proof:
From Topological Closure in Coarser Topology is Larger: 
:$\map \cl C \subseteq \map {\cl_w} C$
Now let $x \not \in \map \cl C$. 
From Finite Topological Space is Compact, $\set x$ is compact. 
Applying: 
:Hahn-Banach Separation Theorem: Compact Convex Set and Closed Convex Set (Real Case) if $\GF = \R$
:Hahn-Banach Separation Theorem: Compact Convex Set and Closed Convex Set (Complex Case) if $\GF = \C$
for $A = \set x$ and $B = \map \cl C$, there exists a bounded linear functional $f : X \to \GF$ such that: 
:$\ds \map \Re {\map f x} < \inf_{y \in \map \cl C} \map \Re {\map f y}$
Now let $\alpha \in \R$ be such that: 
:$\ds \map \Re {\map f x} < \alpha < \inf_{y \in \map \cl C} \map \Re {\map f y}$
Consider: 
:$E = \set {x \in X : \map \Re {\map f x} \ge \alpha}$ 
We know that $C \subseteq E$. 
From Characterization of Continuity of Linear Functional in Weak Topology, $f : \struct {X, w} \to \GF$ is continuous.
So, by Real and Imaginary Part Projections are Continuous and Composite of Continuous Mappings is Continuous, $\map \Re f : \struct {X, w} \to \R$ is continuous.
From Continuity Defined from Closed Sets, $E$ is then weakly closed.
From Topological Closure of Subset is Subset of Topological Closure, $\map {\cl_w} C \subseteq \map {\cl_w} E$.
From Set is Closed iff Equals Topological Closure, we have $\map {\cl_w} E = E$.
So: 
:$\map {\cl_w} C \subseteq E = \set {x \in X : \map \Re {\map f x} \ge \alpha}$ 
Since $\map \Re {\map f x} < \alpha$, we have $x \in X \setminus \map {\cl_w} C$. 
So we obtain: 
:$\map {\cl_w} C \subseteq \map \cl C$
and so: 
:$\map {\cl_w} C = \map \cl C$
{{qed}}
{{explain|need to identify which Mazur this is. Probably Stan.}}
Category:Mazur's Theorem
Category:Weak Topologies on Topological Vector Spaces
Category:Convex Sets (Vector Spaces)
Category:Weakly Closed Sets
ha94clne4wn9zekxaibeoadglav1tm0
Theorem: Open Ball in Infinite-Dimensional Normed Vector Space is not Weakly Open

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space over $\GF$ with weak topology $w$.
Suppose that $\dim X = \infty$. 
Let $\map {B_r} x$ be the open ball in $X$ with radius $r > 0$ and center $x \in X$. 
Then $\map {B_r} x$ is not weakly open.

Proof:
From Translation of Open Set in Normed Vector Space is Open and Dilation of Open Set in Normed Vector Space is Open, it suffices to show that $\map {B_1} 0$ is not weakly open. 
{{AimForCont}} that $\map {B_1} 0$ is weakly open.
From Initial Topology on Vector Space Generated by Linear Functionals is Locally Convex, $\struct {X, w}$ is a locally convex space induced by: 
:$\set {p_f : f \in X^\ast}$
with $p_f : X \to \hointr 0 \infty$ defined by: 
:$\map {p_f} x = \cmod {\map f x}$ 
for each $x \in X$. 
From Open Sets in Standard Topology of Locally Convex Space, there exists $f_1, \ldots, f_n \in X^\ast$ and $\epsilon > 0$ such that: 
:$\set {y \in X : \cmod {\map {f_k} y} < \epsilon \text { for each } 1 \le k \le n} \subseteq \map {B_1} 0$
Define $T : X \to \GF^n$ by: 
:$T x = \tuple {\map {f_1} x, \map {f_2} x, \ldots, \map {f_n} x}$
for each $x \in X$. 
Suppose that: 
:$\ds \bigcap_{i \mathop = 1}^n \ker f_i = \set {\mathbf 0_X}$
Then $\ker T = \set {\mathbf 0_X}$.
So $T$ is injective, and is therefore a bijection onto $T \sqbrk X$.
So $T$ is a vector space isomorphism between $X$ and $T \sqbrk X$. 
So we have: 
:$\dim X = \dim T \sqbrk X$ 
From Dimension of Image of Vector Space under Linear Transformation is Bounded Above by Dimension of Vector Space, we have: 
:$\dim T \sqbrk X \le n$
and so $\dim X \le n < \infty$, contrary to our assumption that $\dim X = \infty$.
So we must have: 
:$\ds \bigcap_{i \mathop = 1}^n \ker f_i \ne \set {\mathbf 0_X}$
Pick $x \ne \mathbf 0_X$ with: 
:$\ds x \in \bigcap_{i \mathop = 1}^n \ker f_i$
Then for each $\lambda \in \GF$, we have $\cmod {\map {f_i} {\lambda x} } = \cmod \lambda \cmod {\map {f_i} x} = 0 < \epsilon$ for each $1 \le i \le n$.
So $\lambda x \in \map {B_1} 0$ for each $\lambda \in \GF$. 
But then, for each $\lambda \in \GF \setminus \set 0$, we have: 
:$\ds \norm x < \frac 1 {\cmod \lambda}$ 
Taking $\lambda \to \infty$ we obtain $\norm x = 0$.
Hence $x = \mathbf 0_X$ from {{NormAxiomVector|1}}, contrary to our assumption that $x \ne \mathbf 0_X$.
{{qed}}
Category:Open Balls
Category:Weakly Open Sets
t7isghzycwmbw0xa2eph9d9jv1h27at
Theorem: Equation of Plane Wave is Particular Solution of Wave Equation/Direction Cosine Form

Let $\phi$ be a plane wave propagated with velocity $c$ in a Cartesian $3$-space.
Let $\phi$ be expressed as:
:$\map \phi {x, y, z, t} = \map f {l x + m y + n z - c t}$
where $l$, $m$ and $n$ are the direction cosines of the normal to $P$.
Then $\phi$ satisfies the wave equation.

Proof:
The wave equation is expressible as:
:$\dfrac 1 {c^2} \dfrac {\partial^2 \phi} {\partial t^2} = \dfrac {\partial^2 \phi} {\partial x^2} + \dfrac {\partial^2 \phi} {\partial y^2} + \dfrac {\partial^2 \phi} {\partial z^2}$
Let $u = l x + m y + n z - c t$.
The second partial derivatives {{WRT|Differentiation}} $x$ are as follows:
{{begin-eqn}}
{{eqn | l = \frac {\partial^2 \phi} {\partial x^2}
      | r = \frac \partial {\partial x} \paren {\frac {\partial \phi} {\partial x} }
}}
{{eqn | r = \frac \partial {\partial x} \paren {\frac {\partial \phi} {\partial u} \frac {\partial u} {\partial x} }
      | c = Chain Rule for Partial Derivatives
}}
{{eqn | r = l \frac \partial {\partial x} \paren {\frac {\partial \phi} {\partial u} }
      | c = Derivative of Constant Multiple
}}
{{eqn | r = l \frac {\partial^2 \phi} {\partial u^2} \frac {\partial u} {\partial x}
      | c = Chain Rule for Partial Derivatives
}}
{{eqn | r = l^2 \frac {\partial^2 \phi} {\partial u^2}
}}
{{end-eqn}}
By {{mutatis}}, the results for the other partial derivatives are as follows:
:$\dfrac {\partial^2 \phi} {\partial y^2} = m^2 \dfrac {\partial^2 \phi} {\partial u^2}$
:$\dfrac {\partial^2 \phi} {\partial z^2} = n^2 \dfrac {\partial^2 \phi} {\partial u^2}$
:$\dfrac {\partial^2 \phi} {\partial t^2} = c^2 \dfrac {\partial^2 \phi} {\partial u^2}$
So, on the {{LHS}} of the wave equation, we have:
{{begin-eqn}}
{{eqn | l = \frac 1 {c^2} \frac {\partial^2 \phi} {\partial t^2}
      | r = \frac 1 {c^2} \paren {c^2 \frac {\partial^2 \phi} {\partial u^2} }
}}
{{eqn | r = \frac {\partial^2 \phi} {\partial u^2}
}}
{{end-eqn}}
On the {{RHS}}, we have:
{{begin-eqn}}
{{eqn | l = \frac {\partial^2 \phi} {\partial x^2} + \frac {\partial^2 \phi} {\partial y^2} + \frac {\partial^2 \phi} {\partial z^2}
      | r = \frac {\partial^2 \phi} {\partial u^2} \paren {l^2 + m^2 + n^2}
}}
{{eqn | r = \frac {\partial^2 \phi} {\partial u^2}
      | c = Relation between Direction Cosines
}}
{{end-eqn}}
{{qed}}
Theorem: Continuous Linear Transformation Space as Banach Algebra

Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space.
Let $\map {CL} X := \map {CL} {X, X}$ be a continuous linear transformation space.
Let $*_X : X \times X \to X$ and $* : \map {CL} X \times \map {CL} X \to \map {CL} X$ be bilinear mappings.
Suppose $\struct {\struct {X, \norm {\, \cdot \,}_X}, *_X}$ is a Banach algebra.
Let $\norm {\, \cdot \,}$ be the supremum operator norm.
Then $\struct {\struct {\map {CL} X, \norm {\, \cdot \,}}, *}$ is a Banach algebra.

Proof:
{{questionable|Please review the source. This cannot be true for any $*$, I believe this should be a composition. Mapping everything to zero is a counterexample.}}
{{ProofWanted}}
Theorem: Set of Points for which Seminorm is Zero is Vector Subspace

Let $\GF \in \set {\R, \C}$. 
Let $X$ be a vector space over $\GF$.
Let $p$ be a seminorm on $X$.
Let:
:$U = \set {x \in X : \map p x = 0}$
Then $U$ is a vector subspace of $X$.

Proof:
From Seminorm Maps Zero Vector to Zero, $\map p {\mathbf 0_X} = 0$.
So $\mathbf 0_X \in U$ and in particular $U \ne \O$.
So we look to apply One-Step Vector Subspace Test.
Let $x, y \in U$ and $\lambda, \mu \in \GF$.
Then we have: 
{{begin-eqn}}
{{eqn	| l = \map p {\lambda x + \mu y}
		| o = \le
		| r = \map p {\lambda x} + \map p {\mu y}
		| c = {{SeminormAxiom|3}}
}}
{{eqn	| r = \cmod \lambda \map p x + \cmod \mu \map p y
		| c = {{SeminormAxiom|2}}
}}
{{eqn	| r = 0
		| c = since $x, y \in U$
}}
{{end-eqn}}
Since $\map p {\lambda x + \mu y} \ge 0$, so:
:$\map p {\lambda x + \mu y} = 0$
so $\lambda x + \mu y \in U$.
By One-Step Vector Subspace Test, we have that $U$ is a vector subspace of $X$. 
{{qed}}
Theorem: Open Ball with respect to Seminorm is Convex, Balanced and Absorbing

Let $\GF \in \set {\R, \C}$. 
Let $X$ be a vector space over $\GF$.
Let $p$ be a seminorm on $X$.
Let $d_p$ be the pseudometric induced by $p$.
Let $B$ be the open unit ball in $\struct {X, d_p}$. 
That is: 
:$B = \set {x \in X : \map p x < 1}$
Then $B$ is convex, balanced and absorbing.

Proof:
=== Proof that $B$ is convex ===
Let $t \in \closedint 0 1$ and $x, y \in B$. 
Then:
{{begin-eqn}}
{{eqn	| l = \map p {t x + \paren {1 - t} y}
		| o = \le
		| r = t \map p x + \paren {1 - t} \map p y
		| c = {{SeminormAxiom|2}}, {{SeminormAxiom|3}}
}}
{{eqn	| o = <
		| r = t + \paren {1 - t}
}}
{{eqn	| r = 1
}}
{{end-eqn}}
so: 
:$t x + \paren {1 - t} y \in B$. 
{{qed|lemma}}
Theorem: Closed Unit Ball in Normed Vector Space is Weakly Closed

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space over $\GF$.
Let $B^-$ be the closed unit ball in $\struct {X, \norm {\, \cdot \,} }$.
Then $B^-$ is weakly closed.

Proof:
From Closed Unit Ball is Convex Set, $B^-$ is convex.
From Closed Ball is Closed, $B^-$ is $\norm {\, \cdot \,}$-closed. 
From Mazur's Theorem: Corollary, we can conclude that $B^-$ is weakly closed.
{{qed}}
Category:Weakly Closed Sets
Category:Closed Balls
Category:Normed Vector Spaces
0z00xz69xza14gdzpcmaqakznsdyxz4
Theorem: Upper Darboux Integral Never Smaller than Lower Darboux Integral

Let $\closedint a b$ be a closed real interval.
Let $f: \closedint a b \to \R$ be a bounded real function.
The lower Darboux integral of $f$ over $\closedint a b$ is less than or equal to the upper Darboux integral of $f$ over the same bounds.
That is:
:$\ds \underline {\int_a^b} \map f x \rd x \le \overline {\int_a^b} \map f x \rd x$

Proof:
Let the value of the lower Darboux integral be $L$, and the value of the upper Darboux integral be $U$.
{{AimForCont}}, suppose $L > U$.
Then $\epsilon = \dfrac {L - U} 2$ is positive.
By the definitions of lower Darboux integral and upper Darboux integral:
:$\ds \sup_P \map L P > \inf_P \map U P$
where $P$ ranges over all subdivisions of $\closedint a b$, and $\map L P$ and $\map U P$ are the lower Darboux sum and upper Darboux sum, respectively.
By the Characterizing Property of Supremum of Subset of Real Numbers, there exists are partition $P_L$ such that:
:$\map L {P_L} > L - \epsilon = \dfrac {L + U} 2$
Likewise, by the Characterizing Property of Infimum of Subset of Real Numbers, there is a partition $P_U$ such that:
:$\map U {P_U} < U + \epsilon = \dfrac {U + L} 2 $
Thus:
:$\map U {P_U} < \map L {P_L}$
But, by Upper Sum Never Smaller than Lower Sum for any Pair of Subdivisions, this is a contradiction.
Therefore, $L \le U$.
{{qed}}
Category:Lower Darboux Integral
Category:Upper Darboux Integral
Category:Integral Calculus
t5m4bvyqo5smne6mslqfbokp1qhx00a
Theorem: Minkowski Functional of Convex Absorbing Set is Finite

Let $\GF \in \set {\R, \C}$. 
Let $X$ be a vector space over $\GF$.
Let $A \subseteq X$ be a convex absorbing set. 
Let $\mu_A$ be the Minkowski functional of $A$. 
Then for each $x \in X$, $\map {\mu_A} x$ is a finite extended real number.
That is:
:$\forall x \in X: \map {\mu_A} x < \infty$

Proof:
Let $x \in X$. 
From Characterization of Convex Absorbing Set in Vector Space:
:$\exists t \in \R_{>0}: x \in t A$
where $t A$ denotes the dilation of $A$ by $t$.
Then: 
:$x \in t^{-1} C$
so that:
:$t \in \set {t > 0 : t^{-1} x \in A}$
Then, we have:
:$\map {\mu_A} x \le t < \infty$ 
{{qed}}
Category:Minkowski Functionals
cnpbkhwmq9fvqmnh2d2qnj4ukuayudf