avewright/proofwiki-math huggingface dataset:
Theorem: Hermitian Element of Unital C*-Algebra is Linear Combination of Two Unitary Elements

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra.
Let $x \in A$ be Hermitian. 
Then there exists unitary elements $u, v \in A$ and $\alpha \ge 0$ such that:
:$x = \alpha \paren {u + v}$

Proof:
If $x = {\mathbf 0}_A$, then we can take $\alpha = 0$ and $u = v = {\mathbf 1}_A$.
Take $x \ne {\mathbf 0}_A$.
First take $\norm x \le 1$. 
From Spectral Radius of Normal Element of C*-Algebra Equal to Norm, we have:
:$\norm x = \sup \set {\cmod \lambda : \lambda \in \map {\sigma_A} x} \le 1$
where $\map {\sigma_A} x$ denotes the spectrum of $x$ in $A$.
From Spectrum of Hermitian Element in Unital C*-Algebra is Real we have $\map {\sigma_A} x \subseteq \R$.
We therefore have:
:$\map {\sigma_A} x \subseteq \closedint {-1} 1$
Hence $1 - t^2 \ge 0$ for each $t \in \map {\sigma_A} x$. 
Hence by the Spectral Mapping Theorem for Polynomials, we obtain:
:$\map {\sigma_A} { {\mathbf 1}_A - x^2} = \set {1 - t^2 : t \in \map {\sigma_A} x} \subseteq \hointr 0 \infty$
From Star of Product of Elements in *-Algebra and Identity Element in Unital *-Algebra is Hermitian, we have that ${\mathbf 1}_A - x^2$ is Hermitian.
So ${\mathbf 1}_A - x^2$ is positive. 
From Existence and Uniqueness of Positive Nth Root of Positive Element of C*-Algebra, there exists a positive $s \in A$ with $s^2 = {\mathbf 1}_A - x^2$.
Take $u = x + i s$ and $v = x - i s$.
We have:
{{begin-eqn}}
{{eqn	| l = u u^\ast
		| r = \paren {x + i s} \paren {x - i s}
}}
{{eqn	| r = x^2 + s^2 
}}
{{eqn	| r = x^2 + \paren { {\mathbf 1}_A - x^2}
}}
{{eqn	| r = {\mathbf 1}_A
}}
{{end-eqn}}
We also have:
:$u^\ast u = \paren {x - is} \paren {x + i s} = x^2 + s^2 = {\mathbf 1}_A$
Hence $u$ is unitary.
Since $v = u^\ast$, we obtain that $v$ is unitary also. 
We clearly have:
{{begin-eqn}}
{{eqn	| l = \frac 1 2 \paren {u + v}
		| r = \frac 1 2 \paren {x + is + \paren {x - is} }
}}
{{eqn	| r = \frac 1 2 \paren {2 x}
}}
{{eqn	| r = x
}}
{{end-eqn}}
Hence we have the result for $\norm x \le 1$.
Now take $\norm x > 1$.
We have that:
:$\ds \norm {\frac x {\norm x} } \le 1$
from {{NormAxiomVector|2}}.
Hence there exists unitary elements $u, v \in A$ such that:
:$\ds \frac x {\norm x} = \frac 1 2 \paren {u + v}$
so that:
:$\ds x = \frac {\norm x} 2 \paren {u + v}$
Hence we are done with $\alpha = \dfrac {\norm x} 2$. 
{{qed}}
Theorem: Equivalence of Definitions of Frame Isomorphism

Let $L_1 = \struct {S_1, \preceq_1}$ and $L_2 = \struct {S_2, \preceq_2}$ be frames.
{{TFAE|def=Frame Isomorphism}}
=== Definition 1 ===
{{:Definition:Frame Isomorphism/Definition 1}}
=== Definition 2 ===
{{:Definition:Frame Isomorphism/Definition 2}}
=== Definition 3 ===
{{:Definition:Frame Isomorphism/Definition 3}}
=== Definition 4 ===
{{:Definition:Frame Isomorphism/Definition 4}}

