Database
BASIC TOPOLOGY
Metric subcomplex vector spaces
Euclidean spaces
crrx
Next ⟩
cehl
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
crrx
Description:
Extend class notation with generalized real Euclidean spaces.
Ref
Expression
Assertion
crrx
class
ℝ↑