Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Well-founded zero, successor, and limits
cwlim
Next ⟩
df-wsuc
Metamath Proof Explorer
Unicode
Structured
Syntax definition
cwlim
Description:
Declare the syntax for well-founded limit class.
Ref
Expression
Assertion
cwlim
class WLim ( R , A )