Proof:
By definition of frame:
:$L_1$ and $L_2$ are complete lattices
From Equivalence of Definitions of Complete Lattice Isomorphism definitions $2$, $3$ and $4$ are equivalent.
Theorem: Frame Isomorphism is Isomorphism in Category Frm

Let $\mathbf{Frm}$ denote the category of frames.
Let $\phi : L_1 \to L_2$ be a morphism of $\mathbf{Frm}$.
Then:
:$\phi$ is an isomorphism of $\mathbf{Frm}$ {{iff}} $\phi$ is a complete lattice isomorphsm

Proof:
Let $L_1$ and $L_2$ be the frames $L_1 = \struct{S_1, \preceq_1}$ and $L_2 = \struct{S_2, \preceq_2}$ respectively.
By definition of category of frames:
:$\phi$ is a frame homomorphisms
By definition of an isomorphism:
:$\phi$ is an isomorphism of $\mathbf{Frm}$
{{iff}}:
:$(1):$ there exists a morphism of $\psi : L_2 \to L_1$ of $\mathbf{Frm}$ such that:
::$\psi \circ \phi = \operatorname{id}_{L_1}$ and $\phi \circ \psi= \operatorname{id}_{L_2}$
:where $\operatorname{id}_{L_1}$ and $\operatorname{id}_{L_2}$ are identity morphisms.
By definition of category of frames:
:$\phi$ satisfies $(1)$
{{iff}}:
:$(2):$ there exists a frame homomorphism $\psi : L_2 \to L_1$ such that:
::the standard compositions of mappings $\psi \circ \phi = \operatorname{id}_{S_1}$ and $\phi \circ \psi = \operatorname{id}_{S_2}$
:where $\operatorname{id}_{S_1}$ and $\operatorname{id}_{S_2}$ are identity mappings.
Theorem: Monomorphism iff Epimorphism in Dual Category

Let $\mathbf C$ be a metacategory.
Let $\mathbf C^{\operatorname{op}}$ be the dual category of $\mathbf C$.
Let $f$ be a morphism of $\mathbf C$.
Then $f$ is a monomorphism in $\mathbf C$ {{iff}} $f^{\operatorname{op}}$ is an epimorphism in $\mathbf C^{\operatorname{op}}$.

Proof:
=== Necessary Condition ===
Let $f$ be a monomorphism in $\mathbf C$.
Let $g^{\operatorname{op}}$ and $h^{\operatorname{op}}$ be morphisms of $\mathbf C^{\operatorname{op}}$:
:the compositions $g^{\operatorname{op}} \circ f^{\operatorname{op}}$ and $h^{\operatorname{op}} \circ f^{\operatorname{op}}$ are defined
We have:
{{begin-eqn}}
{{eqn | l = g^{\operatorname{op} } \circ f^{\operatorname{op} }
      | r = h^{\operatorname{op} } \circ f^{\operatorname{op} }
}}
{{eqn | ll = \leadsto
      | l = \paren{f \circ g}^{\operatorname{op} }
      | r = \paren{f \circ h}^{\operatorname{op} }
      | c = {{Defof|Composition of Morphisms}} in Dual Category
}}
{{eqn | ll = \leadsto
      | l = f \circ g
      | r = f \circ h
      | c = {{Defof|Dual Category}}
}}
{{eqn | ll = \leadsto
      | l = g
      | r = h
      | c = {{Defof|Monomorphism}}
}}
{{eqn | ll = \leadsto
      | l = g^{\operatorname{op} }
      | r = h^{\operatorname{op} }
      | c = {{Defof|Dual Category}}
}}
{{end-eqn}}
It follows that $ f^{\operatorname{op}}$ is an epimorphism in $\mathbf C^{\operatorname{op}}$.
{{qed|lemma}}
Theorem: Epimorphism iff Monomorphism in Dual Category

