Metamath Proof Explorer


Syntax definition chdma1

Description: Extend class notation with preliminary map from vectors to functionals in the closed kernel dual space.

Ref Expression
Assertion chdma1 class HDMap1