Operator Algebras in Lean

1.1 Definitions of \(C^{*}\)–algebras and \(W^{*}\)–algebras

Definition 9
#

A Banach \(*\)–algebra \(\mathcal{A}\) is called a \(C^{*}\)–algebra if it satisfies \(\| x^{*}x\| =\| x\| ^2\) for \(x\in \mathcal{A}\).

Definition 10

A \(C^{*}\)–algebra \(\mathcal{M}\) is called a \(W^{*}\)–algebra if it is a dual space as a Banach Space (i.e., if there exists a Banach space \(\mathcal{M}_{*}\) such that \((\mathcal{M}_{*})^{*}=\mathcal{M}\), where \((\mathcal{M}_{*})^{*}\) is the dual Banach space of \(\mathcal{M_{*}}\)). We call such a Banach Space \(\mathcal{M_{*}}\) the predual of \(\mathcal{M}\).