avewright/proofwiki-math huggingface dataset:
Theorem: Interior Separating Hyperplane Theorem

Let $\struct {X, \tau}$ be a topological vector space over $\R$.
Let $\cl$ be the closure in $\struct {X, \tau}$. 
Let $A \subseteq X$ be a convex set with non-empty interior $\Int A$. 
Let $B \subseteq X$ be a non-empty convex set with $A \cap B = \O$. 
Then $\map \cl A$ and $\map \cl B$ are properly separated by a continuous linear functional.

Proof:
Since $A \cap B = \O$, we have $\Int A \cap B = \O$.
From Interior of Convex Set in Topological Vector Space is Convex, $\Int A$ is convex.
From Interior Point of Subset of Topological Vector Space is Internal Point, each point in $\Int A$ is an internal point of $A$. 
Hence, from Basic Separating Hyperplane Theorem, there exists a linear functional $f$ properly separating $\Int A$ and $B$.
From Continuous Separation of Non-Empty Subsets of Topological Vector Space also Separates Closures, $f$ properly separates $\map \cl {\Int A}$ and $\map \cl B$.
From Closure of Convex Set in Topological Vector Space with Non-Empty Interior coincides with Closure of Interior, we have $\map \cl {\Int A} = \map \cl A$.
Hence $f$ properly separates $\map \cl {\Int A}$ and $\map \cl B$.
From Separation of Non-Empty Set from Set containing Interior Point is Continuous and Proper, $f$ is continuous.
{{qed}}
Theorem: Interior Point of Subset of Topological Vector Space is Internal Point

Let $\struct {X, \tau}$ be a topological vector space over $\R$.
Let $A \subseteq X$ be a non-empty.
Let $x \in \Int A$.
Then $x$ is an internal point of $A$.

Proof:
Since $x \in \Int A$, there exists an open neighborhood $U$ of $x$ such that:
:$U \subseteq \Int A$
From Classification of Open Neighborhoods in Topological Vector Space, there exists an open neighborhood $V$ of ${\mathbf 0}_X$ such that:
:$U = x + V$
Then:
:$x + V \subseteq A$
From Open Neighborhood of Origin in Topological Vector Space is Absorbing, $V$ is absorbing.
Hence $x$ is an internal point of $A$.
{{qed}}
Category:Topological Vector Spaces
ds6dnwhzahxnx3p79716t2d9jhdeec1
Theorem: Sublinear Functional is Linear Functional iff Dominates Unique Linear Functional

Let $X$ be a vector space over $\R$. 
Let $p : X \to \R$ be a sublinear functional.
Then $p$ is linear {{iff}} there exists a unique linear functional $f : X \to \R$ such that:
:$\map f x \le \map p x$ for each $x \in X$.

Proof:
=== Necessary Condition ===
Suppose that $p$ is linear.
Let $f : X \to \R$ be a linear functional such that:
:$\map f x \le \map p x$ for each $x \in X$.
Then, swapping $x$ with $-x$ we have:
:$\map f {-x} \le \map p {-x}$ for each $x \in X$.
That is, since both $f$ and $p$ are linear, we have:
:$-\map f x \le -\map p x$ for each $x \in X$.
Hence:
:$\map f x \ge \map p x$ for each $x \in X$.
Hence:
:$\map f x = \map p x$
Hence such an $f$ is unique.
{{qed|lemma}}
Theorem: Convex Hahn-Banach Theorem

Let $X$ be a vector space over $\R$. 
Let $M$ be a vector subspace of $X$.
Let $p : X \to \R$ be a convex function.
Let $f : M \to \R$ be a linear functional satisfying:
:$\map f x \le \map p x$ for each $x \in M$.
Then there exists a linear functional $\hat f : X \to \R$ extending $f$ and satisfying:
:$\map {\hat f} x \le \map p x$ for each $x \in X$.