Let $\mathbf C$ be a metacategory.
Let $\mathbf C^{\operatorname{op}}$ be the dual category of $\mathbf C$.
Let $f$ be an morphism of $\mathbf C$.
Then $f$ is a epimorphism in $\mathbf C$ {{iff}} $f^{\operatorname{op}}$ is a monomorphism in $\mathbf C^{\operatorname{op}}$.

Proof:
=== Necessary Condition ===
Let $f$ be an epimorphism in $\mathbf C$.
Let $g^{\operatorname{op}}$ and $h^{\operatorname{op}}$ be morphisms of $\mathbf C^{\operatorname{op}}$:
:the compositions $f^{\operatorname{op}} \circ g^{\operatorname{op}}$ and $f^{\operatorname{op}} \circ h^{\operatorname{op}}$ are defined
We have:
{{begin-eqn}}
{{eqn | l = f^{\operatorname{op} } \circ g^{\operatorname{op} }
      | r = f^{\operatorname{op} } \circ h^{\operatorname{op} }
}}
{{eqn | ll = \leadsto
      | l = \paren{g \circ f}^{\operatorname{op} }
      | r = \paren{h \circ f}^{\operatorname{op} }
      | c = {{Defof|Composition of Morphisms}} in Dual Category
}}
{{eqn | ll = \leadsto
      | l = g \circ f
      | r = g \circ f
      | c = {{Defof|Dual Category}}
}}
{{eqn | ll = \leadsto
      | l = g
      | r = h
      | c = {{Defof|Epimorphism}}
}}
{{eqn | ll = \leadsto
      | l = g^{\operatorname{op} }
      | r = h^{\operatorname{op} }
      | c = {{Defof|Dual Category}}
}}
{{end-eqn}}
It follows that $ f^{\operatorname{op}}$ is an monomorphism in $\mathbf C^{\operatorname{op}}$.
{{qed|lemma}}
Theorem: Isomorphism iff Isomorphism in Dual Category

Let $\mathbf C$ be a metacategory.
Let $\mathbf C^{\operatorname{op}}$ be the dual category of $\mathbf C$.
Let $f$ be a morphism of $\mathbf C$.
Then $f$ is an isomorphism in $\mathbf C$ {{iff}} $f^{\operatorname{op}}$ is an isomorphism in $\mathbf C^{\operatorname{op}}$.

Proof:
=== Necessary Condition ===
Let $f: C_1 \to C_2$ be an isomorphism in $\mathbf C$.
Let $g: C_2 \to C_1$ be the inverse morphism of $f$ in $\mathbf C$.
By definition of inverse morphism:
:$g \circ f = \operatorname{id}_{C_1}$
:$f \circ g = \operatorname{id}_{C_2}$
where $\operatorname{id}_{C_1}, \operatorname{id}_{C_2}$ denote the identity morphisms on $C_1, C_2$ respectively.
We have:
{{begin-eqn}}
{{eqn | l = g^{\text{op} } \circ f^{\text{op} }
      | r = \paren{f \circ g}^{\text{op} }
      | c = {{Defof|Composition of Morphisms}} in Dual Category
}}
{{eqn | r = \operatorname{id}_{C_2}^{\text{op} }
      | c = {{Defof|Isomorphism (Category Theory)}}
}}
{{eqn | r = \operatorname{id}_{C_2^{\text{op} } }
      | c = {{Defof|Identity Morphism}} in Definition:Dual Category
}}
{{end-eqn}}
Similarly:
:$f^{\text{op} } \circ g^{\text{op} } = \operatorname{id}_{C_1^{\text{op} }}$
It follows that $f^{\text{op} }$ is an isomorphism in $\mathbf C^{\operatorname{op}}$ by definition.
{{qed|lemma}}
Theorem: Non-Negative Multiple of Positive Element of C*-Algebra is Positive

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $x \in A$ be positive. 
Let $\alpha \ge 0$.
Then $\alpha x$ is positive.

