avewright/proofwiki-math huggingface dataset:
Theorem: Coslice Category is Isomorphic to Comma Category/Lemma 1

:$I$ is a covariant functor

Proof:
=== Object Functor is Well-defined ===
Let $f$ be an object in $C / \mathbf C$.
By definition of coslice category:
:$f$ is a morphism $f: C \to D$ of $\mathbf C$
By definition of identity functor:
:$\operatorname{id}_{\mathbf C} D = D$
Hence:
:$f$ is a morphism $f: G* \to \operatorname{id}_{\mathbf C} D$ of $\mathbf C$
By definition of comma category:
:$\tuple{*, D, f}$ is an object in $\paren{G \downarrow \operatorname{id}_{\mathbf C}}$
It follows that $I$ is a well-defined object functor.
{{qed|lemma}}
Theorem: Coslice Category is Isomorphic to Comma Category/Lemma 2

:$J$ is a covariant functor

Proof:
=== Object Functor is Well-defined ===
By definition of category $\mathbf 1$:
:the only object in $\mathbf 1$ is $*$
By definition of comma category:
:every object in $\paren{G \downarrow \operatorname{id}_{\mathbf C}}$ is of the form $\tuple{*, D, f}$ where:
::$*$ is in $\mathbf 1$
::$D$ is an object of $\mathbf D$
::$f$ is a morphism $f:G* \to  \operatorname{id}_{\mathbf C} D$ of $\mathbf C$
By definition of $G$:
:$G* = C$
By definition of identity functor:
:$\operatorname{id}_{\mathbf C} D = D$
Hence:
:$f$ is a morphism $f:C \to  D$ of $\mathbf C$
By definition of coslice category:
:$f$ is an object in $C / \mathbf C$
It follows that $J$ is a well-defined object functor.
{{qed|lemma}}
Theorem: Coslice Category is Isomorphic to Comma Category/Lemma 3

:$J \circ I = \operatorname{id}_{C / \mathbf C}$
where $\operatorname{id}_{C / \mathbf C}$ is the identity functor on $C / \mathbf C$

