avewright/proofwiki-math huggingface dataset:
Theorem: Inverse Image Mapping is Lower Adjoint to Composite Involving Direct Image Mapping

Let $S, T$ be sets.
Let $f: S \to T$ be a mapping.
Let $f^\to : \powerset S \to \powerset T$ denote the direct image mapping.
Let $f^\gets : \powerset T \to \powerset S$ denote the inverse image mapping.
Let $\complement_S: \powerset S \to \powerset S$ denote the relative complement mapping on the power set of $S$.
Let $\complement_T: \powerset T \to \powerset T$ denote the relative complement mapping on the power set of $T$.
Then:
:$f^\gets : \powerset T \to \powerset S$ is the lower adjoint to $\complement_T \circ f^\to \circ \complement_S : \powerset S \to \powerset T$
That is:
:$\forall A \subseteq S, B \subseteq T : \map {f^\gets} B \subseteq A$ {{iff}} $B \subseteq T \setminus \map {f^\to} {S \setminus A}$

Proof:
We have:
{{begin-eqn}}
{{eqn | q = \forall A \subseteq S, B \subseteq T
      | l = \map {f^\gets} B
      | o = \subseteq
      | r = A
}}
{{eqn | ll = \leadstoandfrom
      | l = f^{-1} \sqbrk B
      | o = \subseteq
      | r = A
      | c = {{Defof|Inverse Image Mapping}}
}}
{{eqn | ll = \leadstoandfrom
      | l = B
      | o = \subseteq
      | r = T \setminus f \sqbrk {S \setminus A}
      | c = Preimage is Subset Iff Subset of Complement of Image of Complement
}}
{{eqn | r = T \setminus \map {f^\to} {S \setminus A}
      | c = {{Defof|Direct Image Mapping}}
}}
{{eqn | r = \relcomp T {\map {f^\to} {\relcomp S A} }
      | c = {{Defof|Relative Complement}}
}}
{{eqn | r = \map {\complement_T \circ f^\to \circ \complement_S} A
      | c = {{Defof|Composition of Mappings}}
}}
{{end-eqn}}
By definition of Galois connection:
:$\tuple{\complement_T \circ f^\to \circ \complement_S, f^\gets}$ is a Galois connection
It follows that $f^\gets : \powerset T \to \powerset S$ is the lower adjoint to $\complement_T \circ f^\to \circ \complement_S : \powerset S \to \powerset T$
{{qed}}
Category:Images
Category:Preimages
70tv1hy1x0favrnfje3r02e1kd341c3
Theorem: Norm satisfying Parallelogram Law induced by Inner Product/Complex Case

Let $V$ be a vector space over $\R$.
Let $\norm \cdot : V \to \R$ be a norm on $V$ such that: 
:$\norm {x + y}^2 + \norm {x - y}^2 = 2 \paren {\norm x^2 + \norm y^2}$
for each $x, y \in V$.
Then the function $\innerprod \cdot \cdot : V \times V \to \C$ defined by: 
:$\ds \innerprod x y = \frac 1 4 \sum_{k \mathop = 0}^3 i^k \norm {x + i^k y}^2$
for each $x, y \in V$, is an inner product on $V$.
Further, $\norm {\, \cdot \,}$ is the inner product norm of $\struct {V, \innerprod \cdot \cdot}$.

Proof:
We write out:
:$\innerprod x y = \dfrac 1 4 \paren {\norm {x + y}^2 + i \norm {x + i y}^2 - \norm {x - y}^2 - i \norm {x - i y}^2}$
We show that $\innerprod \cdot \cdot$ is an inner product.
Theorem: Interior of Set of Real Numbers in Complex Numbers is Empty

Let $\tuple {\C, d}$ be the complex Euclidean space.
Let $\R$ be the subspace of real numbers.
Then the interior of $\R$ in $\C$ is the empty set $\O$.

