Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Extended real and complex numbers, real and complex projective lines
The canonical bijection from the finite ordinals
ciomnn
Next ⟩
df-bj-iomnn
Metamath Proof Explorer
Ascii
Structured
Syntax definition
ciomnn
Description:
Syntax for the canonical bijection from
(
om u. {
om } )
onto
( NN0 u. { pinfty } )
.
Ref
Expression
Assertion
ciomnn
class
i
ω↪ℕ