Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Syntax Definition chj 4972

Description: Extend class notation with join in C_ℋ.

**Assertion**
Ref	Expression
chj	class ∨_ℋ

See definition df-chj 5277 for more information.

Colors of variables: wff set class