Proof:
Define $P : X \to \hointr 0 \infty$ by:
:$\ds \map P x = \inf_{t > 0} t^{-1} \map p {t x}$ for each $x \in X$.
Since $\map p x \ge 0$ for each $x \in X$, we have that $P$ is well-defined.
We can also see, by taking $t = 1$, that:
:$\map P x \le \map p x$ for each $x \in X$.
We show that $P$ is a sublinear functional.
Let $\lambda > 0$ and $x \in X$.
We have:
{{begin-eqn}}
{{eqn	| l = \map P {\lambda x}
		| r = \inf_{t > 0} t^{-1} \map p {\lambda t x}
}}
{{eqn	| r = \lambda \inf_{t > 0} \paren {\lambda t}^{-1} \map p {\lambda t x}
		| c = Multiple of Infimum
}}
{{eqn	| r = \lambda \inf_{s > 0} s^{-1} \map p {s x}
		| c = taking $s = \lambda t$ 
}}
{{eqn	| r = \lambda \map P x
}}
{{end-eqn}}
Hence $P$ is positive homogeneous.
We now show that:
:$\map P {x + y} \le \map P x + \map P y$ for each $x, y \in X$.
Let $t > 0$ and $s > 0$.
We have:
:$\ds \map P {x + y} \le \frac {s + t} {s t} \map p {\frac {s t} {s + t} \paren {x + y} }$
We can write the {{RHS}} as:
:$\ds \frac {s + t} {s t} \map p {\frac s {s + t} \paren {t x} + \frac t {s + t} \paren {s y} }$
Since:
:$\ds 1 = \frac s {s + t} + \frac t {s + t}$
we have that:
:$\ds \map p {\frac s {s + t} \paren {t x} + \frac t {s + t} \paren {s y} } \le \frac s {s + t} \map p {t x} + \frac t {s + t} \map p {s y}$
Hence we have:
{{begin-eqn}}
{{eqn	| l = \frac {s + t} {s t} \map p {\frac s {s + t} \paren {t x} + \frac t {s + t} \paren {s y} }
		| o = \le
		| r = \frac {s + t} {s t} \paren {\frac s {s + t} \map p {t x} + \frac t {s + t} \map p {s y} }
}}
{{eqn	| r = \frac s {s t} \map p {t x} + \frac t {s t} \map p {s y}
}}
{{eqn	| r = \frac 1 t \map p {t x} + \frac 1 s \map p {s y}
}}
{{end-eqn}}
That is:
:$\ds \map P {x + y} \le \frac 1 t \map p {t x} + \frac 1 s \map p {s y}$
Taking the infimum over $t > 0$, we have:
:$\ds \map P {x + y} \le \map P x + \frac 1 s \map p {s y}$
Taking the infimum over $s > 0$, we have:
:$\ds \map P {x + y} \le \map P x + \map P y$
Hence $P$ is a sublinear functional.
Recall that:
:$\map f x \le \map p x$ for each $x \in M$. 
Let $t > 0$.
Swapping $x$ for $t x$, we have:
:$\map f {t x} \le \map p {t x}$ for each $x \in M$.
Multiplying through by $t^{-1}$:
:$t^{-1} \map f {t x} \le t^{-1} \map p {t x}$ for each $x \in M$.
Since $f$ is linear, we have:
:$t^{-1} \map f {t x} = \map f x$
Hence:
:$\map f x \le t^{-1} \map p {t x}$ for each $x \in M$.
Taking the infimum over $t > 0$, we have:
:$\map f x \le \map P x$ for each $x \in M$.
From the Hahn-Banach Theorem: Real Vector Space, there exists a linear functional $\hat f : X \to \R$ extending $f$ such that:
:$\map {\hat f} x \le \map P x$ for each $x \in X$.
Since $\map P x \le \map p x$ for each $x \in X$, we have:
:$\map {\hat f} x \le \map p x$
{{qed}}
Theorem: Normed Vector Space is Finite Dimensional iff Closed Unit Ball is Weak Neighborhood of Origin

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ is a normed vector space over $\GF$.
Let $B_X^-$ be the closed unit ball in $\struct {X, \norm {\, \cdot \,}_X}$.
Let $w$ be the weak topology of $\struct {X, \norm {\, \cdot \,}_X}$.
Then $X$ is finite-dimensional {{iff}} $B_X^-$ is a $w$-neighborhood of ${\mathbf 0}_X$.