Proof:
{{AimForCont}} that: 
:$\R^\circ \ne \O$
Let $x \in \R^\circ$.
From the definition of an open subset of $\C$, there exists $\epsilon \in \R_{>0}$ such that:
:$\set {z \in \C : \cmod {z - x} < \epsilon} \subseteq \R^\circ$
Consider:
:$z = x + \dfrac \epsilon 2 i \in \C \setminus \R$
Then, we have:
:$\cmod {z - x} = \cmod {x + \dfrac \epsilon 2 i - x} = \dfrac \epsilon 2 < \epsilon$ 
Hence $z \in \R^\circ$.
But by the definition of interior, we have $\R^\circ \subseteq \R$. 
This contradicts the fact that $z \in \C \setminus \R$.
{{qed}}
Category:Interior of Set of Real Numbers in Complex Numbers is Empty
Category:Examples of Set Interiors
Category:Complex Numbers
Category:Real Numbers
5z3h4wp57kktjt21n813rkgxiwv9r6a
Theorem: Interior of Set of Real Numbers in Complex Numbers is Empty/Corollary

Let $\tuple {\C, d}$ be the complex Euclidean space.
Consider $S \subseteq \R$ as a topological subspace of $\tuple {\C, d}$.
Then the interior of $S$ in $\C$ is the empty set $\O$.

Proof:
From Interior of Subset we have:
:$S^\circ \subseteq \R^\circ$
From Interior of Set of Real Numbers in Complex Numbers is Empty, we have:
:$\R^\circ = \O$
Hence $S^\circ \subseteq \O$ and so:
:$S^\circ = \O$
from Subset of Empty Set.
{{qed}}
Category:Interior of Set of Real Numbers in Complex Numbers is Empty
d3kct1pun8nhuzs13zh4hkdctsywzhv
Theorem: Localic Functor is Covariant

Let $\mathbf{Top}$ denote the category of topological spaces.
Let $\mathbf{Loc_*}$ denote the category of locales with localic mappings.
Then:
:the localic functor $\mathbf {Lc} : \mathbf{Top} \to \mathbf{Loc_*}$ is a covariant functor

Proof:
=== Object Functor is Well-Defined ===
Let $T$ be a topological space.
By definition of localic object functor:
:$\map {\mathbf {Lc}} T$ is the locale of $T$
From Locale of Topological Space is Locale:
:$\map {\mathbf {Lc}} T$ is a locale
By definition of category of locales with localic mappings:
:$\map {\mathbf {Lc}} T$ is an object of $\mathbf{Loc_*}$
It follows that the object functor of $\mathbf{Lc}$ is well-defined.
{{qed|lemma}}
Theorem: Power in Prime Ideal

Let $A$ be a commutative ring with unity.
Let $\mathfrak p \subseteq A$ be a prime ideal.
Let $n > 0$ be a natural number.
Then for all elements $a \in A$, if $a^n \in \mathfrak p$ then $a \in \mathfrak p$.

Proof:
Proof by induction:
Theorem: Poisson Distribution Approximated by Normal Distribution

Let $X$ be a discrete random variable which has the Poisson distribution $\Poisson \lambda$.
Then for large $\lambda$:
:$\Poisson \lambda \approx \Gaussian \lambda \lambda$
where $\Gaussian \lambda \lambda$ denotes the normal distribution.

