Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cnpi | Structured version Visualization version Unicode version |
Description: The set of positive
integers, which is the set of natural numbers
with 0 removed.
Note: This is the start of the Dedekind-cut construction of real and complex numbers. The last lemma of the construction is mulcnsrec 9965. The actual set of Dedekind cuts is defined by df-np 9803. |
Ref | Expression |
---|---|
cnpi |
Colors of variables: wff setvar class |
Copyright terms: Public domain | W3C validator |