Proof:
From the definition of the weak topology, every $w$-open set is norm open.
We show that under the hypotheses, every norm open set is $w$-open.
Let $U$ be a norm open set.
Let $V \subseteq B_X^-$ be $w$-open.
Then for each $x \in U$, there exists $\delta_x > 0$ such that:
:$x + \delta_x B_X^- \subseteq U$
so that:
:$x + \delta_x V \subseteq U$ for each $x \in U$.
From Dilation of Open Set in Topological Vector Space is Open, $\delta_x V$ is $w$-open.
From Translation of Open Set in Topological Vector Space is Open, $x + \delta_x V$ is $w$-open.
We then have that: 
:$\ds U = \bigcup_{x \mathop \in U} \paren {x + \delta_x V}$ is $w$-open
as the union of open sets.
Hence every norm open set is $w$-open.
Hence the norm topology and the weak topology coincide.
From Weak Topology and Norm Topology on Normed Vector Space Coincide iff Finite Dimensional, $X$ is finite dimensional.
{{qed}}
Category:Normed Vector Spaces
Category:Weak Topologies on Topological Vector Spaces
gy2ds80i5rd5xp168nk6s5qdvlzlda5
Theorem: Closed Unit Ball of Infinite-Dimensional Normed Vector Space has Empty Weak Interior

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space over $\GF$ that is infinite-dimensional.
Let $B_X^-$ be the closed unit ball of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $w$ be the weak topology on $\struct {X, \norm {\, \cdot \,}_X}$.
Let $\operatorname {Int}_w$ be the interior taken in $\struct {X, w}$.
Then $\map {\operatorname {Int}_w} {B_X^-} = \O$.

Proof:
{{AimForCont}} that $\map {\operatorname {Int}_w} {B_X^-} \ne \O$.
Let $u \in \map {\operatorname {Int}_w} {B_X^-}$.
Then there exists an open neighborhood $U$ of $u$ such that $U \subseteq B_X^-$.
From Classification of Open Neighborhoods in Topological Vector Space, there exists an open neighborhood $V$ of ${\mathbf 0}_X$ such that:
:$x + V \subseteq B_X^-$
We show that:
:$\ds \frac 1 2 V \subseteq B_X^-$
For each $v \in V$, we have:
:$\ds \norm {\frac 1 2 v}_X = \frac 1 2 \norm v_X$
We can write $v = \paren {u + v} - u$.
Since $x + V \subseteq B_X^-$, we have $\norm {u + v}_X \le 1$.
Since $u \in \map {\operatorname {Int}_w} {B_X^-}$, we have $\norm u_X \le 1$.
By {{NormAxiomVector|3}}, we therefore have:
:$\norm v_X = \norm {\paren {u + V} - u}_X \le 2$ 
hence:
:$\ds \norm {\frac 1 2 v}_X \le 1$ 
So:
:$\ds \frac 1 2 V \subseteq B_X^-$
From Dilation of Open Set in Topological Vector Space is Open, $\ds \frac 1 2 V$ is a $w$-open neighborhood of ${\mathbf 0}_X$.
Hence $B_X^-$ is a $w$-neighborhood of ${\mathbf 0}_X$.
From Normed Vector Space is Finite Dimensional iff Closed Unit Ball is Weak Neighborhood of Origin, $X$ is finite dimensional.
This is a contradiction.
Hence $\map {\operatorname {Int}_w} {B_X^-} = \O$.
{{qed}}
Theorem: Intersection of Finitely Many Kernels of Linear Functionals in Infinite-Dimensional Vector Space is Infinite-Dimensional with Finite Codimension