Proof:
Let $\sigma_A$ denote the spectrum in $A$.
Since $x$ is positive, we have:
:$\map {\sigma_A} x \subseteq \hointr 0 \infty$
From Spectral Mapping Theorem for Polynomials, we have:
:$\map {\sigma_A} {\alpha x} = \set {\alpha t : t \in \map {\sigma_A} x}$
Since $t \in \map {\sigma_A} x$ has $t \ge 0$, we have $\alpha t \ge 0$ for each $t \in \map {\sigma_A} x$.
Hence we hae:
:$\map {\sigma_A} {\alpha x} \subseteq \hointr 0 \infty$
Further from $(\text C^\ast 4)$ in the definition of an involution, we have:
:$\paren {\alpha x}^\ast = \overline \alpha x^\ast = \alpha x$ 
since $x$ is Hermitian and $\alpha$ is real.
Hence $\alpha x$ is Hermitian with $\map {\sigma_A} {\alpha x} \subseteq \hointr 0 \infty$.
Hence $\alpha x$ is positive.
{{qed}}
Category:Positive Elements of C*-Algebras
Category:Non-Negative Multiple of Positive Element of C*-Algebra is Positive
ttrh9cdrh9stgwn0btwmdo6es6dry62
Theorem: Characterization of Positive Element of Unital C*-Algebra

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra.
Let $a \in A$ be Hermitian. 
Let $t \ge 0$. 
Then if $\norm {a - t {\mathbf 1}_A} \le t$, $a$ is positive.
Conversely if $\norm a \le t$ and $a$ is positive, then $\norm {a - t {\mathbf 1}_A} \le t$.

Proof:
Let $B$ to be $\text C^\ast$-algebra generated by $\set { {\mathbf 1}_A, x}$. 
{{mistake|$x{{=}}a$}}
By C*-Algebra Generated by Commutative Self-Adjoint Set is Commutative, $B$ is commutative.
Further from Spectrum of Element of Unital C*-Subalgebra of Unital C*-Algebra we have $\map {\sigma_B} x = \map {\sigma_A} x$.
Let $\Phi_B$ be the spectrum of $B$.
From Gelfand-Naimark Theorem: Commutative Case: Unital, there exists an isometric unital $\ast$-algebra isomorphism $G : B \to \map \CC {\Phi_B}$.
Suppose that $\norm {a - t {\mathbf 1}_A} \le t$.
Since $G$ is isometric and unital, we have:
:$\norm {a - t {\mathbf 1}_A} = \norm {\map G a - t}_\infty \le t$
where $\norm {\, \cdot \,}_\infty$ is the supremum norm on $\map \CC {\Phi_B}$.
Write $f = \map G a$ for brevity.
Since $G$ is a $\ast$-algebra isomorphism, $f$ is Hermitian.
Hence $\overline {\map f \phi} = \map f \phi$ for each $\phi \in \Phi_B$.
From Complex Number equals Conjugate iff Wholly Real, we then have $\map f \phi \in \R$ for each $\phi \in \Phi_B$.
Hence $\norm {f - t}_\infty \le t$ implies that $\map f \phi \in \closedint 0 {2 t}$ for each $\phi \in \Phi_B$.
From Spectrum of Element of Space of Continuous Functions on Compact Hausdorff Space, we therefore have $\map {\sigma_{\map \CC {\Phi_B} } } f \subseteq \closedint 0 {2 t}$.
Then, from Spectrum of Image of Element of Unital Algebra under Unital Algebra Homomorphism, we have:
:$\map {\sigma_A} a = \map {\sigma_B} a = \map {\sigma_{\map \CC {\Phi_B} } } f \subseteq \closedint 0 {2 t} \subseteq \hointr 0 \infty$
Hence $a$ is positive.
Now suppose that $\norm a \le t$ and $a$ is positive.
Again write $f = \map G a$. 
From Spectrum of Image of Element of Unital Algebra under Unital Algebra Homomorphism we have:
:$\map {\sigma_{\map \CC {\Phi_B} } } f = \map {\sigma_B} a = \map {\sigma_A} a$ 
So $\map {\sigma_{\map \CC {\Phi_B} } } f \subseteq \hointr 0 \infty$.
From Spectrum of Element of Space of Continuous Functions on Compact Hausdorff Space we therefore have:
:$\set {\map f \phi : \phi \in \Phi_B} \subseteq \hointr 0 \infty$
Since $G$ is isometric, we have $\norm f_\infty \le t$. 
So $\map f \phi \in \closedint 0 t$ for each $\phi \in \Phi_B$. 
Hence $t - \map f \phi \in \closedint 0 t$ for each $\phi \in \Phi_B$.
We therefore have $\norm {t - \map G a}_\infty \le t$. 
Again since $G$ is an isometric unital $\ast$-algebra isomorphism, we have $\norm {a - t {\mathbf 1}_A} \le t$. 
{{qed}}
Theorem: Set of Positive Elements of C*-Algebra is Closed

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $A^+$ be the set of positive elements of $A$.
Then $A^+$ is closed.

