avewright/proofwiki-math huggingface dataset:
Theorem: Hahn-Banach Separation Theorem/Hausdorff Locally Convex Space/Real 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 f x < c}$
and:
:$B \subseteq \set {x \in X : \map f x \ge c}$
That is: 
:there exists $f \in X^\ast$ and $c \in \R$ such that $\map f a < c \le \map f b$ for each $a \in A$ and $b \in B$.

Proof:
Fix $a_0 \in A$ and $b_0 \in B$. 
From Sum of Set and Open Set in Topological Vector Space is Open, we have: 
:$A - B$ is open. 
From Translation of Open Set in Topological Vector Space is Open, we have: 
:$A - B + \paren {b_0 - a_0}$ is open.
Note that since $A \cap B = \O$, we have $0 \notin A - B$. 
Hence $b_0 - a_0 \notin A - B + \paren {b_0 - a_0}$.
From {{Corollary|Sum of Convex Sets in Vector Space is Convex}}, we have that $A - B$ is convex.
From Translation of Convex Set in Vector Space is Convex, we have that $A - B + \paren {b_0 - a_0}$ is convex.
Applying Open Convex Set in Hausdorff Locally Convex Space is Separated from Points outside Set by Continuous Linear Functional, there exists $f \in X^\ast$ such that: 
:$\map f v < \map f {b_0 - a_0}$
for all $v \in A - B + \paren {b_0 - a_0}$.
That is: 
:$\map f {a - b + b_0 - a_0} < \map f {b_0 - a_0}$
for each $a \in A$ and $b \in B$. 
Since $f$ is linear, we have: 
:$\map f a < \map f b$
for each $a \in A$ and $b \in B$.
Then we have: 
:$\map f {a_0} < \map f b$
for all $b \in B$. 
Hence: 
:$\ds \inf_{b \mathop \in B} \map f b > -\infty$
Let:
:$\ds c = \inf_{b \mathop \in B} \map f b$
Then, we have: 
:$\map f a \le c \le \map f b$ 
It remains to show that $\map f a < c$ for each $a \in A$.
Let $a \in A$.
Since $A$ is open, there exists an open neighborhood $V_x$ of ${\mathbf 0}_X$ such that $x + V_x$ is an open neighborhood of $x$ in $A$.
Now, since we have: 
:$\map f {a_0} < \map f b$
for each $b \in B$, we in particular have that $f$ is not constant ${\mathbf 0}_X$. 
Hence there exists $v \in X$ such that: 
:$\map f v \ne 0$
Replacing $v$ by $-v$ if necessary, suppose that: 
:$\map f v > 0$
From Multiple of Vector in Topological Vector Space Converges, we have: 
:$\dfrac v n \to {\mathbf 0}_X$ as $n \to \infty$ 
So for some $N \in \N$, we have: 
:$\dfrac v N \in V_x$
by the definition of a convergent sequence.
Set:
:$v' = \dfrac v N$
Then we have $\map f {v'} > 0$ and $x + v' \in A$.
We therefore have: 
{{begin-eqn}}
{{eqn	| l = \map f a
		| o = <
		| r = \map f a + \map f {v'}
}}
{{eqn	| r = \map f {a + v'}
		| c = {{Defof|Linear Functional}}
}}
{{eqn	| o = \le
		| r = c
}}
{{end-eqn}}
In particular, $\map f a < c$ for each $a \in A$.
Hence we have found $f \in X^\ast$ such that: 
:$\map f a < c \le \map f b$ for each $a \in A$ and $b \in B$. 
{{qed}}
Category:Hahn-Banach Separation Theorem
trmm7o25p13qdupauon9y26hpwdco3z
Theorem: Minkowski Functional of Symmetric Convex Absorbing Set in Real Vector Space is Seminorm

Let $X$ be a vector space over $\R$.
Let $A \subseteq X$ be a set that is symmetric, convex and absorbing.
Let $\mu_A$ be the Minkowski functional of $A$. 
Then $\mu_A$ is a seminorm.

Proof:
From Minkowski Functional of Convex Absorbing Set is Positive Homogeneous, $\mu_A$ is a sublinear functional.
Hence we have: 
:$\map {\mu_A} {x + y} \le \map {\mu_A} x + \map {\mu_A} y$ for all $x, y \in X$
and hence {{SeminormAxiom|3}}.
We also have: 
:$\map {\mu_A} {r x} = r \map {\mu_A} x$ for all $r \ge 0$ and $x \in X$.
To establish {{SeminormAxiom|2}}, it remains to show that: 
:$\map {\mu_A} {r x} = \size r \map {\mu_A} x$ for all $r < 0$ and $x \in X$. 
For this we first show that: 
:$\map {\mu_A} {-x} = \map {\mu_A} x$ for all $x \in X$.
Since $A$ is symmetric, we have $A = -A$. 
Then we have: 
{{begin-eqn}}
{{eqn	| l = \map {\mu_A} x
		| r = \inf \set {t > 0 : x \in t A}
		| c = {{Defof|Minkowski Functional of Convex Absorbing Set}}
}}
{{eqn	| r = \inf \set {t > 0 : x \in -t A}
		| c = since $A = -A$
}}
{{eqn	| r = \inf \set {t > 0 : -x \in t A}
}}
{{eqn	| r = \map {\mu_A} {-x}
}}
{{end-eqn}}
Now for $r < 0$ and $x \in X$ we have:
{{begin-eqn}}
{{eqn	| l = \map {\mu_A} {r x}
		| r = \map {\mu_A} {-\size r x}
}}
{{eqn	| r = \size r \map {\mu_A} {-x}
		| c = {{Defof|Sublinear Functional}}
}}
{{eqn	| r = \size r \map {\mu_A} x
}}
{{end-eqn}}
showing {{SeminormAxiom|2}}.
{{qed}}
Category:Minkowski Functionals
Category:Seminorms
6c2lb6pgegts97wg35a1yzpjf2t0xp3
Theorem: Intersection of Balanced Sets in Vector Space is Balanced

Let $\Bbb F \in \set {\R, \C}$.
Let $X$ be a vector space over $\Bbb F$. 
Let $\sequence {E_\alpha}_{\alpha \mathop \in I}$ be an $I$-indexed family of balanced subsets of $X$.
Then:
:$\ds E = \bigcap_{\alpha \mathop \in I} E_\alpha$ is balanced.

Proof:
Let $x \in E$.
Then $x \in E_\alpha$ for all $\alpha \in I$. 
Let $\lambda \in \Bbb F$ have $\cmod \lambda \le 1$.
Since $E_\alpha$ is balanced for each $\alpha \in I$, we have $\lambda x \in E_\alpha$ for each $\alpha \in I$.
So $\lambda x \in E$.
{{qed}}
Category:Balanced Sets
Category:Set Intersection
d0l3abt8mcjjpg1gjkxmdeg0larinls
Theorem: Balanced Set in Vector Space is Symmetric

Let $\GF \in \set {\R, \C}$. 
Let $X$ be a vector space over $\GF$. 
Let $C \subseteq X$ be a balanced set. 
Then $C$ is symmetric.

Proof:
Since $C$ is balanced, we have: 
:$s C \subseteq C$ for all $s \in \C$ with $\cmod s \le 1$.
So in particular, setting $s = -1$:
:$-C \subseteq C$ 
So $C$ is symmetric.
Category:Symmetric Subsets of Vector Spaces
Category:Balanced Sets
mzh45stgo04j1jjdjhc9k6epfl93nun
Theorem: Minkowski Functional of Balanced Convex Absorbing Set in Vector Space is Seminorm

Let $\GF \in \set {\R, \C}$. 
Let $X$ be a vector space over $\GF$. 
Let $A \subseteq X$ be a set that is balanced, convex and absorbing.
Let $\mu_A$ be the Minkowski functional of $A$. 
Then $\mu_A$ is a seminorm.

Proof:
=== Case 1: $\GF = \R$ ===
From Balanced Set in Vector Space is Symmetric, $A$ is symmetric.
Hence by Minkowski Functional of Symmetric Convex Absorbing Set in Real Vector Space is Seminorm, $\mu_A$ is a seminorm in this case.
{{qed|lemma}}
Theorem: Characterization of Paracompactness in T3 Space/Lemma 17

:$\forall n \in \N_{> 0} : \AA_n$ is a discrete set of subsets.

Proof:
=== Lemma 16 ===
{{:Characterization of Paracompactness in T3 Space/Lemma 16}}
Let $n \in \N_{> 0}$.
Let $x \in X$.
Theorem: Continuous Mappings into Hausdorff Space coinciding on Everywhere Dense Set coincide

Let $\struct {X, \tau_X}$ be a topological space.
Let $\struct {Y, \tau_Y}$ be a Hausdorff space. 
Let $D$ be an everywhere dense subset of $X$. 
Let $f : X \to Y$ and $g : X \to Y$ be continuous mappings such that: 
:$\map f x = \map g x$ for all $x \in D$.
Then: 
:$\map f x = \map g x$ for all $x \in X$.

Proof:
{{AimForCont}} that there exists $x_0 \in X$ such that $\map f {x_0} \ne \map g {x_0}$.
Since $\struct {Y, \tau_Y}$ is Hausdorff, there exists an open neighborhood $U$ of $\map f {x_0}$ and an open neighborhood $V$ of $\map g {x_0}$ such that: 
:$U \cap V = \O$
We then have: 
:$x_0 \in f^{-1} \sqbrk U \cap g^{-1} \sqbrk V$
Let:
:$W = f^{-1} \sqbrk U \cap g^{-1} \sqbrk V$
Since $f$ and $g$ are continuous, $W$ is the intersection of two open sets in $\struct {X, \tau_X}$. 
So $W$ is open in $\struct {X, \tau_X}$ by the definition of a topology. 
Since $D$ is an everywhere dense subset of $X$, there therefore exists $y \in D \cap W$.
Then we have $\map f y \in U$ and $\map g y \in V$.
Since $U \cap V = \O$, it follows that $\map f y \ne \map g y$. 
But we also have $y \in D$, and {{hypothesis}} we have that $\map f x = \map g x$ for all $x \in D$.
Hence we have a contradiction.
We conclude: 
:$\map f x = \map g x$ for all $x \in X$.
{{qed}}
Theorem: Continuous Mappings into Hausdorff Space coinciding on Everywhere Dense Set coincide

Let $\struct {X, \tau_X}$ be a topological space.
Let $\struct {Y, \tau_Y}$ be a Hausdorff space. 
Let $D$ be an everywhere dense subset of $X$. 
Let $f : X \to Y$ and $g : X \to Y$ be continuous mappings such that: 
:$\map f x = \map g x$ for all $x \in D$.
Then: 
:$\map f x = \map g x$ for all $x \in X$.

Proof:
Let $x \in X$.
Since $D$ is everywhere dense, we have that $x \in \map \cl D$, where $\map \cl D$ is the topological closure of $D$. 
By Point in Set Closure iff Limit of Net, there exists a directed set $\struct {\Lambda, \preceq}$ and a net $\family {x_\lambda}_{\lambda \in \Lambda}$ in $D$ converging to $x$.
From Characterization of Continuity in terms of Nets, we have that the nets $\family {\map f {x_\lambda} }_{\lambda \in \Lambda}$ and $\family {\map g {x_\lambda} }_{\lambda \in \Lambda}$ converge to $\map f x$ and $\map g x$ in $\struct {Y, \tau_Y}$ respectively.
By hypothesis, we have: 
:$\map f {x_\lambda} = \map g {x_\lambda}$ for each $\lambda \in \Lambda$.
So we have that $\family {\map f {x_\lambda} }_{\lambda \in \Lambda}$ converges to both $\map f x$ and $\map g x$.
Since $\struct {Y, \tau_Y}$ is Hausdorff, from Characterization of Hausdorff Property in terms of Nets we obtain that $\map f x = \map g x$, hence the demand.
{{qed}}
Theorem: Characterization of Paracompactness in T3 Space/Lemma 18

:$\AA$ is a cover of $X$

Proof:
Let $x \in X$.
We have {{hypothesis}}:
:$\forall n \in \N_{>0} : \Delta_X \subseteq U_n$
By definition of image:
:$\forall n \in \N_{>0} : x \in \map {U_n} x$
Let:
:$y = \min \set{z \in X : x \in \ds \bigcup_{n \in N} \map {U_n} z}$
with respect to the well-ordering $\preccurlyeq$.
By choice of $y$
:$\exists n \in \N_{>0}$: $x \in \map {U_n} y$ 
and 
:$\forall z \preccurlyeq y, z \ne y : x \notin \map {U_{n + 1}} z$
By definition of set union:
:$x \notin \ds \bigcup_{z \preccurlyeq y, z \ne y} \map {U_{n + 1}} z$
By definition of set difference
:$x \in \map {U_n} y \setminus \ds \bigcup_{z \preccurlyeq y, z \ne y} \map {U_{n + 1}} z$
That is:
:$x \in \map {A_n} y$
Since $x$ was arbitrary:
:$\forall x \in X : \exists y \in X, n \in \N_{>0} : x \in \map {A_n} y$
Hence $\AA$ is a cover of $X$ by definition.
{{qed}}
Category:Characterization of Paracompactness in T3 Space
dufcugd1o7yqmcg962i443h5uf0s7ue
Theorem: Product of Directed Sets is Directed Set

Let $\struct {\Lambda_1, \preceq_1}$ and $\struct {\Lambda_2, \preceq_2}$ be directed sets. 
Define a relation $\sqsubseteq$ on $\Lambda_1 \times \Lambda_2$ by: 
:$\tuple {\lambda_1, \lambda_2} \sqsubseteq \tuple {\mu_1, \mu_2}$
for $\tuple {\lambda_1, \lambda_2}, \tuple {\mu_1, \mu_2} \in \Lambda_1 \times \Lambda_2$ {{iff}}:
:$\lambda_1 \preceq_1 \mu_1$ and $\lambda_2 \preceq_2 \mu_2$
Then $\struct {\Lambda_1 \times \Lambda_2, \sqsubseteq}$ is a directed set.

Proof:
From Product of Preordered Sets is Preordered, $\sqsubseteq$ is a preordering.
We now show that $\sqsubseteq$ is directed. 
Let $\tuple {\lambda_1, \mu_1}, \tuple {\lambda_2, \mu_2} \in \Lambda_1 \times \Lambda_2$.
Then since $\preceq_1$ is directed, there exists $\lambda \in \Lambda_1$ such that: 
:$\lambda_1 \preceq_1 \lambda$ and $\lambda_2 \preceq_2 \lambda$.
Since $\preceq_2$ is directed, there exists $\mu \in \Lambda_2$ such that:
:$\mu_1 \preceq_2 \mu$ and $\mu_2 \preceq_2 \mu$.
So we have: 
:$\tuple {\lambda_1, \mu_1} \sqsubseteq \tuple {\lambda, \mu}$
and:
:$\tuple {\lambda_2, \mu_2} \sqsubseteq \tuple {\lambda, \mu}$
So $\tuple {\Lambda_1 \times \Lambda_2, \sqsubseteq}$ is a directed set.
{{qed}}
Category:Directed Preorderings
q2oxsungxyy1jdnb2j5dtwodrdfgo99
Theorem: Characterization of Convergent Net in Metric Space

Let $\struct {X, d}$ be a metric space.
Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ be a net in $X$. 
Let $x \in X$. 
Then $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ converges in $\struct {X, d}$ {{iff}}:
:for each $\epsilon > 0$ there exists $\lambda_0 \in \Lambda$ such that $\map d {x_\lambda, x} < \epsilon$ for $\lambda \in \Lambda$ with $\lambda_0 \preceq \lambda$.

Proof:
=== Necessary Condition ===
Suppose that $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ converges to $x$ in $\struct {X, d}$.
Let $\epsilon > 0$. 
From Open Ball is Open Set, the open ball $\map {B_\epsilon} x$ with radius $\epsilon$ and center $x$ is open in $\struct {X, d}$.
Since $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ converges to $x$, there exists $\lambda_0 \in \Lambda$ such that: 
:$x_\lambda \in \map {B_\epsilon} x$ for $\lambda \in \Lambda$ with $\lambda_0 \preceq \lambda$. 
That is: 
:$\map d {x_\lambda, x} < \epsilon$ for $\lambda \in \Lambda$ with $\lambda_0 \preceq \lambda$.
{{qed|lemma}}
Theorem: Characterization of Even Cover

Let $T = \struct {S, \tau}$ be a topological space.
Let $\UU$ be a cover of $S$.
Let $\tau_{S \times S}$ denote the product topology on the cartesian product $S \times S$.
Then $\UU$ is an even cover of $T$ {{iff}} there exists an open neighborhood $V$ of the diagonal $\Delta_S$ of $S \times S$ in the product space $\struct {S \times S, \tau_{S \times S} }$:
:$\set{\map V x : x \in S}$ is a refinement of $\UU$
where:
:$V$ is seen as a relation on $S \times S$
:$\map V x$ denotes the image of $x$ under $V$.

Proof:
=== Necessary Condition ===
Let $\UU$ be an even cover of $T$.
By definition of even cover, there exists a neighborhood $N$ of the diagonal $\Delta_S$ of $S \times S$ in the product space $\struct {S \times S, \tau_{S \times S} }$:
:$\set{\map N x : x \in S}$ is a refinement of $\UU$
By definition of a neighborhood, there exists an open set $V$ of $\struct {S \times S, \tau_{S \times S} }$:
:$\Delta_S \subseteq V \subseteq N$
From Set is Open iff Neighborhood of all its Points and Set is Neighborhood of Subset iff Neighborhood of all Points of Subset:
:$V$ is an open neighborhood of the $\Delta_S$
It remains to show that $\set {\map V x : x \in S}$ is a refinement of $\UU$.
Let $x \in S$.
We have:
:$\tuple{x, x} \in \Delta_S \subseteq V$
By definition of image:
:$x \in \map V x$
From {{Corollary|Image under Subset of Relation is Subset of Image under Relation}}:
:$\map V x \subseteq \map N x$
By definition of refinement:
:$\exists U \in \UU : \map N x \subseteq U$
From Subset Relation is Transitive:
:$\map V x \subseteq U$
Since $x$ was arbitrary, we have:
:$\forall x \in S : x \in \map V x$
and
:$\forall x \in S : \exists U \in \UU : \map V x \subseteq U$
It follows that $\set{\map V x : x \in S}$ is a cover of $S$ and a refinement of $\UU$ by definition.
{{qed|lemma}}
Theorem: Inverse of Open Set in Product Space is Open in Inverse Product Space

Let $\struct{S_1, \tau_1}$ and $\struct{S_2, \tau_2}$ be topological spaces.
Let $\tau_{S_1 \times S_2}$ be the product topology on the Cartesian product $S_1 \times S_2$.
Let $\tau_{S_2 \times S_1}$ be the product topology on the Cartesian product $S_2 \times S_1$.
Let $V \subseteq S_1 \times S_2$.
Let $V^{-1} \subseteq S_2 \times S_1$ denote the inverse of $V$ viewed as a relation on $S_1 \times S_2$.
Then:
:$V$ is open in $\struct{S_1 \times S_2, \tau_{S_1 \times S_2}}$ {{iff}} $V^{-1}$ is open in $\struct{S_2 \times S_1, \tau_{S_2 \times S_1}}$

Proof:
=== Necessary Condition ===
Let $V$ be open in $\struct{S_1 \times S_2, \tau_{S_1 \times S_2}}$.
Let $\tuple{s_2, s_1} \in V^{-1}$
By definition of inverse:
:$\tuple{s_1, s_2} \in V$
By definition of product topology:
:$\BB_{12} = \set{U \times W : U \in \tau_1, W \in \tau_2}$ is a basis for $\tau_{S_1 \times S_2}$
By definition of basis:
:$\exists U \in \tau_1, W \in \tau_2 : \tuple{s_1, s_2} \in U \times W \subseteq V$
By definition of inverse:
:$\tuple{s_2, s_1} \in W \times U \subseteq V^{-1}$
By definition of product topology:
:$\BB_{21} = \set{W \times U : W \in \tau_2, U \in \tau_1}$ is a basis for $\tau_{S_2 \times S_1}$
Since $\tuple{s_2, s_1}$ was arbitrary, we have:
:$\forall \tuple{s_2, s_1} \in V^{-1} : \exists W \times U \in \BB_{21} : \tuple{s_2, s_1} \in W \times U \subseteq V^{-1}$
From Characterization of Set Equals Union of Sets:
:$V^{-1} = \bigcup \set{W \times U \in \BB_{21} : W \times U \subseteq V^{-1}}$
By {{Open-set-axiom|1}}:
:$V^{-1}$ is open in $\struct{S_2 \times S_1, \tau_{S_2 \times S_1}}$
{{qed|lemma}}
Theorem: Standard Topology of Locally Convex Space has Local Basis of Balanced Convex Absorbing Sets

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \PP}$ be a locally convex space over $\GF$ with standard topology $\tau$. 
Then there exists a local basis $\BB$ for ${\mathbf 0}_X$ in $\struct {X, \tau}$ such that: 
:each $A \in \BB$ is balanced, convex and absorbing.

Proof:
For each $\epsilon > 0$ and $S$ a finite subset of $\PP$, set: 
:$U_{\epsilon, S} = \set {x \in X : \map p x < \epsilon \text { for each } p \in S}$
and:
:$\BB = \set {U_{\epsilon, S} : \epsilon > 0 \text { and } S \subseteq \PP \text { finite} }$
From Open Sets in Standard Topology of Locally Convex Space, $\BB'$ is a local basis for ${\mathbf 0}_X$ in $\struct {X, \tau}$.
From Convex Open Neighborhood of Origin in Topological Vector Space contains Balanced Convex Open Neighborhood:
:for each $A \in \BB'$ there exists a balanced convex open neighborhood $V_A$ for ${\mathbf 0}_X$ such that $U_A \subseteq A$.
Then: 
:$\BB = \set {V_A : A \in \BB'}$
forms a local basis for ${\mathbf 0}_X$ in $\struct {X, \tau}$, consisting of balanced convex open neighborhoods of ${\mathbf 0}_X$.
From Locally Convex Space is Topological Vector Space, $\struct {X, \tau}$ is a topological vector space.
From Convex Subset of Topological Vector Space containing Zero Vector in Interior is Absorbing Set, we therefore obtain that $V_A$ is absorbing for each $A \in \BB'$.
Hence $\BB$ is a local basis for ${\mathbf 0}_X$ in $\struct {X, \tau}$, consisting of balanced convex absorbing sets. 
{{qed}}
Category:Locally Convex Spaces
Category:Balanced Sets
Category:Absorbing Sets
Category:Convex Sets (Vector Spaces)
pmj4m2i4kdqarm9j8vg7tst7t2xiybz
Theorem: Realification of Topological Vector Space is Topological Vector Space

Let $\struct {X, \tau}$ be a topological vector space over $\C$.
Let $X_\R$ be the realification of $X$.
Then $\struct {X_\R, \tau}$ is a topological vector space over $\R$. 
Further, $\struct {X, \tau}$ is a Hausdorff topological vector space {{iff}} $\struct {X_\R, \tau}$ is a Hausdorff topological vector space.

Proof:
Since $\struct {X, \tau}$ is a topological vector space, the vector addition map $+_X : X \times X \to X$ is continuous.
Note that the underlying sets and topologies of $X_\R$ and $X$ are identical, we are only restricting the scalar field.
So the vector addition map $+_{X_\R} : X_\R \times X_\R \to X_\R$ is also continuous.
Again since $\struct {X, \tau}$ is a topological vector space, the scalar multiplication map $\circ_X : \C \times X \to X$.
By the definition of realification, the scalar multiplication map $\circ_{X_\R} : \R \times X \to X$ on the realification is precisely the restriction of $\circ_X$ to $\R \times X$.
From Restriction of Continuous Mapping is Continuous, $\circ_{X_\R}$ is therefore continuous. 
So $\struct {X_\R, \tau}$ is a topological vector space over $\R$.
The topology on $X$ and $X_{\R}$ are the same, so $\struct {X, \tau}$ is a Hausdorff topological vector space {{iff}} $\struct {X_\R, \tau}$ is a Hausdorff topological vector space.
{{qed}}
Category:Topological Vector Spaces
Category:Realifications of Complex Vector Spaces
5c4eofww5rqojc49ul37x4rd93bamj9
Theorem: Hahn-Banach Separation Theorem/Hausdorff Locally Convex 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 $X_\R$ be the realification of $X$. 
Applying Hahn-Banach Separation Theorem: Hausdorff Locally Convex Space: Real Case: Open Convex Set and Convex Set, there exists a continuous $\R$-linear functional $g : X \to \R$ and $c \in \R$ such that: 
:$\map g a < c \le \map g b$ for each $a \in A$ and $b \in B$.
From Continuous Real Linear Functional on Complex Topological Vector Space is Real Part of Continuous Complex Linear Functional, there exists $f \in X^\ast$ such that: 
:$\map g x = \map \Re {\map f x}$ for each $x \in X$. 
Then, we have: 
:$\map \Re {\map f a} < c \le \map \Re {\map f b}$ for each $a \in A$ and $b \in B$.
{{qed}}
Category:Hahn-Banach Separation Theorem
fmij6ml7om928465h14v95gtblapir2
Theorem: Hahn-Banach Separation Theorem/Hausdorff Locally Convex Space/Complex Case/Compact Convex Set and Closed Convex Set

Let $A \subseteq X$ be an compact convex set.
Let $B \subseteq X$ be a closed convex set disjoint from $A$. 
Then there exists $f \in X^\ast$ such that: 
:$\ds \sup_{x \mathop \in A} \map \Re {\map f x} < \inf_{x \mathop \in B} \map \Re {\map f x}$

Proof:
Let $X_\R$ be the realification of $X$. 
Applying Hahn-Banach Separation Theorem: Hausdorff Locally Convex Space: Real Case: Compact Convex Set and Closed Convex Set, there exists a continuous $\R$-linear functional $g : X \to \R$ and $c \in \R$ such that: 
:$\ds \sup_{x \mathop \in A} \map g x < \inf_{x \mathop \in B} \map g x$
From Continuous Real Linear Functional on Complex Topological Vector Space is Real Part of Continuous Complex Linear Functional, there exists $f \in X^\ast$ such that: 
:$\map g x = \map \Re {\map f x}$ for each $x \in X$. 
Then, we have: 
:$\ds \sup_{x \mathop \in A} \map \Re {\map f x} < \inf_{x \mathop \in B} \map \Re {\map f x}$
{{qed}}
Category:Hahn-Banach Separation Theorem
oybkbxnonnk0d33n9mzf48bnoegwd8k
Theorem: Spanning Criterion of Normed Vector Space

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space over $\GF$.
Let $X^\ast$ be the vector space of bounded linear functionals on $X$.
Let $A \subseteq X$ be a subset.
Let $\vee A$ be the closed linear span of $A$, i.e. the closure of the linear span of $A$.
Then $z \in \vee A$ {{iff}}:
:$\forall \ell \in X^\ast : \ell \restriction_A = 0 \implies \map \ell z = 0$
where $\ell \restriction_A$ denotes the restriction of $\ell$ to $A$.

Proof:
=== Necessary condition ===
Let $z \in \vee A$.
Let $\ell \in X^\ast$ such that $\ell \restriction_A = 0$.
Recall, by {{Defof|Bounded Linear Functional|$X^\ast$}}, there is a $C > 0$ such that:
:$(1):\quad \forall x \in X : \size {\map \ell x} \le C \norm x$
On the other hand::
{{begin-eqn}}
{{eqn | l = \map \ell {z - \sum_{i \mathop = 1}^n \alpha_i a_i}
      | r = \map \ell z - \sum_{i \mathop = 1}^n \alpha_i \map \ell {a_i}
      | c = {{Defof|Bounded Linear Functional}}
}}
{{eqn | r = \map \ell z
      | c = $\map \ell {a_i} = 0$ {{hypothesis}}
      | n = 2
}}
{{end-eqn}}
Let $\epsilon > 0$.
Then there exist:
:$n \in \Z_{>0}$
:$\alpha_1, \ldots, \alpha_n \in \GF$
:$a_1, \ldots, a_n \in A$
such that:
:$\ds (3):\quad \norm {z - \sum_{i \mathop = 1}^n \alpha_i a_i} < \epsilon$.
Therefore:
{{begin-eqn}}
{{eqn | l = \size {\map \ell z}
      | r = \size {\map \ell {z - \sum_{i \mathop = 1}^n \alpha_i a_i} }
      | c = by $(2)$
}}
{{eqn | o = \le
      | r = C \norm {z - \sum_{i \mathop = 1}^n \alpha_i a_i}
      | c = by $(1)$
}}
{{eqn | o = <
      | r = C \epsilon
      | c = by $(3)$
}}
{{end-eqn}}
By $\epsilon \to 0$, we obtain:
:$\map \ell z = 0$
{{qed|lemma}}
Theorem: Absolute Error of Sum is not Greater than Sum of Absolute Errors

Let $X_1, X_2, \ldots, X_n$ be approximations to a collection of (true) values $x_1, x_2, \ldots, x_n$ respectively.
Let $\Delta X_i$ be the absolute error of $X_i$ in $x_i$ for $i \in \set {1, 2, \ldots, n}$.
Then:
:$\ds \map \Delta {\sum_{i \mathop = 1}^n X_i} \le \sum_{i \mathop = 1}^n \Delta X_i$
That is, the absolute error of a sum of approximations is not greater than the sum of the absolute errors of those approximations.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 2}$, let $\map P n$ be the proposition:
:$\ds \map \Delta {\sum_{i \mathop = 1}^n X_i} \le \sum_{i \mathop = 1}^n \Delta X_i$
for appropriately defined $X_1, X_2, \ldots, X_n$ and $x_1, x_2, \ldots, x_n$.