Let $K$ be a field.
Let $X$ be an infinite-dimensional vector space over $K$.
Let $X^\#$ be the algebraic dual of $X$.
Let $F$ be a non-empty finite subset of $X^\#$. 
We then have that:
:$\ds \map {\operatorname {dim} } {\bigcap_{f \in F} \map \ker f} = \infty$
and:
:$\ds \map {\operatorname {codim} } {\bigcap_{F \in F} \map \ker f} < \infty$
where $\ker$ denotes the kernel.
In particular:
:$\ds \bigcap_{f \in F} \map \ker f \ne \set { {\mathbf 0}_X}$

Proof:
Let $\operatorname {codim}$ denote codimension.
From Kernel of Linear Transformation is Linear Subspace, $\ker f$ is a vector subspace for each $f \in F$.
From Set of Linear Subspaces is Closed under Intersection:
:$\ds \bigcap_{f \in F} \ker f$ is a vector subspace of $X$.
If $f = {\mathbf 0}_{X^\#}$, then $\map \ker f = X$.
From Codimension of Whole Vector Space, we then have $\map {\operatorname {codim} } f = 0$.
If $f \ne {\mathbf 0}_{X^\#}$, then we have $\map {\operatorname {codim} } f = 1$ from Kernel of Non-Zero Linear Functional has Codimension 1.
Hence:
:$\map {\operatorname {codim} } f \le 1$ for all $f \in F$.
From Codimension of Intersection of Finitely Many Vector Subspaces is Bounded Above by Sum of Codimensions, we have:
:$\ds \map {\operatorname {codim} } {\bigcap_{f \in F} \ker f} \le \sum_{f \in F} \map {\operatorname {codim} } {\map \ker f} \le \size F < \infty$
From Dimension of Quotient Vector Space, we have:
:$\ds \map \dim {\bigcap_{f \in F} \ker f} + \map {\operatorname {codim} } {\bigcap_{f \in F} \ker f} = \dim X = \infty$
Since:
:$\ds \map {\operatorname {codim} } {\bigcap_{f \in F} \ker f} < \infty$
we must have:
:$\ds \map \dim {\bigcap_{f \in F} \ker f} = \infty$
Hence:
:$\ds \bigcap_{f \in F} \map \ker f \ne \set { {\mathbf 0}_X}$
{{qed}}
Category:Vector Spaces
iwsiclbysns32fjvzbgvf6rbz6uvgjr
Theorem: Duality Mapping of Dual System of Normed Vector Space with Normed Dual is Jointly Continuous

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space over $\GF$.
Let $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ be the normed dual space of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $\struct {X \times X^\ast, \norm {\, \cdot \,}_{X \times X^\ast} }$ be the direct product $X \times X^\ast$ with the direct product norm.
Define $\innerprod \cdot \cdot : X \times X^\ast \to \GF$ by:
:$\innerprod x f = \map f x$ for each $\tuple {x, f} \in X \times X^\ast$.
Then $\innerprod \cdot \cdot : \struct {X \times X^\ast, \norm {\, \cdot \,}_{X \times X^\ast} } \to \GF$ is continuous.

Proof:
Let $\sequence {\tuple {x_n, f_n} }_{n \mathop \in \N}$ be a sequence in $X \times X^\ast$ converging to $\tuple {x, f}$.
We then have:
{{begin-eqn}}
{{eqn	| l = \cmod {\innerprod {x_n} {f_n} - \innerprod x f}
		| r = \cmod {\innerprod {x_n} {f_n} - \innerprod {x_n} f + \innerprod {x_n} f - \innerprod x f}
}}
{{eqn	| o = \le
		| r = \cmod {\innerprod {x_n} {f_n - f} + \innerprod {x_n - x} f}
		| c = {{Defof|Dual System}}
}}
{{eqn	| o = \le
		| r = \cmod {\innerprod {x_n} {f_n - f} } + \cmod {\innerprod {x_n - x} f}
		| c = Triangle Inequality
}}
{{eqn	| r = \cmod {\map {\paren {f_n - f} } {x_n} } + \cmod {\map f {x_n - x} }
}}
{{eqn	| o = \le
		| r = \norm {f_n - f}_{X^\ast} \norm {x_n}_X + \norm f_{X^\ast} \norm {x_n - x}_X 
		| c = Fundamental Property of Norm on Bounded Linear Functional
}}
{{end-eqn}}
From Convergent Sequence in Normed Vector Space is Bounded, there exists $M > 0$ such that:
:$\norm {x_n}_X \le M$ for each $n \in \N$.
Hence we have:
:$\cmod {\innerprod {x_n} {f_n} - \innerprod x f} \le M \norm {f_n - f}_{X^\ast} + \norm f_{X^\ast} \norm {x_n - x}_X$
From Convergence in Direct Product Norm, we have:
:$x_n \to x$ in $\struct {X, \norm {\, \cdot \,}_X}$
and:
:$f_n \to f$ in $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast}$
and hence:
:$\cmod {\innerprod {x_n} {f_n} - \innerprod x f} \to 0$
We have therefore shown that if:
:$\tuple {x_n, f_n} \to \tuple {x, f}$ in $\struct {X \times X^\ast, \norm {\, \cdot \,}_{X \times X^\ast} }$
then:
:$\innerprod {x_n} {f_n} \to \innerprod x f$
Hence $\innerprod \cdot \cdot$ is sequentially continuous.
From Sequential Continuity is Equivalent to Continuity in Metric Space, $\innerprod \cdot \cdot$ is continuous.
{{qed}}
Theorem: Pointwise Supremum of Family of Lower Semicontinuous Functions is Lower Semicontinuous

Let $\struct {X, \tau}$ be a topological space.
Let $\family {f_\alpha}_{\alpha \mathop \in I}$ be a set of lower semicontinuous functions $f_\alpha : X \to \overline \R$.
Define $f : X \to \overline \R$ by:
:$\ds \map f x = \limsup_{\alpha \mathop \in I} \map {f_\alpha} x$ for each $x \in X$.
Then $f$ is lower semicontinuous.

Proof:
For $t \in \R$, we have:
:$\ds \limsup_{\alpha \mathop \in I} \map {f_\alpha} x \le t$
{{iff}}:
:$\map {f_\alpha} x \le t$ for each $\alpha \in I$.
Hence:
:$\ds \set {x \in X : \map f x \le t} = \bigcap_{\alpha \mathop \in I} \set {x \in X : \map {f_\alpha} x \le t}$
Since $f_\alpha$ is lower semicontinuous, we have:
:$\set {x \in X : \map {f_\alpha} x \le t}$ is closed for each $\alpha \in I$
by Characterization of Lower Semicontinuity.
Hence:
:$\set {x \in X : \map f x \le t}$ is the intersection of closed sets.
Hence by Characterization of Lower Semicontinuity, $f$ is lower semicontinuous.
{{qed}}
Theorem: Negative of Limit Superior of Real Net is Limit Inferior

Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ be a net valued in $\R$.
Then:
:$\ds -\limsup_{\lambda \mathop \in \Lambda} x_\lambda = \liminf_{\lambda \mathop \in \Lambda} \paren {-x_\lambda}$

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = -\limsup_{\lambda \mathop \in \Lambda} x_\lambda
		| r = -\inf_{\lambda_0 \mathop \in \Lambda} \sup_{\lambda \succeq \lambda_0} x_\lambda
		| c = {{Defof|Limit Superior of Net}}
}}
{{eqn	| r = \sup_{\lambda \mathop \in \Lambda} \paren {-\sup_{\lambda \succeq \lambda_0} x_\lambda}
		| c = Negative of Infimum is Supremum of Negatives
}}
{{eqn	| r = \sup_{\lambda \mathop \in \Lambda} \inf_{\lambda \succeq \lambda_0} \paren {-x_\lambda}
		| c = Negative of Supremum is Infimum of Negatives
}}
{{eqn	| r = \liminf_{\mathop \in \Lambda} \paren {-x_\lambda}
		| c = {{Defof|Limit Inferior of Net}}
}}
{{end-eqn}}
{{qed}}
Category:Limits Superior
Category:Limits Inferior
g54wd5z0difrttk7fzgjvf20dmipgs9
Theorem: Real-Valued Lower Semicontinuous Function on Compact Space attains Minimum with Compact Set of Minimizers

