English
In a C*-algebra context with sufficient structure, the following nine conditions are equivalent: (list as in the statement).
Русский
В контексте C*-алгебры при наличии необходимой структуры выполняются взаимно эквивалентные девять условий: перечислены выше.
LaTeX
$$$\text{IsStrictlyPositive}(a) \iff \text{IsStrictlyPositive}(\sqrt{a}) \land a = \sqrt{a} \cdot \sqrt{a} \iff \text{IsUnit}(\sqrt{a}) \land a = \sqrt{a} \cdot \sqrt{a} \iff \exists b, \text{IsStrictlyPositive}(b) \land a = b \cdot b \iff \exists b, \text{IsUnit}(b) \land \text{IsSelfAdjoint}(b) \land a = b \cdot b \iff \exists b, \text{IsUnit}(b) \land a = \star b \cdot b \iff \exists b, \text{IsUnit}(b) \land a = b \cdot \star b \iff (0 \le a) \land \text{IsUnit}(a) \iff \text{IsSelfAdjoint}(a) \land \forall x \in \operatorname{spectrum}_{\mathbb{R}}(a), 0 < x$$$
Lean4
theorem _root_.CStarAlgebra.isStrictlyPositive_iff_isStrictlyPositive_sqrt_and_eq_sqrt_mul_sqrt {a : A} :
IsStrictlyPositive a ↔ IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a :=
CStarAlgebra.isStrictlyPositive_TFAE.out 0 1
