Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Real subtraction
cresub
Next ⟩
df-resub
Metamath Proof Explorer
Ascii
Structured
Syntax definition
cresub
Description:
Real number subtraction.
Ref
Expression
Assertion
cresub
class
−
ℝ