cnpi - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > cnpi		GIF version

Syntax Definition cnpi 7213

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.

**Assertion**
Ref	Expression
cnpi	class N

See definition df-ni 7245 for more information.

Colors of variables: wff set class