avewright/proofwiki-math huggingface dataset:
Theorem: Characterization of Convergence of Net in Weak Topology Induced by Dual System

Let $K$ be a topological field.
Let $\innerprod X {X'}$ be a dual system over $K$. 
Let $\map \sigma {X, X'}$ be the weak topology on $X$ induced by $\innerprod X {X'}$.
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 to $x$ in $\struct {X, \map \sigma {X, X'} }$ {{iff}}:
:$\innerprod {x_\lambda} {x'} \to \innerprod x {x'}$ for each $x' \in X'$.

Proof:
For each $x' \in X'$, define $f_{x'} : X \to \GF$ by:
:$\map {f_{x'} } x = \innerprod x {x'}$ for each $x \in X$. 
Let $F = \set {f_{x'} : x' \in X'}$.
By the definition of the weak topology on $X$ induced by $\innerprod X {X'}$, $\map \sigma {X, X'}$ is the initial topology on $X$ induced by $F$.
By Characterization of Convergence of Net in Initial Topology, we have $x_\lambda \to x$ {{iff}}:
:$\map {f_{x'} } {x_\lambda} \to \map {f_{x'} } x$ for each $x' \in X'$.
That is:
:$\innerprod {x_\lambda} {x'} \to \innerprod x {x'}$ for each $x' \in X'$.
{{qed}}
Category:Weak Topologies Induced by Dual Systems
Category:Nets (Set Theory)
tcq1p4cssp699bccg0mbgqmcgb24xfj
Theorem: Open Set in Initial Topology on Vector Space Induced by Linear Functionals

Let $\GF \in \set {\R, \C}$.
Let $E$ be a vector space over $\GF$.
Let $E^\#$ be the algebraic dual of $E$.
Let $F \subseteq E^\#$ be a vector subspace.
Let $\tau$ be the initial topology on $E$ induced by $F$.
Let $U \subseteq E$. 
Then $U$ is open in $\struct {X, \tau}$ {{iff}} for each $x \in X$ there exists $\epsilon > 0$ and $f_1, \ldots, f_n \in F$ such that:
:$\set {y \in X : \cmod {\map {f_i} x - \map {f_i} y} < \epsilon \text { for each } 1 \le i \le n} \subseteq U$

Proof:
From Initial Topology on Vector Space Generated by Linear Functionals is Locally Convex, $\tau$ is generated by the seminorms: 
:$\set {p_f : f \in F}$
where we define $p_f : X \to \R_{\ge 0}$ by:
:$\map {p_f} x = \cmod {\map f x}$
for each $x \in X$.
Then, from Open Sets in Standard Topology of Locally Convex Space, $U$ is open in $\struct {X, \tau}$ {{iff}} for each $x \in X$ there exists $\epsilon > 0$ and $f_1, \ldots, f_n \in F$ such that:
:$\set {y \in X : \map {p_{f_i} } {x - y} < \epsilon \text { for each } 1 \le i \le n} \subseteq U$
that is:
:$\set {y \in X : \cmod {\map {f_i} {x - y} } < \epsilon \text { for each } 1 \le i \le n} \subseteq U$
Since each $f_i$ is linear, this is to say:
:$\set {y \in X : \cmod {\map {f_i} x - \map {f_i} y} < \epsilon \text { for each } 1 \le i \le n} \subseteq U$
{{qed}}
Category:Initial Topology
886j2v23omof6gngv2iidv4w08brcoo
Theorem: Characterization of von Neumann-Boundedness in Weak Topology Induced by Dual System

Let $\GF \in \set {\R, \C}$.
Let $\innerprod X {X'}$ be a dual system over $\GF$.
Let $\map \sigma {X, X'}$ be the weak topology on $X$ induced by $X'$.
Let $E \subseteq X$.
Then $E$ is von Neumann-bounded in $\struct {X, \map \sigma {X, X'} }$ {{iff}} for each $x' \in X'$ we have:
:$\ds \sup_{x \mathop \in E} \cmod {\innerprod x {x'} } < \infty$

Proof:
For each $x' \in X'$, define $f_{x'} : X \to \GF$ by:
:$\map {f_{x'} } x = \innerprod x {x'}$ for each $x \in X$.
Let $F = \set {f_{x'} : x' \in X'}$.
By the definition of the weak topology on $X$ induced by $X'$, $\map \sigma {X, X'}$ is the initial topology on $X$ generated by $F$.
By Characterization of von Neumann-Boundedness in Initial Topology on Vector Space Induced by Linear Functionals, $E$ is von Neumann-bounded in $\struct {X, \map \sigma {X, X'} }$ {{iff}} for each $x' \in X'$ we have:
:$\ds \sup_{x \mathop \in E} \cmod {\map {f_{x'} } x } < \infty$
That is:
:$\ds \sup_{x \mathop \in E} \cmod {\innerprod x {x'} } < \infty$
{{qed}}
Category:Von Neumann-Bounded Subsets of Topological Vector Spaces
Category:Dual Systems
q8l7mu2d36kz34fjaz1kvqfm5o38717
Theorem: Characterization of von Neumann-Boundedness in Weak-* Topology Induced by Dual System

Let $\GF \in \set {\R, \C}$.
Let $\innerprod X {X'}$ be a dual system over $\GF$.
Let $\map \sigma {X', X}$ be the weak topology on $X'$ induced by $X$.
Let $E' \subseteq X'$.
Then $E'$ is von Neumann-bounded in $\struct {X', \map \sigma {X', X} }$ {{iff}} for each $x \in X$ we have:
:$\ds \sup_{x' \mathop \in E'} \cmod {\innerprod x {x'} } < \infty$

Proof:
For each $x \in X$, define $\pi_x : X' \to K$ by:
:$\map {\pi_x} {x'} = \innerprod x {x'}$ for each $x \in X$.
Let:
:$F = \set {\pi_x : x \in X}$
By the definition of the weak topology on $X'$ induced by $\innerprod X {X'}$, $\map \sigma {X', X}$ is the initial topology on $X$ generated by $F$.
By Characterization of von Neumann-Boundedness in Initial Topology on Vector Space Induced by Linear Functionals, $E'$ is von Neumann-bounded in $\struct {X', \map \sigma {X', X} }$ {{iff}} for each $x' \in X'$ we have:
:$\ds \sup_{x' \mathop \in E'} \cmod {\map {\pi_x} {x'} } < \infty$
That is:
:$\ds \sup_{x' \mathop \in E'} \cmod {\innerprod x {x'} } < \infty$
for each $x \in X$.
{{qed}}
Category:Von Neumann-Bounded Subsets of Topological Vector Spaces
Category:Dual Systems
dzjrhnh8sk1fq8ynifojxojra1zzk2y
Theorem: Transpose of Dual System is Dual System

Let $K$ be a field.
Let $\innerprod E F_{E \times F}$ be a dual system over $K$.
Define a mapping $\innerprod \cdot \cdot_{F \times E} : F \times E \to K$ by:
:$\innerprod f x_{F \times E} = \innerprod x f_{E \times F}$
Then $\innerprod F E_{F \times E}$ is a dual system over $K$.

Proof:
By Transpose of Bilinear Mapping is Bilinear Mapping, $\innerprod \cdot \cdot_{F \times E}$ is a bilinear mapping.
Suppose that $f_0 \in F$ is such that:
:$\innerprod {f_0} x_{F \times E} = {\mathbf 0}_K$
for each $x \in E$.
Then we have:
:$\innerprod x {f_0}_{E \times F} = {\mathbf 0}_K$
Since $\innerprod \cdot \cdot_{E \times F}$ is a dual system, we have:
:$f_0 = {\mathbf 0}_F$
Now suppose that $x_0 \in E$ is such that:
:$\innerprod f {x_0}_{F \times E} = {\mathbf 0}_K$
for each $f \in F$.
Then we have:
:$\innerprod {x_0} f_{E \times F} = {\mathbf 0}_K$
Since $\innerprod \cdot \cdot_{E \times F}$ is a dual system, we have:
:$x_0 = {\mathbf 0}_E$
{{qed}}
Category:Dual Systems
4llu34vq21o5g1m6n08sbv9wnenex5f
Theorem: Absolute Prepolar is Absolute Polar in Transpose

Let $\GF \in \set {\R, \C}$.
Let $\innerprod E F_{E \times F}$ be a dual system over $\GF$.
Let $\innerprod F E_{F \times E}$ be the transpose dual system.
Let $B \subseteq F$ be a non-empty set.
Let $B_\circ$ be the absolute prepolar of $B$ taken in $\innerprod E F_{E \times F}$.
Let $B^{\circ^T}$ be the absolute polar of $B$ taken in $\innerprod F E_{F \times E}$. 
Then we have:
:$B_\circ = B^{\circ^T}$

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = B_\circ
		| r = \set {x \in E : \cmod {\innerprod x f_{E \times F} } \le 1 \text { for all } f \in B}
}}
{{eqn	| r = \set {x \in E : \cmod {\innerprod f x_{F \times E} } \le 1 \text { for all } f \in B}
}}
{{eqn	| r = B^{\circ^T}
}}
{{end-eqn}}
{{qed}}
Category:Absolute Polars
Category:Absolute Prepolars
dpylhwj9fmzvfkq0sbbbkjys7sr65tk
Theorem: Weak Topology on Transpose Dual System is Weak-* Topology on Original System

Let $\GF \in \set {\R, \C}$.
Let $\innerprod E F_{E \times F}$ be a dual system over $\GF$.
Let $\innerprod F E_{F \times E}$ be the transpose of $\innerprod E F_{E \times F}$.
Let $\tau_1$ be the weak topology on $F$ induced by $\innerprod F E_{F \times E}$. 
Let $\tau_2$ be the weak-$\ast$ topology on $F$ induced by $\innerprod E F_{E \times F}$. 
Then $\tau_1 = \tau_2$. 
Hence, we can use the notation $\map \sigma {F, E}$ for both topologies without confusion.

Proof:
For each $x \in E$, define the mapping $g_x : F \to K$ by:
:$\map {g_x} f = \innerprod f x_{F \times E} = \innerprod x f_{E \times F}$ for each $\tuple {f, x} \in F \times E$.
By the definition of the weak topology on $F$, $\tau_1$ is the initial topology induced by $\set {g_x : x \in E}$.
For each $x \in E$, define a mapping $\pi_x : F \to K$ by:
:$\map {\pi_x} f = \innerprod x f_{E \times F}$ for each $\tuple {f, x} \in E \times F$.
By the definition of the weak-$\ast$ topology on $F$, $\tau_2$ is the initial topology induced by $\set {\pi_x : x \in E}$.
We have $g_x = \pi_x$ for each $x \in E$, and hence $\tau_1 = \tau_2$.
{{qed}}
Category:Weak Topologies Induced by Dual Systems
Category:Weak-* Topologies Induced by Dual Systems
llwtmyb3invdpjj8darri5clf9j7zcb
Theorem: Bipolar Set contains Original Set

Let $\GF \in \set {\R, \C}$.
Let $\innerprod X {X'}$ be a dual system over $\GF$.
Let $A \subseteq X$ be a non-empty set.
Let $\paren {A^\circ}_\circ$ be the bipolar of $A$.
Then:
:$A \subseteq \paren {A^\circ}_\circ$

Proof:
We have $x \in \paren {A^\circ}_\circ$ {{iff}}:
:$\cmod {\innerprod x f} \le 1$ for each $f \in A^\circ$.
We have that $f \in A^\circ$ {{iff}}:
:$\cmod {\innerprod x f} \le 1$ for each $x \in A$. 
Hence for $x \in A$, we have:
:$\cmod {\innerprod x f} \le 1$ for each $f \in A^\circ$.
Hence $x \in \paren {A^\circ}_\circ$.
{{qed}}
Category:Bipolar Sets
nkw2pk99oxixym6gbhuznkcrc46wima
Theorem: Equivalence of Definitions of Boolean Lattice/Definition 2 implies Definition 1

Let $\struct {S, \vee, \wedge, \neg}$ be a Boolean algebra.
Let $\struct {S, \vee, \wedge, \preceq}$ be an ordered structure.
Suppose that:
:$\forall a, b \in S: a \wedge b \preceq a \vee b$
Then, $\struct {S, \vee, \wedge, \preceq}$ is a complemented distributive lattice.

Proof:
By axiom $\paren {\text {BA}_1 3}$, let $\bot, \top \in S$ denote the identities of $\vee$ and $\wedge$, respectively.
We will first show that $\struct {S, \vee, \wedge, \preceq}$ is a lattice.
By definition 2, we must prove that, for all $a, b \in S$:
:$a \vee b$ is the join of $a$ and $b$
:$a \wedge b$ is the meet of $a$ and $b$
We have:
{{begin-eqn}}
{{eqn | l = \bot
      | r = a \wedge \bot
      | c = Identities of Boolean Algebra are also Zeroes
}}
{{eqn | o = \preceq
      | r = a \vee \bot
      | c = {{hypothesis}}
}}
{{eqn | r = a
      | c = {{Defof|Identity Element}}
}}
{{eqn | ll = \leadsto
      | l = b
      | r = \bot \vee b
      | c = {{Defof|Identity Element}}
}}
{{eqn | o = \preceq
      | r = a \vee b
      | c = {{Defof|Ordered Structure}}, by the above
}}
{{end-eqn}}
That is, applying axiom $\paren {\text {BA}_1 1}$:
:$\forall a, b \in S: a, b \preceq a \vee b$
Now, fix $c \in S$ such that:
:$a, b \preceq c$
Then:
{{begin-eqn}}
{{eqn | l = a \vee b
      | o = \preceq
      | r = a \vee c
      | c = {{Defof|Ordered Structure}}
}}
{{eqn | o = \preceq
      | r = c \vee c
      | c = {{Defof|Ordered Structure}}
}}
{{eqn | r = c
      | c = Operations of Boolean Algebra are Idempotent
}}
{{end-eqn}}
Therefore, $a \vee b$ is the join of $a$ and $b$ in $\struct {S, \preceq}$.
By a dual argument, $a \wedge b$ is the meet of $a$ and $b$ in $\struct {S, \preceq}$.
We have now shown that $\struct {S, \vee, \wedge, \preceq}$ is a lattice.
Since $\bot, \top \in S$ are identities of $\vee$ and $\wedge$, we have that $\struct {S, \vee, \wedge, \preceq}$ is a bounded lattice by definition.
By axiom $\paren {\text {BA}_1 4}$, $\struct {S, \vee, \wedge, \preceq}$ is a complemented lattice.
Finally, by axiom $\paren {\text {BA}_1 2}$, $\struct {S, \vee, \wedge, \preceq}$ is a distributive lattice.
The result follows.
{{qed}}
Theorem: Boolean Lattice as Boolean Algebra

Let $\struct {S, \vee, \wedge, \preceq}$ be a Boolean lattice by definition $1$.
Then, there is a unique unary operation:
:$\neg : S \to S$
such that $\struct {S, \vee, \wedge, \neg}$ forms a Boolean algebra.
In particular, for each $a \in S$, we will have $\neg a$ be the complement of $a$.

Proof:
Let $\neg a$ be defined as the unique complement of $a$ in $S$, if such an element exists.
By definition of a lattice, $a \vee b$ and $a \wedge b$ are defined in $S$ for all $a, b \in S$.
Moreover, by Complement in Boolean Lattice is Unique, $\neg a$ exists in $S$ for every $a \in S$.
So, axiom $\paren {\text {BA}_1 0}$ holds for $\struct {S, \vee, \wedge, \neg}$.
By:
:Join is Commutative
:Meet is Commutative
axiom $\paren {\text {BA}_1 1}$ holds.
By definition of a distributive lattice, axiom $\paren {\text {BA}_1 2}$ holds.
By definition of a bounded lattice, axiom $\paren {\text {BA}_1 3}$ holds.
Finally, by definition of a complement, axiom $\paren {\text {BA}_1 4}$ holds.
{{qed|lemma}}
Now, let $\neg' : S \to S$ also form a Boolean algebra as $\struct {S, \vee, \wedge, \neg'}$.
Then, by axiom $\paren {\text {BA}_1 4}$, $\neg' a$ is the complement of $a$ for every $a \in S$.
Therefore, since this complement is unique:
:$\neg' a = \neg a$
and so $\neg$ is the unique unary operation such that:
:$\struct {S, \vee, \wedge, \neg}$ forms a Boolean algebra.
{{qed}}
Category:Boolean Algebra is Equivalent to Boolean Lattice
Category:Boolean Algebras
Category:Boolean Lattices
p3e8grqjk8scb2w66fvq0o9353v85x3
Theorem: Equivalence of Definitions of Boolean Lattice/Definition 1 implies Definition 3

Let $\struct {S, \vee, \wedge, \preceq}$ be a complemented distributive lattice.
Then, there is a unary operation $\neg$ on $S$ such that:
:$\paren 1: \quad \forall a, b \in S: a \preceq \neg b \iff a \wedge b = \bot$
:$\paren 2: \quad \forall a \in S: \neg \neg a = a$

Proof:
Fix $a, b \in S$, and suppose that $a \preceq \neg b$.
Then, by Meet Precedes Operands:
:$a \wedge b \preceq a \preceq \neg b$
:$a \wedge b \preceq b$
so by definition of meet:
:$a \wedge b \preceq \neg b \wedge b$
Since $\neg b$ is the complement of $b$:
:$\neg b \wedge b = \bot$
hence:
:$a \wedge b \preceq \bot$
But as $\bot$ is the bottom, it is the smallest element, so:
:$\bot \preceq a \wedge b$
Therefore:
:$a \wedge b = \bot$
Now, fix $a, b \in S$, and suppose that $a \wedge b = \bot$.
Then:
{{begin-eqn}}
{{eqn | l = a
      | o = \preceq
      | r = a \vee \neg b
      | c = Join Succeeds Operands
}}
{{eqn | r = \paren {a \vee \neg b} \wedge \top
      | c = {{Defof|Top of Lattice|index = 2}}
}}
{{eqn | r = \paren {a \vee \neg b} \wedge \paren {b \vee \neg b}
      | c = {{Defof|Complement (Lattice Theory)|Complement}}
}}
{{eqn | r = \paren {a \wedge b} \vee \neg b
      | c = {{Defof|Distributive Lattice|index = 2}}
}}
{{eqn | r = \bot \vee \neg b
      | c = {{hypothesis}}
}}
{{eqn | r = \neg b
      | c = {{Defof|Bottom of Lattice|index = 2}}
}}
{{end-eqn}}
Hence:
:$a \preceq \neg b \iff a \wedge b = \bot$
which is to say that $\paren 1$ holds.
{{qed|lemma}}
Finally, by Complement in Boolean Algebra is Unique, $\struct {S, \vee, \wedge, \preceq}$ is a uniquely complemented lattice.
Therefore, by Complement of Complement in Uniquely Complemented Lattice, $\paren 2$ holds.
{{qed}}
Theorem: Mass of Body with given Density

Let $\BB$ be a body occupying a region $V$ of space.
Let $\map \rho {\mathbf r}$ denote the (mass) density of $\BB$ at the point within $V$ whose position vector is $\mathbf r$.
Then the mass $m$ of $\BB$ is given by:
:$m = \ds \int_V \map \rho {\mathbf r} \rd V$

Proof:
To find the total mass of $\BB$, divide it into many finite regions $\set {\Delta \BB_i}$ each with a volume $\Delta V_i$.
Within each $\Delta \BB_i$, choose a point $\mathbf r_i$.
Let the density of $\Delta \BB_i$ be uniform and given by $\map \rho {\mathbf r_i}$.
Thus, the mass of $\Delta \BB_i$ is:
:$\Delta m_i = \map \rho {\mathbf r_i} \Delta V_i$.
The total mass of $\BB$ is the sum of the masses of $\set {\Delta \BB_i}$:
{{begin-eqn}}
{{eqn | o = \approx
      | l = m
      | r = \sum_i \Delta m_i
}}
{{eqn | r = \sum_i \map \rho {\mathbf r_i} \Delta V_i
}}
{{end-eqn}}
The exact mass is found by taking the limit as norm $\norm {\Delta V_i} \to 0$.
{{begin-eqn}}
{{eqn | l = m
      | r = \lim_{\norm {\Delta V_i} \mathop \to 0} \sum_i \map \rho {\mathbf r_i} \Delta V_i
}}
{{eqn | r = \int_V \map \rho {\mathbf r} \rd V
      | c = 
}}
{{end-eqn}}
{{qed}}
{{Questionable|This argument uses Riemann integral language to convert the summation into an integral, which may not be correct.}}
Theorem: Expression for Balanced Hull

Let $\GF \in \set {\R, \C}$.
Let $X$ be a vector space over $\GF$.
Let $A \subseteq X$ be non-empty..
Then the balanced hull $\map {\operatorname {bal} } A$ is well-defined and:
:$\ds \map {\operatorname {bal} } A = \bigcup_{\lambda \in \GF : \cmod \lambda \le 1} \lambda A$

Proof:
We first show that:
:$\ds B = \bigcup_{\lambda \in \GF : \cmod \lambda \le 1} \lambda A$
is a balanced set containing $A$.
Let $x \in B$ and $\mu \in \GF$ be such that $\cmod \mu \le 1$. 
Since $x \in B$, there exists $\lambda \in \GF$ with $\cmod \lambda \le 1$ and $y \in A$ such that $x = \lambda y$.
Then $\mu x = \lambda \mu y$.
We have $\cmod {\lambda \mu} \le \cmod \mu \le 1$. 
Hence $\mu x \in B$ for $\cmod \mu \le 1$. 
Hence $B$ is balanced set.
Further, since $1 \in \GF$ and $\cmod 1 \le 1$, we have $A \subseteq B$.
We now show that every balanced set containing $A$ also contains $B$.
Let $C \subseteq X$ be a balanced set containing $A$.
Let $x \in A$ and $\lambda \in \GF$ have $\cmod \lambda \le 1$.
Then $x \in C$ and hence $\lambda x \in C$ since $C$ is balanced. 
Hence $\lambda A \subseteq B$ for $\cmod \lambda \le 1$. 
Hence:
:$\ds B = \bigcup_{\lambda \in \GF : \cmod \lambda \le 1} \lambda A \subseteq C$ 
Hence:
:$\ds B = \bigcup_{\lambda \in \GF : \cmod \lambda \le 1} \lambda A$
is the $\subseteq$-smallest balanced set containing $A$.
Hence the balanced hull $\map {\operatorname {bal} } A$ is well-defined and:
:$\ds \map {\operatorname {bal} } A = \bigcup_{\lambda \in \GF : \cmod \lambda \le 1} \lambda A$
{{qed}}
Category:Balanced Sets
24sywvmwkxr19tug7ai0265jc12khh2
Theorem: Balanced Hull is Intersection of Balanced Sets containing Set

Let $\GF \in \set {\R, \C}$.
Let $X$ be a vector space over $\GF$.
Let $A \subseteq X$ be a non-empty set.
Let $\map {\operatorname {bal} } A$ be the balanced hull of $A$.
Then:
:$\ds \map {\operatorname {bal} } A = \bigcap \set {B \supseteq A: B \text { is balanced} }$

Proof:
Note that:
:$\map {\operatorname {bal} } A \in \set {B \supseteq A: B \text { is balanced} }$
and hence:
:$\set {B \supseteq A: B \text { is balanced} } \ne \O$
Hence:
:$\ds \bigcap \set {B \supseteq A: B \text { is balanced} }$ is well-defined.
Further, from Intersection of Balanced Sets in Vector Space is Balanced, we have that:
:$\ds \bigcap \set {B \supseteq A: B \text { is balanced} } \supseteq A$ is balanced.
Since $\map {\operatorname {bal} } A$ is $\subseteq$-smallest among the balanced sets containing $A$, we have:
:$\ds \map {\operatorname {bal} } A = \bigcap \set {B \supseteq A: B \text { is balanced} }$
{{qed}}
Category:Balanced Sets
mx85ddjf8tpoeyzjb9fieapcrl1vtpk
Theorem: Convex Hull of Balanced Set is Balanced

Let $\GF \in \set {\R, \C}$.
Let $X$ be a vector space over $\GF$.
Let $B \subseteq X$ be a balanced set.
Let $\map {\operatorname {conv} } B$ be the convex hull of $B$.
Then $\map {\operatorname {conv} } B$ is balanced.

Proof:
Let $x \in \map {\operatorname {conv} } B$ and $\lambda \in \GF$ have $\cmod \lambda \le 1$. 
Then there exists $x_1, \ldots, x_n \in B$ and $t_1, \ldots, t_n \in \closedint 0 1$ such that:
:$\ds x = \sum_{j \mathop = 1}^n t_j x_j$
Then:
:$\ds \lambda x = \sum_{j \mathop = 1}^n t_j \paren {\lambda x_j}$
Since $B$ is balanced, we have $\lambda x_j \in B$ for each $1 \le j \le n$. 
Hence we have $\lambda x \in \map {\operatorname {conv} } B$.
Hence $\map {\operatorname {conv} } B$ is balanced.
{{qed}}
Category:Convex Sets (Vector Spaces)
Category:Balanced Sets
bwgkm42z93imq8m6xn0tdy9q14kis49
Theorem: Convex Balanced Hull is Intersection of all Convex Balanced Sets containing Set

Let $\GF \in \set {\R, \C}$.
Let $X$ be a vector space over $\GF$.
Let $A \subseteq X$ be a non-empty set.
Let $\map {\operatorname {cobal} } A$ be the convex balanced hull of $A$.
We then have:
:$\ds \map {\operatorname {cobal} } A = \bigcap \set {C \supseteq A : C \text { is convex and balanced} }$

Proof:
Let:
:$\ds B = \bigcap \set {C \supseteq A : C \text { is convex and balanced} }$
From Convex Hull of Balanced Set is Balanced, the convex hull of the balanced hull of $A$, $\map {\operatorname {conv} } {\map {\operatorname {bal} } A}$ is balanced.
Hence:
:$\set {C \supseteq A : C \text { is convex and balanced} } \ne \O$
From Intersection of Convex Sets is Convex Set (Vector Spaces), $B$ is convex.
From Intersection of Balanced Sets in Vector Space is Balanced, $B$ is balanced.
Further, if $C \supseteq A$ is convex and balanced, we have $C \supseteq B$. 
Hence from the definition of the convex balanced hull, we have that $\map {\operatorname {cobal} } A = B$.
{{qed}}
Category:Convex Balanced Hulls
q177zdr1cgeiaum5jktv09u2je627sq
Theorem: Absolute Prepolar is Non-Empty

Let $\GF \in \set {\R, \C}$.
Let $\innerprod E F$ be a dual system over $\GF$.
Let $B \subseteq F$ be non-empty. 
Let $B_\circ$ be the absolute prepolar of $B$.
Then $B_\circ \ne \O$.

Proof:
Since $\innerprod \cdot \cdot$ is bilinear, we have $\innerprod { {\mathbf 0}_E} f = 0$ for each $f \in F$.
In particular, we have $\innerprod { {\mathbf 0}_E} f = 0$ for each $f \in B$.
Hence ${\mathbf 0}_E \in B_\circ$, hence $B_\circ \ne \O$.
{{qed}}
Category:Absolute Prepolars
cpzv07ghkmaalp1dz3n48s0870kn6d4
Theorem: Absolute Prepolar is Convex Set

Let $\GF \in \set {\R, \C}$.
Let $\innerprod E F$ be a dual system over $\GF$.
Let $B \subseteq F$ be non-empty. 
Let $B_\circ$ be the absolute prepolar of $B$.
Then $B_\circ$ is convex.

Proof:
Let $x, y \in B_\circ$ and $t \in \closedint 0 1$.
Then:
:$\cmod {\innerprod x f} \le 1$
and:
:$\cmod {\innerprod y f} \le 1$
for all $f \in B$.
We now have:
{{begin-eqn}}
{{eqn	| l = \cmod {\innerprod {t x + \paren {1 - t} y} f}
		| r = \cmod {t \innerprod x f + \paren {1 - t} \innerprod y f}
		| c = $\innerprod \cdot \cdot$ is bilinear
}}
{{eqn	| o = \le
		| r = t \cmod {\innerprod x f} + \paren {1 - t} \cmod {\innerprod y f}
		| c = Triangle Inequality: Complex Numbers
}}
{{eqn	| o = \le
		| r = t + \paren {1 - t}
}}
{{eqn	| r = 1
}}
{{end-eqn}}
for all $f \in B$.
Hence:
:$t x + \paren {1 - t} y \in B_\circ$
{{qed}}
Category:Absolute Prepolars
Category:Convex Sets (Vector Spaces)
5a9ey6h2f0107qdj9pykr3xntil5gtx
Theorem: Absolute Prepolar is Balanced

Let $\GF \in \set {\R, \C}$.
Let $\innerprod E F$ be a dual system over $\GF$.
Let $B \subseteq F$ be non-empty. 
Let $B_\circ$ be the absolute prepolar of $B$.
Then $B_\circ$ is balanced.

Proof:
Let $x \in B_\circ$ and $\lambda \in \GF$ have $\cmod \lambda \le 1$.
Then, for each $f \in B$, we have:
{{begin-eqn}}
{{eqn	| l = \cmod {\innerprod {\lambda x} f}
		| r = \cmod \lambda \cmod {\innerprod x f}
}}
{{eqn	| o = \le
		| r = \cmod {\innerprod x f}
}}
{{eqn	| o = \le
		| r = 1
}}
{{end-eqn}}
Hence $\lambda x \in B_\circ$.
{{qed}}
Category:Absolute Prepolars
Category:Balanced Sets
c791neu2b87cdwngizyp14kvgeu18lm
Theorem: Absolute Prepolar is Closed in Weak Topology

Let $\GF \in \set {\R, \C}$.
Let $\innerprod E F$ be a dual system over $\GF$.
Let $\map \sigma {E, F}$ be the weak-$\ast$ topology on $F$ induced by $\innerprod E F$.
Let $B \subseteq E$ be non-empty. 
Let $B_\circ$ be the absolute prepolar of $B$.
Then $B_\circ$ is $\map \sigma {E, F}$-closed.

Proof:
We use Characterization of Closedness in terms of Nets.
That is, we show that every convergent net valued in $B_\circ$ has its limit in $B_\circ$. 
Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ be a convergent net valued in $B_\circ$ with limit $x$.
We show that $x \in B_\circ$.
We have:
:$\cmod {\innerprod {x_\lambda} f} \le 1$ for each $f \in B$.
By Characterization of Convergence of Net in Weak Topology Induced by Dual System, we have:
:$\innerprod {x_\lambda} f \to \innerprod x f$ for each $f \in B$.
Hence:
:$\cmod {\innerprod x f} \le 1$ for each $f \in B$.
Hence $x \in B_\circ$.
{{qed}}
Category:Absolute Prepolars
Category:Weak Topologies Induced by Dual Systems
fr7cfh6b5fkt4x34n89h02mrhbqzhrd