Metamath Proof Explorer

Syntax definition crrh

Description: Map the real numbers into a complete field.

Ref Expression
Assertion crrh 
class RRHom