Proof:
Let $\struct {A_+, \ast, \norm {\, \cdot \,}_\ast}$ be the unitization of $A$. 
Let ${\mathbf 1}_+$ be the identity element of $A_+$. 
Let $\iota : A \to A_+$ be the mapping defined by:
:$\map \iota a = \tuple {a, 0}$
for each $a \in A$. 
Let $\sequence {a_n}_{n \mathop \in \N}$ be a sequence in $A^+$ such that $a_n \to a$ in $\struct {A, \norm {\, \cdot \,} }$.
From Convergence in Direct Product Norm, $\sequence {\tuple {a_n, 0} }_{n \mathop \in \N}$ converges to $\struct {a, 0}$ in $\struct {A_+, \norm {\, \cdot \,}_\ast}$. 
From Convergent Sequence in Normed Vector Space is Bounded, there exists $t \ge 0$ such that:
:$\norm {\tuple {a_n, 0} } \le t$
From Element of C*-Algebra is Positive iff Positive in Unitization, $\tuple {a_n, 0}$ is positive for each $n \in \N$.
Hence from Characterization of Positive Element of Unital C*-Algebra, we must have:
:$\norm {\tuple {a_n, 0} - t {\mathbf 1}_+} \le t$ 
Taking $n \to \infty$ we obtain:
:$\norm {\tuple {a, 0} - t {\mathbf 1}_+} \le t$ 
from Norm is Continuous.
Hence by Characterization of Positive Element of Unital C*-Algebra, $\tuple {a, 0}$ is positive in $A_+$.
Hence by Element of C*-Algebra is Positive iff Positive in Unitization, $a \in A^+$. 
Hence by the definition of a closed set in a normed vector space, $A^+$ is closed.
{{qed}}
Theorem: Sum of Two Positive Elements of C*-Algebra is Positive

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $a, b$ be positive.
Then $a + b$ is positive.