Proof:
{{MissingLinks}}
{{tidy}}
Let $n$ be a sufficiently large number.
Let $X_1,X_2,\dots X_n$ be independent and identically distributed random variables such that they have a $\Poisson {\frac{\lambda}{n}}$ distribution.
It follows from Expectation of Poisson Distribution and Variance of Poisson Distribution that $\mu = \expect{X_i} = \frac{\lambda}{n}$ and $\sigma^2 = \var{X_i} = \frac{\lambda}{n}$.
Let $\ds S=\sum_{i=1}^n X_i$. It follows from Sum of Independent Poisson Random Variables is Poisson that $S\sim \Poisson {n\frac{\lambda}{n}} = \Poisson \lambda$.
It follows from Central Limit Theorem that $\ds \frac{S-n\mu}{\sqrt{n\sigma^2}} = \frac{S-\lambda}{\sqrt{\lambda}}$ is distributed approximately as a standarized normal distribution, then it follows that: 
:$(1): \quad \map {F_{\frac{S-\lambda}{\sqrt{\lambda}}}} {x} \approx \map {F_{\Gaussian 0 1}} {x}$
where $\map {F_X} {x}$ is the cumulative distribution function.
Then:
{{begin-eqn}}
{{eqn | l = \map {F_{S} } {x}
      | r = \map \Pr {S \le x}
      | c = Definition of the cumulative distribution function.
}}
{{eqn | r = \map \Pr {S - \lambda \le x - \lambda}
}}
{{eqn | r = \map \Pr {\frac{S - \lambda}{\sqrt{\lambda} } \le \frac{x - \lambda}{\sqrt{\lambda} } }
}}
{{eqn | r = \map {F_{\frac{S - \lambda}{\sqrt{\lambda} } } } { \frac{x - \lambda}{\sqrt{\lambda} } }
}}
{{eqn | o = \approx
      | r = \map {F_{\Gaussian 0 1 } } { \frac{x - \lambda}{\sqrt{\lambda} } }
      | c = Using equation $\paren{1}$.
}}
{{eqn | r = \map \Pr {\Gaussian 0 1 \le \frac{x - \lambda}{\sqrt{\lambda} } }
}}
{{eqn | r = \map \Pr {\sqrt{\lambda} \Gaussian 0 1 + \lambda \le x}
}}
{{eqn | r = \map \Pr {\Gaussian \lambda \lambda \le x}
      | c = Using Linear Transformation of Normal Random Variable.
}}
{{eqn | r = \map {F_{\Gaussian \lambda \lambda} } x
}}
{{end-eqn}}
{{qed}}
Theorem: Extension of Continuous Complex-Valued Function Vanishing at Infinity to Alexandroff Extension is Continuous/Corollary

Let $X$ be a locally compact Hausdorff space.
Let $f : X \to \C$ be a continuous complex-valued function vanishing at infinity.
Then $f \sqbrk X \cup \set 0$ is compact.

Proof:
Let $X^\ast = X \cup \set p$ be the Alexandroff extension of $X$.
From Alexandroff Extension is Compact, $X^\ast$ is compact.
Define $f^\ast : X^\ast \to \C$ by taking:
:$\map {f^\ast} x = \begin{cases}\map f x & x \in X \\ 0 & x = p\end{cases}$
for each $x \in X^\ast$. 
From Extension of Continuous Complex-Valued Function Vanishing at Infinity to Alexandroff Extension is Continuous, $f^\ast$ is continuous.
From Continuous Image of Compact Space is Compact, $f^\ast \sqbrk {X^\ast}$ is compact.
We have:
{{begin-eqn}}
{{eqn	| l = f^\ast \sqbrk {X^\ast}
		| r = \set {\map {f^\ast} x : x \in X \cup \set p}
		| c = {{Defof|Alexandroff Extension}}
}}
{{eqn	| r = \set {\map {f^\ast} x : x \in X} \cup \set {\map {f^\ast} p}
}}
{{eqn	| r = \set {\map f x : x \in X} \cup \set 0
}}
{{eqn	| r = f \sqbrk X \cup \set 0
}}
{{end-eqn}}
Hence $f \sqbrk X \cup \set 0$ is compact.
{{qed}}
Category:Extension of Continuous Complex-Valued Function Vanishing at Infinity to Alexandroff Extension is Continuous
75tuy3h8p098xepvvnf4udr0p1wslu0
Theorem: Reciprocal of Continuous Complex-Valued Function Vanishing at Infinity does not Vanish at Infinity

Let $X$ be a locally compact Hausdorff space. 
Let $f : X \to \C$ be a continuous function that vanishes at infinity such that:
:$\map f x \ne 0$ for each $x \in X$.
Then $\dfrac 1 f : X \to \C$ does not vanish at infinity.