Proof:
For each object $f$ in $C / \mathbf C$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J \circ I} f
      | r = \map J {I f }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J \tuple{*, \operatorname{cod} f, f}
      | c = Definition of $I$
}}
{{eqn | r = f
      | c = Definition of $J$
}}
{{eqn | r = \operatorname{id}_{C / \mathbf C} f
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
For each morphism $h: f \to f'$ in $C / \mathbf C$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J \circ I} h
      | r = \map J {I h }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J \tuple{\operatorname{id}_*, h}
      | c = Definition of $I$
}}
{{eqn | r = h
      | c = Definition of $J$
}}
{{eqn | r = \operatorname{id}_{C / \mathbf C} h
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
It follows that:
:$J \circ I = \operatorname{id}_{C / \mathbf C}$
{{qed}}
Category:Coslice Category is Isomorphic to Comma Category
slkd90u8hkwle22ld2kbd3niea3j0sy
Theorem: Coslice Category is Isomorphic to Comma Category/Lemma 4

:$I \circ J = \operatorname{id}_{\paren{G \downarrow \operatorname{id}_{\mathbf C} }}$
where $\operatorname{id}_{\paren{G \downarrow \operatorname{id}_{\mathbf C} }}$ is the identity functor on $\paren{G \downarrow \operatorname{id}_{\mathbf C} }$

Proof:
By definition of comma category:
:For each object $\tuple{*, D, f}$ in $\paren{G \downarrow \operatorname{id}_{\mathbf C} }$:
::$\text{(1)} \quad \operatorname{cod} f = D$
For each object $\tuple{*, D,f}$ in $\paren{G \downarrow \operatorname{id}_{\mathbf C} }$ we have:
{{begin-eqn}}
{{eqn | l = \paren{I \circ J} \tuple{*, D, f}
      | r = \map I {J \tuple{*, D, f} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = I f
      | c = Definition of $J$
}}
{{eqn | r = \tuple{*, \operatorname{cod} f, f}
      | c = Definition of $I$
}}
{{eqn | r = \tuple{*, D, f}
      | c = by $\text{(1)}$
}}
{{eqn | r = \operatorname{id}_{\paren{G \downarrow \operatorname{id}_{\mathbf C} } } \tuple{*, D, f}
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
For each morphism $\tuple{\operatorname{id}_*, h}: \tuple{*, D,f} \to \tuple{*, D',f'}$ in $\paren{G \downarrow F}$ we have:
{{begin-eqn}}
{{eqn | l = \paren{I \circ J} \tuple{\operatorname{id}_*, h}
      | r = \map I {J \tuple{\operatorname{id}_*, h} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = I h
      | c = Definition of $J$
}}
{{eqn | r = \tuple{\operatorname{id}_*, h}
      | c = Definition of $I$
}}
{{eqn | r = \operatorname{id}_{\paren{G \downarrow \operatorname{id}_{\mathbf C} } } \tuple{\operatorname{id}_*, h}
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
It follows that:
:$I \circ J = \operatorname{id}_{\paren{G \downarrow \operatorname{id}_{\mathbf C} } }$
{{qed}}
Category:Coslice Category is Isomorphic to Comma Category
sq1rkkw72hrxwnbjey60u3wzdvsqwk5
Theorem: Morphism Category is Isomorphic to Comma Category/Lemma 1

:$I$ is a covariant functor

Proof:
=== Object Functor is Well-defined ===
Let $f$ be an object in $\mathbf C^\to$.
By definition of morphism category:
:$f$ is a morphism $f: \operatorname{dom} f \to \operatorname{cod} f$ of $\mathbf C$
By definition of identity functor:
:$\map {\operatorname{id}_{\mathbf C} } {\operatorname{dom} f} = \operatorname{dom} f$
and:
:$\map {\operatorname{id}_{\mathbf C} } {\operatorname{cod} f} = \operatorname{cod} f$
Hence:
:$f$ is a morphism $f: \map {\operatorname{id}_{\mathbf C} } {\operatorname{dom} f} \to \map {\operatorname{id}_{\mathbf C} } {\operatorname{cod} f}$ of $\mathbf C$
By definition of comma category:
:$\tuple{\operatorname{dom} f, \operatorname{cod} f, f}$ is an object in $\paren{\operatorname{id}_{\mathbf C} \downarrow \operatorname{id}_{\mathbf C}}$
It follows that $I$ is a well-defined object functor.
{{qed|lemma}}
Theorem: Morphism Category is Isomorphic to Comma Category/Lemma 2

:$J$ is a covariant functor

Proof:
=== Object Functor is Well-defined ===
By definition of comma category:
:every object in $\paren{\operatorname{id}_{\mathbf C} \downarrow \operatorname{id}_{\mathbf C} }$ is of the form $\tuple{E, D, f}$:
:$f$ is a morphism $f : \operatorname{id}_{\mathbf C} E \to \operatorname{id}_{\mathbf C} D$ in $\mathbf C$
By definition of identity morphism:
:$\operatorname{id}_{\mathbf C} D = D$
and:
:$\operatorname{id}_{\mathbf C} E = E$
Hence given an object $\tuple{E, D, f}$ in $\paren{\paren{\operatorname{id}_{\mathbf C} \downarrow \operatorname{id}_{\mathbf C} } }$:
:$f$ is a morphism $f:E \to  D$ of $\mathbf C$
By definition of morphism category:
:$f$ is an object in $\mathbf C^\to$
It follows that $J$ is a well-defined object functor.
{{qed|lemma}}
Theorem: Morphism Category is Isomorphic to Comma Category/Lemma 3

:$J \circ I = \operatorname{id}_{\mathbf C^\to}$
where $\operatorname{id}_{\mathbf C^\to}$ is the identity functor on $\mathbf C^\to$

Proof:
For each object $g$ in $\mathbf C^\to$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J \circ I} g
      | r = \map J {I g }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J \tuple{\operatorname {dom} g, \operatorname {cod} g, g}
      | c = Definition of $I$
}}
{{eqn | r = g
      | c = Definition of $J$
}}
{{eqn | r = \map {\operatorname{id}_{\mathbf C^\to} } g
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
For each morphism $\tuple{k, h}: g \to g'$ in $\mathbf C^\to$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J \circ I} \tuple{k, h}
      | r = \map J {I \tuple{k, h} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J \tuple{k, h}
      | c = Definition of $I$
}}
{{eqn | r = \tuple{k, h}
      | c = Definition of $J$
}}
{{eqn | r = \operatorname{id}_{\mathbf C^\to} \tuple{k, h}
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
It follows that:
:$J \circ I = \operatorname{id}_{\mathbf C^to}$
{{qed}}
Category:Morphism Category is Isomorphic to Comma Category
0zyt1xw7j62o3mx01mg7f41e2f9fdct
Theorem: Morphism Category is Isomorphic to Comma Category/Lemma 4

:$I \circ J = \operatorname{id}_{\paren{\operatorname{id}_{\mathbf C} \downarrow \operatorname{id}_{\mathbf C} }}$
where $\operatorname{id}_{\paren{\operatorname{id}_{\mathbf C} \downarrow \operatorname{id}_{\mathbf C} }}$ is the identity functor on $\paren{\operatorname{id}_{\mathbf C} \downarrow \operatorname{id}_{\mathbf C} }$

Proof:
By definition of comma category:
:For each object $\tuple{E, D, g}$ in $\paren{\operatorname{id}_{\mathbf C} \downarrow \paren{\operatorname{id}_{\mathbf C}}}$:
::$\text{(1)} \quad \operatorname{dom} g = E$
::$\text{(2)} \quad \operatorname{cod} g = D$
For each object $\tuple{E, D, g}$ in $\paren{\operatorname{id}_{\mathbf C} \downarrow \paren{\operatorname{id}_{\mathbf C}}}$ we have:
{{begin-eqn}}
{{eqn | l = \paren{I \circ J} \tuple{E, D, g}
      | r = \map I {J \tuple{E, D, g} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = I g
      | c = Definition of $J$
}}
{{eqn | r = \tuple{\operatorname{dom} g, \operatorname{cod} g, g}
      | c = Definition of $I$
}}
{{eqn | r = \tuple{E, D, g}
      | c = By $\text{(1)}$ and $\text{(2)}$
}}
{{eqn | r = \operatorname{id}_{\paren{\operatorname{id}_{\mathbf C} \downarrow \operatorname{id}_{\mathbf C} } } \tuple{E, D, g}
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
For each morphism $\tuple{k, h}: \tuple{E, D, g} \to \tuple{E', D', g'}$ in $\paren{\operatorname{id}_{\mathbf C} \downarrow \paren{\operatorname{id}_{\mathbf C}}}$ we have:
{{begin-eqn}}
{{eqn | l = \paren{I \circ J} \tuple{k, h}
      | r = \map I {J \tuple{k, h} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = I \tuple{k, h}
      | c = Definition of $J$
}}
{{eqn | r = \tuple{k, h}
      | c = Definition of $J$
}}
{{eqn | r = \operatorname{id}_{\paren{\operatorname{id}_{\mathbf C} \downarrow \operatorname{id}_{\mathbf C} } } \tuple{k, h}
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
It follows that:
:$I \circ J = \operatorname{id}_{\paren{\operatorname{id}_{\mathbf C} \downarrow \operatorname{id}_{\mathbf C} } }$
{{qed}}
Category:Morphism Category is Isomorphic to Comma Category
0hpzrbk68sofbbd74gf062x8og41xoh
Theorem: One-Sided Prepolar is One-Sided Polar in Transpose

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_\odot$ be the one-sided prepolar of $B$ taken in $\innerprod E F_{E \times F}$.
Let $B^{\odot^T}$ be the one-sided polar of $B$ taken in $\innerprod F E_{F \times E}$.
Then we have:
:$B_\odot = B^{\odot^T}$

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = B_\odot
		| r = \set {x \in E :\innerprod x f_{E \times F} \le 1 \text { for all } f \in B}
}}
{{eqn	| r = \set {x \in E : \innerprod f x_{F \times E} \le 1 \text { for all } f \in B}
}}
{{eqn	| r = B^{\odot^T}
}}
{{end-eqn}}
{{qed}}
Category:One-Sided Prepolars
Category:One-Sided Polars
3lduvpj3i9e93u3dr9yzlxlwo5webcc
Theorem: One-Sided Polar is One-Sided Prepolar in Transpose

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 $A \subseteq E$ be a non-empty set.
Let $A^\odot$ be the one-sided polar of $A$ taken in $\innerprod E F_{E \times F}$.
Let $A_{\odot^T}$ be the one-sided prepolar of $A$ taken in $\innerprod F E_{F \times E}$. 
Then we have:
:$A^\odot = A_{\odot^T}$

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = A^\odot
		| r = \set {f \in F :\innerprod x f_{E \times F} \le 1 \text { for all } x \in A}
}}
{{eqn	| r = \set {f \in F : \innerprod f x_{F \times E} \le 1 \text { for all } x \in A}
}}
{{eqn	| r = A_{\odot^T}
}}
{{end-eqn}}
{{qed}}
Category:One-Sided Polars
Category:One-Sided Prepolars
n7rliqzbz2fhooo391m9xmobu5bvi1k
Theorem: One-Sided Polar of Symmetric Set is equal to Absolute Polar

Let $\innerprod E F$ be a dual system over $\R$. 
Let $A \subseteq E$ be a symmetric set.
Let $A^\odot$ be the one-sided polar of $A$.
Let $A^\circ$ be the absolute polar of $A$.
Then $A^\odot = A^\circ$.

Proof:
Let $f \in A^\circ$.
Then for each $x \in A$, we have:
:$\cmod {\innerprod x f} \le 1$
and in particular:
:$\innerprod x f \le 1$
Hence $f \in A^\odot$.
Hence we have:
:$A^\circ \subseteq A^\odot$
We now just need to show that:
:$A^\odot \subseteq A^\circ$
Let $f \in A^\odot$.
Let $x \in A$.
Then:
:$\innerprod x f \le 1$
Further, we have $-x \in A$ since $A$ is symmetric.
Hence we also have:
:$\innerprod {-x} f \le 1$
Since $\innerprod \cdot \cdot$ is bilinear, we have:
:$-\innerprod x f \le 1$
and hence:
:$\innerprod x f \ge -1$ 
Hence we conclude that:
:$-1 \le \innerprod x f \le 1$
giving:
:$\cmod {\innerprod x f} \le 1$ 
Hence $f \in A^\circ$. 
Hence $f \in A^\odot$ implies that $f \in A^\circ$.
Hence $A^\odot \subseteq A^\circ$.
We conclude that $A^\odot = A^\circ$.
{{qed}}
Category:One-Sided Polars
Category:Absolute Polars
5ti0lwpjfhn8wsnj721c63n9dyh2uy4
Theorem: Normed Vector Space with Normed Dual Space is Dual System

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space.
Let $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ be the normed dual space of $\struct {X, \norm {\, \cdot \,}_X}$.
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 $\tuple {X, X^\ast, \innerprod \cdot \cdot}$ is a dual system.

Proof:
Let $X^\#$ be the algebraic dual of $X$.
From Normed Dual Space is Banach Space, $X^\ast$ is a vector subspace of $X^\#$.
From Normed Dual Space Separates Points, $X^\ast$ separates points.
Hence from Vector Space with Subspace of Algebraic Dual Separating Points is Dual System, $\tuple {X, X^\ast, \innerprod \cdot \cdot}$ is a dual system.
{{qed}}
Category:Normed Vector Spaces
Category:Dual Systems
fvuj8xhserql2n7oakjeg2ky4ocwycl
Theorem: Sphere is not Developable Surface

The sphere is ''not'' a developable surface.

Proof:
{{ProofWanted|Little formal work on curvature has been established on {{ProofWiki}}, so this is being left open while some of that work has been accomplished. Should be a result Gaussian Curvature of Sphere equals Curvature of Great Circle or some such}}
Theorem: One-Sided Polar is Closed in Weak-* Topology

Let $\innerprod E F$ be a dual system over $\R$.
Let $\map \sigma {F, E}$ be the weak-$\ast$ topology on $F$ induced by $\innerprod E F$.
Let $A \subseteq E$ be a non-empty set.
Let $A^\odot$ be the one-sided polar.
Then $A^\odot$ is $\map \sigma {F, E}$-closed.

Proof:
We use Characterization of Closedness in terms of Nets.
We show that every convergent net valued in $A^\odot$ has its limit in $A^\odot$.
Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\family {f_\lambda}_{\lambda \mathop \in \Lambda}$ be a convergent net valued in $A^\odot$ with limit $f \in F$. 
Then for each $x \in A$ and $\lambda \in \Lambda$ we have:
:$\innerprod x {f_\lambda} \le 1$
From Characterization of Convergence of Net in Weak-* Topology Induced by Dual System, we have:
:$\innerprod x {f_\lambda} \to \innerprod x f$
Hence:
:$\innerprod x f \le 1$ for each $x \in A$.
Hence $f \in A^\odot$.
Hence by Characterization of Closedness in terms of Nets, $A^\odot$ is $\map \sigma {F, E}$-closed.
{{qed}}
Category:One-Sided Polars
Category:Weak Topologies Induced by Dual Systems
dw6wqohab40o4ofltic2lszb81iiv3g
Theorem: Closed Unit Ball in Normed Vector Space is Balanced

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

Proof:
Let $x \in B_X^-$.
Let $\lambda \in \GF$ be such that $\cmod \lambda \le 1$. 
We have:
{{begin-eqn}}
{{eqn	| l = \norm {\lambda x}_X
		| r = \cmod \lambda \norm x_X
		| c = {{NormAxiomVector|2}}
}}
{{eqn	| o = \le
		| r = \norm x_X 
}}
{{eqn	| o = \le
		| r = 1
}}
{{end-eqn}}
{{qed}}
Category:Balanced Sets
Category:Normed Vector Spaces
2ilxs2d2ix8zcd42xunhzu0dy0gp91z
Theorem: Absolute Polar of Closed Unit Ball in Normed Vector Space

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 $B_X^-$ be the closed unit ball of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $B_{X^\ast}^-$ be the closed unit ball of $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$. 
Let $\paren {B_X^-}^\circ$ be the absolute polar of $B_X^-$ taken in the dual system $\innerprod X {X^\ast}$. 
Then:
:$\paren {B_X^-}^\circ = B_{X^\ast}^-$

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = \paren {B_X^-}^\circ
		| r = \set {f \in X^\ast : \cmod {\map f x} \le 1 \text { for each } x \in B_X^-}
}}
{{eqn	| r = \set {f \in X^\ast : \norm f_{X^\ast} \le 1}
		| c = {{Defof|Norm on Bounded Linear Functional}}
}}
{{eqn	| r = B_{X^\ast}^-
}}
{{end-eqn}}
{{qed}}
Category:Absolute Polars
Category:Normed Vector Spaces
jxyjt1qhx5r48bcjhd9i1iwztb3609s
Theorem: One-Sided Polar of Closed Unit Ball in Normed Vector Space

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 space of \struct {X, \norm {\, \cdot \,}_X}$.
Let $B_X^-$ be the closed unit ball of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $B_{X^\ast}^-$ be the closed unit ball of $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$. 
Let $\paren {B_X^-}^\odot$ be the one-sided polar of $B_X^-$ taken in the dual system $\innerprod X {X^\ast}$. 
Then:
:$\paren {B_X^-}^\odot = B_{X^\ast}^-$

Proof:
Let $\paren {B_X^-}^\circ$ be the absolute polar of $B_X^-$.
From Closed Unit Ball in Normed Vector Space is Balanced, we have that $B_X^-$ is balanced.
Hence from One-Sided Polar of Symmetric Set is equal to Absolute Polar and Balanced Set in Vector Space is Symmetric, we have:
:$\paren {B_X^-}^\odot = \paren {B_X^-}^\circ$
From Absolute Polar of Closed Unit Ball in Normed Vector Space, we have:
:$\paren {B_X^-}^\odot = B_{X^\ast}^-$
{{qed}}
Category:One-Sided Polars
Category:Normed Vector Spaces
1wwb8ks9g7gx8jmnpi8sit8qo8pn04w
Theorem: Absolute Prepolar of Closed Unit Ball in Normed Dual Space

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 $B_X^-$ be the closed unit ball of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $B_{X^\ast}^-$ be the closed unit ball of $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$. 
Let $\paren {B_{X^\ast}^-}_\circ$ be the absolute prepolar of $B_{X^\ast}^-$ taken in the dual system $\innerprod X {X^\ast}$.
Then:
:$\paren {B_{X^\ast}^-}_\circ = B_X^-$

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = \paren {B_{X^\ast}^-}_\circ
		| r = \set {x \in X : \cmod {\map f x} \le 1 \text { for all } f \in B_{X^\ast}^-}
}}
{{eqn	| r = \set {x \in X : \sup_{f \mathop \in B_{X^\ast}^-} \cmod {\map f x} \le 1}
}}
{{eqn	| r = \set {x \in X : \norm x_X \le 1}
		| c = Norm in terms of Normed Dual Space
}}
{{eqn	| r = B_X^- 
}}
{{end-eqn}}
{{qed}}
Category:Absolute Prepolars
Category:Normed Dual Spaces
ndw5cf4kvdnb40bfsspw6esrhxkr4o2
Theorem: Real Matrix is Diagonalizable if Roots of Characteristic Equation are Real and Distinct

Let $\mathbf A$ be a square matrix of order $n$ whose entries are real.
Let the $n$ roots of the characteristic equation of $\mathbf A$ be real and distinct.
Then $\mathbf A$ is diagonalizable in $\mathbb R^n$.

Proof:
From Number of Roots of Polynomial With Complex Coefficients Equals Degree of Polynomial, $n$ distinct roots of a degree $n$ characteristic polynomial must have algebraic multipicity of $1$.
Since Algebraic Multiplicity is not Less than Geometric Multiplicity, the geometric multiplicity of each eigenvalue is $1$.
Thus, $\mathbf A$ has $n$ eigenvectors.
From Eigenvectors Corresponding to Distinct Eigenvalues of Linear Operator are Linearly Independent, these eigenvectors are a linearly independent set.
We have
:$\mathbf A \mathbf v_i = \lambda_i \mathbf v_i$
where
:$\mathbf v_i$ is an eigenvector of $\mathbf A$
:$\lambda_i$ is an eigenvalue associated with $\mathbf v_i$
Since $\mathbf A$ and $\lambda_i$ are real, $\mathbf v_i$ can always be chosen from $\mathbb R^n$.
Thus, the eigenvectors of $\mathbf A$ form a basis for $\mathbb R^n$.
Therefore, by the definition, $\mathbf A$ is diagonalizable in $\mathbb R^n$.
{{qed}}
Theorem: Powers of Diagonalizable Matrix

Let $\mathbf A$ be a square matrix which is diagonalizable matrix.
Let $\mathbf D$ be the diagonal matrix which is the result of the equation:
:$\mathbf D = \mathbf X^{-1} \mathbf A \mathbf X$
for some nonsingular matrix $\mathbf X$.
Then for all $n \in \Z_{\ge 0}$:
:$\mathbf A^n = \mathbf X \mathbf D^n \mathbf X^{-1}$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\mathbf A^n = \mathbf X \mathbf D^n \mathbf X^{-1}$
Let $\mathbf A$ be of dimension $m$ where $m \in \Z_{\ge 1}$.
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = \mathbf A^0
      | r = \mathbf I_m
      | c = where $\mathbf I_m$ is the identity matrix of dimension $m$
}}
{{eqn | r = \mathbf X \mathbf X^{-1}
      | c = {{Defof|Inverse Matrix}}
}}
{{eqn | r = \mathbf X \mathbf D^0 \mathbf X^{-1}
      | c = as $\mathbf D^0 = \mathbf I_m$
}}
{{end-eqn}}
Thus $\map P 0$ is seen to hold.
Theorem: Existence of Continuous Linear Functional separating Point in Hausdorff Locally Convex Space from Convex Set with Non-Empty Interior

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \PP}$ be a Hausdorff locally convex space over $\GF$.
Let $X^\ast$ be the topological dual space of $\struct {X, \PP}$.
Let $C \subseteq X$ be a convex set with non-empty interior. 
Let $\Int C$ be the interior of $C$.
Let $x_0 \in X \setminus C$. 
Then there exists $f \in X^\ast$ such that:
:$\map \Re {\map f x} \le \map \Re {\map f {x_0} }$ for each $x \in C$
and:
:$\map \Re {\map f x} < \map \Re {\map f {x_0} }$ for each $x \in \Int C$.

Proof:
Since $x \in X \setminus C$, we also have $x \in X \setminus \Int C$. 
From Interior of Convex Set in Topological Vector Space is Convex, $\Int C$ is convex.
From Hahn-Banach Separation Theorem: Hausdorff Locally Convex Space: Complex Case: Open Convex Set and Convex Set applied to $\set {x_0}$ and $\Int C$, there exists $f \in X^\ast$ such that:
:$\map \Re {\map f x} < \map \Re {\map f {x_0} }$ for each $x \in \Int C$.
It remains to show that:
:$\map \Re {\map f x} \le \map \Re {\map f {x_0} } $ for each $x \in C$. 
Let $t \in \openint 0 1$.
From Dilation of Open Set in Topological Vector Space is Open, $t \Int C$ is open.
From Sum of Set and Open Set in Topological Vector Space is Open, $\paren {1 - t} C + t \Int C$ is open. 
Further, since $C$ is convex, we have $\paren {1 - t} C + t \Int C \subseteq \paren {1 - t} C + t C \subseteq C$. 
Hence we have:
:$\paren {1 - t} C + t \Int C \subseteq \Int C$ 
Let $y \in \Int C$.
We then have:
:$\paren {1 - t} x + t y \in \Int C$ for each $t \in \openint 0 1$ and $x \in C$. 
Hence we have:
:$\map \Re {\map f {\paren {1 - t} x + t y} } < \map \Re {\map f {x_0} }$ for each $x \in C$ and $t \in \openint 0 1$.
Hence:
:$\paren {1 - t} \map \Re {\map f x} + t \map \Re {\map f y} < \map \Re {\map f {x_0} }$ for each $x \in C$ and $t \in \openint 0 1$. 
Taking $t \to 0^+$, we have:
:$\map \Re {\map f x} \le \map \Re {\map f {x_0} }$ for each $x \in C$.
Hence $f$ is our desired continuous linear functional.
{{qed}}