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