cho - Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Syntax Definition cho 8843

Description: Extend class notation with set of Hermitian Hilbert space operators.

**Assertion**
Ref	Expression
cho	class HrmOp

See definition df-hmop 9794 for more information.

Colors of variables: wff set class