Proof:
From Quotient Rule for Continuous Complex Functions:
:$\dfrac 1 f$ is continuous.
{{AimForCont}} $\dfrac 1 f$ vanishes at infinity.
Then from Continuous Complex-Valued Function Vanishing at Infinity is Bounded and Attains Supremum, $\dfrac 1 f$ is bounded.
Since $f$ vanishes at infinity, for each $n \in \N$ there exists a compact set $K_n \subseteq X$ such that:
:$0 < \cmod {\map f x} < \dfrac 1 n$ for each $x \in X \setminus K_n$ 
That is:
:$\cmod {\dfrac 1 {\map f x} } > n$ for each $x \in X \setminus K_n$
This contradicts that $\dfrac 1 f$ is bounded.
Hence $\dfrac 1 f$ does not vanish at infinity.
{{qed}}
Category:Complex-Valued Functions Vanishing at Infinity
nwlmb0ps94ahg3vbfjisscn7co95lou
Theorem: Unitization of Non-Unital Subalgebra of Unital Algebra is Isomorphic to Unital Subalgebra

Let $A$ be a unital algebra over $\C$.
Let $B$ be a subalgebra of $A$ that is not unital.
Let $B_+$ be the unitization of $B$.
Let $B \oplus \C {\mathbf 1}_A$ be the (internal) direct sum of $B$ and $\C {\mathbf 1}_A$. 
Define $f : B_+ \to B \oplus \C {\mathbf 1}_A$ by:
:$\map f {b, \lambda} = b + \lambda {\mathbf 1}_A$
for each $\tuple {b, \lambda} \in B_+$. 
Then $f$ is a unital algebra isomorphism.

Proof:
Since:
:$B \oplus {\mathbf 1}_A = \set {b + \lambda {\mathbf 1}_A : b \in B, \, \lambda \in \C} = \set {\map f {b, \lambda} : \tuple {b, \lambda} \in B_+}$
we have that $f$ is a surjection.
We show that $f$ is linear.
Let $\tuple {b_1, \lambda_1}, \tuple {b_2, \lambda_2} \in B_+$ and $t \in \C$.
We then have:
{{begin-eqn}}
{{eqn	| l = \map f {b_1, \lambda_1} + t \map f {b_2, \lambda_2}
		| r = \paren {b_1 + \lambda_1 {\mathbf 1}_A} + t \paren {b_2 + \lambda_2 {\mathbf 1}_A}
}}
{{eqn	| r = \paren {b_1 + t b_2} + \paren {\lambda_1 + t \lambda_2} {\mathbf 1}_A
}}
{{eqn	| r = \map f {b_1 + t b_2, \lambda_1 + t \lambda_2}
}}
{{eqn	| r = \map f {\tuple {b_1, \lambda_1} + t \tuple {b_2, \lambda_2} }
}}
{{end-eqn}}
So $f$ is indeed linear.
Further we have:
{{begin-eqn}}
{{eqn	| l = \map f {b_1, \lambda_1} \map f {b_2, \lambda_2}
		| r = \paren {b_1 + \lambda_1 {\mathbf 1}_A} \paren {b_2 + \lambda_2 {\mathbf 1}_A}
}}
{{eqn	| r = b_1 b_2 + \lambda_1 b_2 + \lambda_2 b_1 + \lambda_1 \lambda_2 {\mathbf 1}_A 
}}
{{eqn	| r = \map f {b_1 b_2 + \lambda_1 b_2 + \lambda_2 b_1, \lambda_1 \lambda_2}
}}
{{eqn	| r = \map f {\tuple {b_1, \lambda_1} \tuple {b_2, \lambda_2} }
}}
{{end-eqn}}
So $f$ is an algebra homomorphism.
From Linear Transformation is Injective iff Kernel Contains Only Zero, to finish we only need to show that $\ker f = \set { \tuple { {\mathbf 0}_A, 0} }$.
Suppose that:
:$\map f {b, \lambda} = 0$
for $\tuple {b, \lambda} \in B_+$.
Suppose first that $\lambda \ne 0$. 
From:
:$b = -\lambda {\mathbf 1}_A$
we then have:
:${\mathbf 1}_A = -\lambda^{-1} b \in B$ 
This contradicts that $B$ is not unital.
Hence we have $\lambda = 0$.
Then we have $b = {\mathbf 0}_A$.
Hence $\ker f = \set { \tuple { {\mathbf 0}_A, 0} }$.
So $f$ is an algebra isomorphism.
Finally, we have:
:$\map f { {\mathbf 0}_A, 1} = {\mathbf 1}_A$
so $f$ is a unital algebra isomorphism.
{{qed}}
Category:Algebras
Category:Unitizations of Algebras over Fields
t0t7ivkzi4e3uahbg2tw79knjtq33ea
Theorem: Image of Group of Units in Unital Algebra under Unital Algebra Homomorphism