Let $\struct {X, \tau}$ be a compact topological space.
Let $f : X \to \R$ be a lower semicontinuous function.
Then there exists $x_0 \in X$ such that:
:$\ds \map f {x_0} = \inf_{x \mathop \in X} \map f x$ 
and $\ds f^{-1} \sqbrk {\inf_{x \mathop \in X} \map f x}$ is compact.

Proof:
Let $A = f \sqbrk X$.
For each $c \in A$, define:
:$F_c = \set {x \in X : \map f x \le c}$ 
Since $f$ is lower semicontinuous, $F_c$ is closed for each $c \in A$.
Further, for $c_1, \ldots, c_n \in A$, we have:
{{begin-eqn}}
{{eqn	| l = \bigcap_{j \mathop = 1}^n F_{c_j}
		| r = \bigcap_{j \mathop = 1}^n \set {x \in X : \map f x \le c_j}
}}
{{eqn	| r = \set {x \in X : \map f x \le \min \set {c_1, \ldots, c_n} }
}}
{{end-eqn}}
Since:
:$\min \set {c_1, \ldots, c_n} = c_j \in f \sqbrk X$ for some $1 \le j \le n$
we have:
:$\set {x \in X : \map f x \le \min \set {c_1, \ldots, c_n} } \supseteq \set {x \in X : \map f x = c_j} \ne \O$
Hence:
:$\ds \bigcap_{j \mathop = 1}^n F_{c_j} \ne \O$
From Definition:Finite Intersection Property:
:$\set {F_c : c \in A} \subseteq \map \PP X$ has the finite intersection property.
From Intersection of Closed Subsets satisfying Finite Intersection Property in Compact Space, we have that:
:$\ds \bigcap_{c \mathop \in A} F_c \ne \O$
since $X$ is compact.
Then there exists:
:$\ds x_0 \in \bigcap_{c \mathop \in A} F_c$
We have:
:$\ds x_0 \in \bigcap_{c \mathop \in A} F_c$
{{iff}}:
:$\map f {x_0} \le c$ for each $c \in A$.
That is:
:$\map f {x_0} \le \map f x$ for each $x \in X$.
Hence:
:$\ds x_0 \in \bigcap_{c \mathop \in A} F_c$
{{iff}}:
:$\ds \map f {x_0} = \inf_{x \mathop \in X} \map f x$ 
From this, we have:
:$\ds f^{-1} \sqbrk {\inf_{x \mathop \in X} \map f x} = \bigcap_{c \mathop \in A} F_c \ne \O$
Since each $F_c$ is closed, we have:
:$\ds \bigcap_{c \mathop \in A} F_c$ is closed.
From Closed Subspace of Compact Space is Compact, we have that:
:$\ds f^{-1} \sqbrk {\inf_{x \mathop \in X} \map f x} = \bigcap_{c \mathop \in A} F_c$ is compact.
{{qed}}
Theorem: Real-Valued Upper Semicontinuous Function on Compact Space attains Maximum with Compact Set of Maximizers

