Metamath Proof Explorer


Syntax definition crrx

Description: Extend class notation with generalized real Euclidean spaces.

Ref Expression
Assertion crrx class ℝ↑