Proof:
From $(\text C^\ast 2)$ in the definition of an involution, $a + b$ is Hermitian.
First suppose that $A$ is unital.
From Characterization of Positive Element of Unital C*-Algebra we have:
:$\norm {a - \norm a {\mathbf 1}_A} \le \norm a$
and:
:$\norm {b - \norm b {\mathbf 1}_A} \le \norm b$ 
Hence we have:
{{begin-eqn}}
{{eqn	| l = \norm {\paren {a + b} - \paren {\norm a + \norm b} {\mathbf 1}_A}
		| r = \norm {\paren {a - \norm a {\mathbf 1}_A} + \paren {b - \norm b {\mathbf 1}_A} }
}}
{{eqn	| o = \le
		| r = \norm {a - \norm a {\mathbf 1}_A} + \norm {b - \norm b {\mathbf 1}_A}
		| c = {{NormAxiomVector|3}}
}}
{{eqn	| r = \norm a + \norm b 
}}
{{end-eqn}}
From {{NormAxiomVector|3}}, we have:
:$\norm {a + b} \le \norm a + \norm b$
Hence by Characterization of Positive Element of Unital C*-Algebra, we have that $a + b$ is positive.
Now suppose that $A$ is not unital.
Let $A_+$ be the unitization of $A$. 
Define:
:$\tuple {u, \lambda}^\ast = \tuple {u^\ast, \overline \lambda}$
for each $\tuple {u, \lambda} \in A_+$.
From Existence of Unitization of C*-Algebra, there exists a unique algebra norm $\norm {\, \cdot \,}_\ast$ such that $\struct {A_+, \ast, \norm {\, \cdot \,}_\ast}$ is a unital $\text C^\ast$-algebra.
With this definition $\tuple {a, 0}$, $\tuple {b, 0}$ and $\tuple {a + b, 0}$ are all Hermitian in $A_+$. 
Further:
:$\map {\sigma_{A_+} } {\tuple {a, 0} } = \map {\sigma_A} a \subseteq \hointr 0 \infty$
:$\map {\sigma_{A_+} } {\tuple {b, 0} } = \map {\sigma_A} b \subseteq \hointr 0 \infty$
:$\map {\sigma_{A_+} } {\tuple {a + b, 0} } = \map {\sigma_A} {a + b}$
From the unital case, we have that $\tuple {a + b, 0}$ is positive in $A_+$. 
Hence $\map {\sigma_{A_+} } {\tuple {a + b, 0} } \subseteq \hointr 0 \infty$.
Hence $\map {\sigma_A} {a + b} \subseteq \hointr 0 \infty$. 
Hence $a + b$ is positive.
{{qed}}
Theorem: Spectral Radius of Normal Element of C*-Algebra Equal to Norm/Corollary

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra. 
Let $r_A$ be the spectral radius in $A$.
Let $x \in A$ be normal such that:
:$\map {r_A} x = 0$
Then $x = {\mathbf 0}_A$.

Proof:
From Spectral Radius of Normal Element of C*-Algebra Equal to Norm, we have:
:$\norm x = \map {r_A} x = 0$
Hence from {{NormAxiomVector|1}}, we have $x = {\mathbf 0}_A$.
{{qed}}
Category:Spectral Radius of Normal Element of C*-Algebra Equal to Norm
fp8t9u64etd6n80gvtopi9ny7qlzhbf
Theorem: Set of Positive Elements of C*-Algebra is Convex Cone

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra. 
Let $A^+$ be the set of positive elements of $A$.
Then $A^+$ is a convex cone.

Proof:
From Non-Negative Multiple of Positive Element of C*-Algebra is Positive, if $x \in A^+$ and $\alpha \in \R_{\ge 0}$, we have $\alpha x \in A^+$. 
Hence $A^+$ is a cone.
From Sum of Two Positive Elements of C*-Algebra is Positive, we have $x + y \in A^+$ for $x, y \in A^+$.
Hence $A^+$ is a convex cone.
{{qed}}
Category:Positive Elements of C*-Algebras
rhm3zspsoeewpg0uoo5ltpj52ssoyhz
Theorem: Positive Part of Continuous Function is Continuous

Let $X$ be a topological space.
Let $f : X \to \R$ be continuous.
Let $f^+$ be the positive part of $f$. 
Then $f^+$ is continuous.

Proof:
From Constant Function is Continuous, we have that $\mathbf 0 : X \to \R$ defined by $\map {\mathbf 0} x = 0$ for each $x \in X$ is continuous.
From Maximum Rule for Continuous Real-Valued Functions, we have that the function $f \vee \mathbf 0 : X \to \R$ defined by:
:$\map {\paren {f \vee \mathbf 0} } x = \max \set {0, \map f x}$ for each $x \in X$
is continuous.
By the definition of the positive part, we have:
:$f^+ = f \vee \mathbf 0$
Hence the result.
{{qed}}
Theorem: Negative Part of Continuous Function is Continuous

