Database
BASIC ALGEBRAIC STRUCTURES
Generalized pre-Hilbert and Hilbert spaces
Orthocomplements and closed subspaces
ccss

Next ⟩ cthl

Metamath Proof Explorer

Ascii
Unicode

Syntax definition ccss

Description: Extend class notation with set of closed subspaces.

		Ref	Expression
	Assertion	ccss	$class ClSubSp$