Let $\struct {X, \tau}$ be a compact topological space.
Let $f : X \to \R$ be a upper semicontinuous function.
Then there exists $x_0 \in X$ such that:
:$\ds \map f {x_0} = \sup_{x \mathop \in X} \map f x$ 
and $\ds f^{-1} \sqbrk {\sup_{x \mathop \in X} \map f x}$ is compact.

Proof:
From Function is Upper Semicontinuous iff Negative is Lower Semicontinuous, $-f$ is lower semicontinuous.
From Real-Valued Lower Semicontinuous Function on Compact Space attains Minimum with Compact Set of Minimizers, there exists $x_0 \in X$ such that:
:$\ds -\map f {x_0} = \inf_{x \mathop \in X} \paren {-\map f x}$
From Negative of Supremum is Infimum of Negatives, we have:
:$\ds \inf_{x \mathop \in X} \paren {-\map f x} = -\sup_{x \mathop \in X} \map f x$
Hence:
:$\ds \map f {x_0} = \sup_{x \mathop \in X} \map f x$
Further, from Real-Valued Lower Semicontinuous Function on Compact Space attains Minimum with Compact Set of Minimizers, we have that:
:$\ds \paren {-f}^{-1} \sqbrk {\inf_{x \mathop \in X} \paren {-\map f x} }$ is compact.
Then:
{{begin-eqn}}
{{eqn	| l = \paren {-f}^{-1} \sqbrk {\inf_{x \mathop \in X} \paren {-\map f x} }
		| r = \set {x_0 \in X : -\map f {x_0} = \inf_{x \mathop \in X} \paren {-\map f x} }
}}
{{eqn	| r = \set {x_0 \in X : \map f {x_0} = -\inf_{x \mathop \in X} \paren {-\map f x} }
}}
{{eqn	| r = \set {x_0 \in X : \map f {x_0} = \sup_{x \mathop \in X} \map f x}
		| c = Negative of Infimum is Supremum of Negatives
}}
{{eqn	| r = f^{-1} \sqbrk {\sup_{x \mathop \in X} \map f x}
}}
{{end-eqn}}
{{qed}}
Theorem: Evaluation Mapping of Infinite-Dimensional Normed Vector Space is not Jointly Continuous with Normed Vector Space given Weak Topology

Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space over $\R$.
Let $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ be the normed dual of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $w$ be the weak topology of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $\struct {X, w} \times \struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ be the direct product of $\struct {X, w}$ and $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ with the product topology 
Define $\innerprod \cdot \cdot : \struct {X, w} \times \struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} } \to \R$ by:
:$\innerprod x f = \map f x$ for each $\tuple {x, f} \in X \times X^\ast$.
Then $\innerprod \cdot \cdot$ is not continuous at $\struct { {\mathbf 0}_X, {\mathbf 0}_{X^\ast} }$.