Let $X$ be a topological space.
Let $f : X \to \R$ be continuous.
Let $f^-$ be the negative part of $f$. 
Then $f^-$ is continuous.

Proof:
From Constant Function is Continuous, we have that $\mathbf 0 : X \to \R$ defined by $\map {\mathbf 0} x = 0$ for each $x \in X$ is continuous.
From Minimum Rule for Continuous Real-Valued Functions, we have that the function $f \vee \mathbf 0 : X \to \R$ defined by:
:$\map {\paren {f \wedge \mathbf 0} } x = \min \set {0, \map f x}$ for each $x \in X$
is continuous.
From Multiple Rule for Continuous Real-Valued Function, $-\paren {f \wedge \mathbf 0}$ is continuous.
From the definition of the negative part, we have $f^- = -\paren {f \wedge \mathbf 0}$.
Hence $f^-$ is continuous.
{{qed}}
Theorem: Complex-Valued Function Dominated by Function Vanishing at Infinity also Vanishes at Infinity

Let $X$ be a topological space. 
Let $g : X \to \C$ be a complex-valued function vanishing at infinity.
Let $f : X \to \C$ be such that $\cmod f \le \cmod g$.
Then $f$ vanishes at infinity.

Proof:
Let $\epsilon > 0$.
Since $g$ vanishes at infinity, there exists a compact set $F \subseteq X$ such that:
:$\cmod {\map g x} < \epsilon$ for $x \in X \setminus F$. 
We then have:
:$\cmod {\map f x} \le \cmod {\map g x} < \epsilon$ for $x \in X \setminus F$.
Since $\epsilon$ was arbitrary, we have that $f$ vanishes at infinity.
{{qed}}
Category:Complex-Valued Functions Vanishing at Infinity
6f9m14ym66zogpco24a7aiyijmz5cid
Theorem: Positive Part of Real-Valued Function Vanishing at Infinity Vanishes at Infinity

Let $X$ be a topological space. 
Let $f : X \to \R$ be a real-valued function vanishing at infinity.
Let $f^+$ be the positive part of $f$. 
Then $f^+$ vanishes at infinity.

Proof:
From Positive Part of Function Bounded above by Absolute Value, we have:
:$0 \le f^+ \le \cmod f$
From Complex-Valued Function Dominated by Function Vanishing at Infinity also Vanishes at Infinity:
:$f^+$ vanishes at infinity.
{{qed}}
Category:Positive Parts
Category:Complex-Valued Functions Vanishing at Infinity
gbm9bm05erzw1z5ruw6osp4wbx58be9
Theorem: Positive Part of Function Bounded above by Absolute Value

Let $X$ be a set.
Let $f : X \to \C$ be a function.
Let $f^+$ be the positive part of $f$.
Then $f^+ \le \cmod f$.

Proof:
By definition, we have $f^+ \ge 0$. 
Let $f^-$ be the negative part of $f$. 
By definition, we also have $f^- \ge 0$.
Hence $f^+ \le f^+ + f^-$.
By Sum of Positive and Negative Parts, we have $f^+ + f^- = \cmod f$. 
Hence $0 \le f^+ \le \cmod f$.
{{qed}}
Category:Positive Parts
e47s1edq6a1qzltnrxefsn2bsag0nc1
Theorem: Negative Part of Function Bounded above by Absolute Value

Let $X$ be a set.
Let $f : X \to \C$ be a function.
Let $f^-$ be the negative part of $f$.
Then $f^- \le \cmod f$.

Proof:
By definition, we have $f^- \ge 0$. 
Let $f^+$ be the positive part of $f$. 
By definition, we also have $f^+ \ge 0$.
Hence $f^- \le f^+ + f^-$.
By Sum of Positive and Negative Parts, we have $f^+ + f^- = \cmod f$. 
Hence $0 \le f^- \le \cmod f$.
{{qed}}
Category:Negative Parts
fjk0mt1cipzitewb2qrscsiz8th52v5
Theorem: Negative Part of Real-Valued Function Vanishing at Infinity Vanishes at Infinity

