Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Topology and algebraic structures
Canonical embedding of the real numbers into a complete ordered field
crrext
Next ⟩
df-rrh
Metamath Proof Explorer
Unicode
Structured
Syntax definition
crrext
Description:
Extend class notation with the class of extension fields of
RR
.
Ref
Expression
Assertion
crrext
class RRExt