English
An element a is strictly positive if and only if it is self-adjoint and its real spectrum is contained in (0, ∞).
Русский
Элемент a строго положителен тогда и только тогда, когда он самосопряжён и спектр Real(a) лежит в (0, ∞).
LaTeX
$$$\text{IsStrictlyPositive}(a) \iff \text{IsSelfAdjoint}(a) \land \forall x \in \sigma_{\mathbb{R}}(a),\; 0 < x$$$
Lean4
theorem _root_.CStarAlgebra.isStrictlyPositive_iff_isSelfAdjoint_and_spectrum_pos {a : A} :
IsStrictlyPositive a ↔ IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x :=
CStarAlgebra.isStrictlyPositive_TFAE.out 0 8