Let $R$ be a ring.
Let $A, B$ be unital $R$-algebras.
Let $\phi : A \to B$ be an unital algebra homomorphism.
Let $\map G A$ and $\map G B$ the groups of units of $A$ and $B$ respectively. 
Then:
:$\phi \sqbrk {\map G A} \subseteq \map G B$

Proof:
Let ${\mathbf 1}_A$ be the identity element of $A$. 
Let $x \in \map G A$.
Then there exists $y \in A$ such that $x y = y x = {\mathbf 1}_A$. 
We then have $\map \phi {x y} = \map \phi {y x} = \map \phi { {\mathbf 1}_A} = {\mathbf 1}_B$ since $\phi$ is a unital algebra homomorphism.
Since $\phi$ is an algebra homomorphism, we have:
:$\map \phi x \map \phi y = \map \phi y \map \phi x = {\mathbf 1}_B$
Hence $\map \phi y$ is the inverse of $\map \phi x$ in $B$. 
So $\map \phi x \in \map G B$. 
Hence:
:$\phi \sqbrk {\map G A} \subseteq \map G B$
{{qed}}
Category:Algebras
Category:Image of Group of Units in Unital Algebra under Unital Algebra Homomorphism
g5zm5nr2sefg02p43uofx8whtoods59
Theorem: Spectrum of Image of Element of Unital Algebra under Unital Algebra Homomorphism

Let $A, B$ be unital algebras over $\C$.
Let $\phi : A \to B$ be a unital algebra homomorphism.
Let $x \in A$.
We then have:
:$\map {\sigma_B} {\map \phi x} \subseteq \map {\sigma_A} x$ 
where $\sigma_A$ and $\sigma_B$ denote spectra in $A$ and $B$ respectively. 
If $\phi$ is a unital algebra isomorphism, we further have $\map {\sigma_B} {\map \phi x} = \map {\sigma_A} x$.

Proof:
We show that:
:$\map {\rho_A} x \subseteq \map {\rho_B} {\map \phi x}$
where $\rho_A$ and $\rho_B$ denote the resolvent sets in $A$ and $B$ respectively.
Let $\lambda \in \map {\rho_A} x$.
Then there exists $y \in A$ such that $\paren {\lambda {\mathbf 1}_A - x} y = y \paren {\lambda {\mathbf 1}_A - x} = {\mathbf 1}_A$.
Hence we have:
:$\map \phi {\paren {\lambda {\mathbf 1}_A - x} y} = \map \phi {y \paren {\lambda {\mathbf 1}_A - x} } = \map \phi { {\mathbf 1}_A} = {\mathbf 1}_B$
since $\phi$ is a unital algebra homomorphism.
Since $\phi$ is an algebra homomorphism, we have:
:$\map \phi {\lambda {\mathbf 1}_A - x} \map \phi y = \map \phi y \map \phi {\paren {\lambda {\mathbf 1}_A - x} } = {\mathbf 1}_B$
Hence $\map \phi y$ is an inverse for $\map \phi {\lambda {\mathbf 1}_A - x}$.
Since $\phi$ is an algebra homomorphism, we have $\map \phi {\lambda {\mathbf 1}_A - x} = \lambda {\mathbf 1}_B - \map \phi x$. 
Hence $\lambda \in \map {\rho_B} {\map \phi x}$. 
So we have:
:$\map {\rho_A} x \subseteq \map {\rho_B} {\map \phi x}$
Hence:
:$\map {\sigma_B} {\map \phi x} \subseteq \map {\sigma_A} x$ 
If $\phi$ is a unital algebra isomorphism, we have that $\phi^{-1} : B \to A$ is also a unital algebra isomorphism from Inverse of Algebraic Structure Isomorphism is Isomorphism: General Result.
Hence we have:
:$\map {\sigma_A} {\map {\phi^{-1} } y} \subseteq \map {\sigma_B} y$ 
for each $y \in B$. 
For $x \in A$, we can set $y = \map \phi x$ to obtain:
:$\map {\sigma_A} x \subseteq \map {\sigma_B} {\map \phi x}$
We therefore obtain:
:$\map {\sigma_A} x = \map {\sigma_B} {\map \phi x}$ 
{{qed}}
Category:Spectrum of Image of Element of Unital Algebra under Unital Algebra Homomorphism
Category:Spectra (Spectral Theory)
arg8x8zfez980v5n2xx7iejnnqt7zuf
Theorem: Subalgebra Generated by Self-Adjoint Set is Self-Adjoint