Proof:
Let $\struct {\FF, \subseteq}$ be the set of non-empty finite subsets of $X^\ast$ equipped with set inclusion.
From Set of Finite Subsets is Directed Set with Set Inclusion, $\struct {\FF, \subseteq}$ is directed.
From Intersection of Finitely Many Kernels of Linear Functionals in Infinite-Dimensional Vector Space is Infinite-Dimensional with Finite Codimension:
:$\ds \bigcap_{f \in F} \ker f \ne \set { {\mathbf 0}_X}$ for each $F \in \FF$.
For each $F \in \FF$, take:
:$\ds x_F \in \bigcap_{f \in F} \ker f \ne \set { {\mathbf 0}_X}$
with $\norm {x_F}_X = \size F$.
From Existence of Support Functional, for each $F \in \FF$ there exists $f_F \in X^\ast$ such that $\norm f_{X^\ast} = 1$ and:
:$\map {f_F} {x_F} = \norm {x_F} = \size F$ 
For each $F \in \FF$, define:
:$\ds g_F = \frac {f_F} {\size F}$
We have, by {{NormAxiomVector|2}}:
:$\ds \norm {g_F}_{X^\ast} = \frac 1 {\size F}$
Since $X^\ast$ is infinite, for each $n \in \N$ we can pick a set $F_n \subseteq X^\ast$ with $\size {F_n} = n$. 
Then, for $F$ with $F \supseteq F_n$, we have:
:$\ds \norm {g_F}_{X^\ast} \le \frac 1 n$ 
Hence we have that $g_F \to {\mathbf 0}_{X^\ast}$ as a net in $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$.
Further, as shown in Infinite-Dimensional Normed Vector Space contains Weakly Null Net with Unbounded Tails, we have that $x_F \to {\mathbf 0}_X$ in $\struct {X, w}$. 
From Characterization of Convergence of Net in Product Topology, we have:
:$\tuple {x_F, g_F} \to \tuple { {\mathbf 0}_X, {\mathbf 0}_{X^\ast} }$
However, we have:
:$\ds \innerprod {x_F} {g_F} = \frac {\map {f_F} {x_F} } {\size F} = 1$
while:
:$\innerprod { {\mathbf 0}_X} { {\mathbf 0}_{X^\ast} } = 0$
Hence, from Characterization of Hausdorff Property in terms of Nets, we have that:
:$\innerprod {x_F} {g_F} \not \to \innerprod { {\mathbf 0}_X} { {\mathbf 0}_{X^\ast} }$
Hence from Characterization of Continuity in terms of Nets, $\innerprod \cdot \cdot$ is not continuous.
{{qed}}
Theorem: Existence of Locally Convex Topology Consistent with Dual System