Let $X$ be a topological space. 
Let $f : X \to \R$ be a real-valued function vanishing at infinity.
Let $f^-$ be the negative part of $f$. 
Then $f^-$ vanishes at infinity.

Proof:
From Negative Part of Function Bounded above by Absolute Value, we have:
:$0 \le f^- \le \cmod f$
From Complex-Valued Function Dominated by Function Vanishing at Infinity also Vanishes at Infinity:
:$f^-$ vanishes at infinity.
{{qed}}
Category:Negative Parts
Category:Complex-Valued Functions Vanishing at Infinity
8o73qhtf59g9tkl6ohjxqj4wgt8wdj7
Theorem: Product of Positive and Negative Parts is Zero

Let $X$ be a set.
Let $f : X \to \R$ be a real-valued function.
Let $f^+$ and $f^-$ be the positive part and negative part of $f$ respectively.
Then $f^+ f^- = 0$.

Proof:
Let $x \in X$.
If $\map f x = 0$, then we have $\map {f^+} x = \map {f^-} x = 0$. 
Hence $\map {f^+} x = \map {f^-} x = 0$ in this case.
If $\map f x > 0$, then $\map {f^+} x = \map f x$ and $\map {f^-} x = 0$.
So $\map {f^+} x \map {f^-} x = 0$ in this case also.
Finally, if $\map f x < 0$, then $\map {f^+} x = 0$ and $\map {f^-} x = -\map f x$.
So $\map {f^+} x \map {f^-} x = 0$ in this case.
We have covered all possibilities, so we have $\map {f^+} x \map {f^-} x = 0$ for each $x \in X$.
{{qed}}
Category:Positive Parts
Category:Negative Parts
ffcguwq1g1fae287j5kh1y6hl242elc
Theorem: Set of Positive Elements of C*-Algebra is Set of Products of Element with its Star

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $a \in A$. 
Let $A^+$ be the set of positive elements of $A$.
We have:
:$A^+ = \set {a^\ast a : a \in A}$

Proof:
From Product of Element of C*-Algebra with its Star is Positive, we have:
:$\set {a^\ast a : a \in A} \subseteq A^+$
Conversely suppose that $x \in A^+$.
From Existence and Uniqueness of Positive Nth Root of Positive Element of C*-Algebra, there exists $y \in A^+$ such that $x = y^2$.
Since $y$ is Hermitian, we have $x = y^\ast y$.
So $x \in \set {a^\ast a : a \in A}$.
Hence:
:$A^+ = \set {a^\ast a : a \in A}$
{{qed}}
Theorem: Conjugation in C*-Algebra preserves Positivity

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $a \in A$ be positive.
Let $c \in A$.
Then $c^\ast a c$ is positive.

Proof:
Since $a$ is positive, there exists a positive $b \in A$ such that $a = b^2$ from Existence and Uniqueness of Positive Nth Root of Positive Element of C*-Algebra.
We then have:
:$\paren {b c}^\ast \paren {b c} = c^\ast b^2 c = c^\ast a c$
From Product of Element of C*-Algebra with its Star is Positive, we have that $\paren {b c}^\ast \paren {b c}$ is positive.
Hence $c^\ast a c$ is positive.
{{qed}}
Theorem: Conjugation in C*-Algebra preserves Positivity/Corollary

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $\le$ be the canonical preordering on $A$.
Let $a, b \in A$ be such that $a \le b$. 
Let $c \in A$.
Then $c^\ast a c \le c^\ast b c$.

Proof:
Since $a \le b$, we have that $b - a$ is positive.
Hence $c^\ast \paren {b - a} c$ is positive by Conjugation in C*-Algebra preserves Positivity.
Hence $c^\ast b c - c^\ast a c$ is positive.
By the definition of $\le$, we have $c^\ast a c \le c^\ast b c$. 
{{qed}}