Let $\tuple {A, \ast}$ be a $\ast$-algebra over $\C$. 
Let $S \subseteq A$ be self-adjoint.
Let $K \sqbrk S$ be the subalgebra generated by $S$.
Then $\C \sqbrk S$ is a $\ast$-subalgebra of $A$.

Proof:
From Explicit Form for Generated Subalgebra, we have:
:$\C \sqbrk S = \map \span \AA$
where:
:$\AA = \set {x_1^{k_1} x_2^{k_2} \ldots x_n^{k_n} : x_1, \ldots, x_n \in S, \, k_1, \ldots, k_n \ge 1}$
From Star of Product of Elements in *-Algebra we have:
:$\paren {x_1^{k_1} x_2^{k_2} \ldots x_n^{k_n} }^\ast = x_n^{k_n} \ldots x_2^{k_2} x_1^{k_1} \in S$
Hence $\AA$ is self-adjoint.
Then $\C \sqbrk S$ is self-adjoint from Linear Span of Self-Adjoint Subset of *-Algebra is Self-Adjoint.
Hence $\C \sqbrk S$ is a $\ast$-subalgebra of $A$.
{{qed}}
Category:*-Algebras
ovn6452in9vn4ftafbgtr6m6ndovz7p
Theorem: Linear Span of Self-Adjoint Subset of *-Algebra is Self-Adjoint

Let $\tuple {A, \ast}$ be a $\ast$-algebra over $\C$. 
Let $S \subseteq A$ be self-adjoint.
Then $\map \span S$ is self-adjoint.

Proof:
Let:
:$\ds \sum_{i \mathop = 1}^n \lambda_i x_i \in \map \span S$
where $\lambda_1, \ldots, \lambda_n \in \C$ and $x_1, \ldots, x_n \in S$.
From $(\text C^\ast 2)$ and $(\text C^\ast 3)$ in the definition of an involution, we have:
:$\ds \paren {\sum_{i \mathop = 1}^n \lambda_i x_i}^\ast = \sum_{i \mathop = 1}^n \overline {\lambda_i} x_i^\ast$
Since $S$ is self-adjoint, we have $x_i^\ast \in S$ for each $i$.
Hence we have:
:$\ds \sum_{i \mathop = 1}^n \overline {\lambda_i} x_i^\ast \in \map \span S$
Hence $\map \span S$ is self-adjoint.
{{qed}}
Category:*-Algebras
q7hhfn343go7fmh0sjioeigrpq8wqpc
Theorem: Star of Convergent Sequence in Banach *-Algebra Converges

Let $\struct {A, \ast}$ be a $\ast$-algebra over $\C$.
Let $\sequence {x_n}_{n \in \N}$ be a convergent sequence in $A$ with:
:$x_n \to x$ 
Then:
:$x_n^\ast \to x^\ast$

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = \norm {x_n^\ast - x^\ast}
		| r = \norm {\paren {x_n - x}^\ast} 
		| c = $(\text C^\ast 2)$, $(\text C^\ast 4)$ in definition of involution
}}
{{eqn	| r = \norm {x_n - x}
		| c = {{Defof|Banach *-Algebra}}
}}
{{eqn	| o = \to
		| r = 0
		| c = Sequence in Normed Vector Space Convergent to Limit iff Norm of Sequence minus Limit is Null Sequence
}}
{{end-eqn}}
so:
:$x_n^\ast \to x^\ast$
{{qed}}
Category:Banach *-Algebras
dxx6cx1jn61xfcphu6j46m47bvaes3o
Theorem: Closure of Self-Adjoint Subset of Banach *-Algebra is Self-Adjoint