Let $\GF \in \set {\R, \C}$.
Let $\innerprod E F$ be a dual system over $\GF$.
Then there exists a locally convex topology on $E$ consistent with $\innerprod E F$.

Proof:
For each $f \in F$, define $\pi_f : E \to \GF$ by:
:$\map {\pi_f} x = \innerprod x f$ for each $x \in E$. 
Let $\tau$ be the initial topology on $E$ induced by $\pi_f$.
This is precisely the weak topology $\map \sigma {E, F}$.
Let $\struct {E, \tau}^\ast$ be the topological dual space of $\struct {E, \tau}$.
We aim to show that $\struct {E, \tau}^\ast = \set {\pi_f : f \in F}$ to finish.
For each $f \in F$, define $p_f : E \to \hointr 0 \infty$ by:
:$\map {p_f} x = \size {\map {\pi_f} x}$ for each $x \in E$. 
Let $\PP = \set {p_f : f \in F}$. 
From Initial Topology on Vector Space Generated by Linear Functionals is Locally Convex, $\struct {E, \PP}$ is a locally convex space with standard topology $\tau$.
From Continuity of Linear Functionals in Weak Topology Induced by Pair of Vector Spaces with Bilinear Mapping, it follows that $\struct {E, \tau}^\ast = \set {\pi_f : f \in F}$.
Hence $\tau$ is the locally convex topology on $E$ consistent with $\innerprod E F$.
{{qed}}
Category:Dual Systems
4gz4s7gr8x9fz9mshchez7hwyb9iik5
Theorem: Metric Projection Fixes Points of Convex Set

Let $\GF \in \set {\R, \C}$.
Let $\struct {\HH, \innerprod \cdot \cdot}$ be a Hilbert space over $\GF$.
Let $\norm {\, \cdot \,}_\HH$ be the inner product norm.
Let $\pi_C : \HH \to C$ be the metric projection of $\HH$ onto $C$. 
Then:
:$\map {\pi_C} x = x$ for each $x \in C$.

Proof:
Let $x \in C$.
We have:
:$\ds \inf_{z \mathop \in C} \norm {x - z}_\HH \le \norm {x - x}_\HH = 0$
Hence:
:$\ds \inf_{z \mathop \in C} \norm {x - z}_\HH = 0$
Hence from Unique Point of Minimal Distance to Closed Convex Subset of Hilbert Space and the definition of the metric projection we have $\map {\pi_C} x = x$.
{{qed}}