Database
BASIC STRUCTURES
Extensible structures
Definition of the structure quotient
cxrs
Next ⟩
df-ordt
Metamath Proof Explorer
Unicode
Structured
Syntax definition
cxrs
Description:
Extend class notation with the extended real number structure.
Ref
Expression
Assertion
cxrs
class RR*s