Let $\struct {A, \ast}$ be a $\ast$-algebra over $\C$.
Let $S \subseteq A$ be self-adjoint.
Then the closure $S^-$ of $S$ is self-adjoint.

Proof:
Let $x \in S^-$. 
From Point in Closure of Subset of Metric Space iff Limit of Sequence, there exists a sequence $\sequence {x_n}_{n \mathop \in \N}$ in $S$ with $x_n \to x$. 
Since $S$ is self-adjoint, we have $x_n^\ast \in S$. 
From Star of Convergent Sequence in Banach *-Algebra Converges, we have $x_n^\ast \to x^\ast$. 
From Point in Closure of Subset of Metric Space iff Limit of Sequence, we have $x^\ast \in S^-$. 
Hence if $x \in S^-$, we have $x^\ast \in S^-$. 
So $S^-$ is self-adjoint.
{{qed}}
Category:Banach *-Algebras
mhbytyp2i8442nv9ira87kytobkgje7
Theorem: C*-Algebra Generated by Commutative Self-Adjoint Set is Commutative

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $S \subseteq A$ be a self-adjoint set such that:
:$x y = y x$ for each $x, y \in S$. 
Let $\map {\text C^\ast} S$ be the $\text C^\ast$-algebra generated by $S$. 
Then $\map {\text C^\ast} S$ is commutative.

Proof:
Let $C$ be the subalgebra generated by $S$. 
From Subalgebra Generated by Commuting Elements is Commutative, $C$ is commutative.
From Explicit Form for Generated C*-Algebra, we have $\map {\text C^\ast} S = C^-$. 
From Closure of Commutative Set in Banach Algebra is Commutative, $C^-$ is commutative.
Hence $\map {\text C^\ast} S$ is commutative.
{{qed}}
Category:C*-Algebras
e20ocsnwbmgp6slfw9lsfodiqozjeyg
Theorem: Spectrum of Hermitian Element in Unital C*-Algebra is Real

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra.
Let $x \in A$ be Hermitian. 
Let $\map {\sigma_A} x$ denote the spectrum of $x$ in $A$.
Then $\map {\sigma_A} x \subseteq \R$.

Proof:
Let $A' \subseteq A$ be the $\text C^\ast$-algebra generated by $\set { {\mathbf 1}_A, x}$. 
By C*-Algebra Generated by Commutative Self-Adjoint Set is Commutative, $A'$ is commutative.
Let $\Phi_{A'}$ be the spectrum of $A'$.
From Spectrum of Element of Unital C*-Subalgebra of Unital C*-Algebra, we have:
:$\map {\sigma_A} x = \map {\sigma_{A'} } x$
From Spectrum of Element of Unital Commutative Banach Algebra, we have $\map {\sigma_A} x = \map {\sigma_{A'} } x = \set {\map \phi x : \phi \in \Phi_{A'} }$. 
From Character on Unital C*-Algebra is Real at Hermitian Elements, we have $\map \phi x \in \R$ for each $\phi \in \Phi_{A'}$. 
Hence $\map {\sigma_A} x \subseteq \R$. 
{{qed}}
Category:C*-Algebras
Category:Hermitian Elements of *-Algebras
6w9hrxg4hvy5p12gtiwr47byxfqacit
Theorem: Complete Boolean Lattice is a Frame

Let $\struct{B, \vee, \wedge, \neg, \preceq}$ be a complete Boolean lattice.
Then:
:$\struct{B, \vee, \wedge, \preceq}$ is a frame.

Proof:
From Boolean Lattice is Heyting Lattice:
:$\struct{B, \vee, \wedge, \preceq}$ is a complete Heyting lattice.
From Characterization of Locale:
:$\struct{B, \vee, \wedge, \preceq}$ is a frame.
{{qed}}
Category:Boolean Lattices
Category:Frames
jf74ombbcrepcbhnlt4bh7wdg3iuybs
Theorem: Complete Boolean Lattice is a Locale

Let $\struct{B, \vee, \wedge, \neg, \preceq}$ be a complete Boolean lattice.
Then:
:$\struct{B, \vee, \wedge, \preceq}$ is a locale.

Proof:
From Boolean Lattice is Heyting Lattice:
:$\struct{B, \vee, \wedge, \preceq}$ is a complete Heyting lattice.
From Characterization of Locale:
:$\struct{B, \vee, \wedge, \preceq}$ is a locale.
{{qed}}
Category:Boolean Lattices
Category:Locales
1d736s6333h98zpxue779ro7pbauzn4
Theorem: Finite Boolean Lattice is a Locale

Let $\struct{B, \vee, \wedge, \neg, \preceq}$ be a finite Boolean lattice.
Then:
:$\struct{B, \vee, \wedge, \preceq}$ is a locale.

Proof:
By definition of a lattice:
:$B$ admits all finite non-empty suprema and finite non-empty infima.
By definition of a Boolean lattice:
:$B$ has a greatest element and a smallest element.
From Infimum of Empty Set is Greatest Element and Supremum of Empty Set is Smallest Element:
:$B$ admits empty supremum and empty infimum.
Hence
:$B$ admits all supremum and infimum.
By definition of complete lattice:
:$B$ is complete
From Complete Boolean Lattice is a Locale:
:$B$ is a locale.
{{qed}}
Category:Boolean Lattices
Category:Locales
l39tlbo3pl4a5p87otzofkq26neajm5
Theorem: Two is Boolean Lattice

Let $\struct{\mathbf 2, \vee, \wedge, \neg, \preceq}$ be (Boolean lattice) two.
Then:
:$\struct{\mathbf 2, \vee, \wedge, \neg, \preceq}$ is a Boolean lattice.

Proof:
By definition of Boolean lattice two:
:$\struct{\mathbf 2, \vee, \wedge, \neg}$ is Boolean algebra two
From Two is Boolean Algebra:
:$\struct{\mathbf 2, \vee, \wedge, \neg}$ is a Boolean algebra
From Boolean Algebra is Equivalent to Boolean Lattice:
:$\struct{\mathbf 2, \vee, \wedge, \neg, \preccurlyeq}$ is a Boolean lattice
where:
:$\forall a, b \in \mathbf 2 : a \preccurlyeq b$ {{iff}} $a = a \wedge b$
By definition of Boolean algebra two:
:$\wedge$ is given by the Cayley table:
:<nowiki>$\begin{array}{c|cc}
 \land & \bot & \top \\ \hline
 \bot  & \bot & \bot \\
 \top  & \bot & \top
\end{array}$
</nowiki>
By manual checking it is seen that:
:$\preccurlyeq = \set{\tuple{\bot, \bot}, \tuple{\bot, \top}, \tuple{\top, \top}}$
By definition of Boolean lattice two:
:$\preceq = \set{\tuple{\bot, \bot}, \tuple{\bot, \top}, \tuple{\top, \top}}$
Hence:
:$\preceq = \preccurlyeq$.
The result follows.
{{qed}}
Category:Boolean Lattices
tqyz3627yn1tzgr4rkegq9ymvmjb2t7
Theorem: Two is a Locale

Let $\struct{\mathbf 2, \vee, \wedge, \neg, \preceq}$ denote (Boolean lattice) two.
Then:
:$\struct{\mathbf 2, \vee, \wedge, \preceq}$ is a locale.

Proof:
Follows immediately from:
* Two is Boolean Lattice
* Finite Boolean Lattice is a Locale
{{qed}}
Category:Boolean Lattices
Category:Locales
sucnmkknv7ukc9n7odqg53odogbhwga