Conversion between Cardinal
and ℕ∞
#
In this file we define a coercion Cardinal.ofENat : ℕ∞ → Cardinal
and a projection Cardinal.toENat : Cardinal →+*o ℕ∞
.
We also prove basic theorems about these definitions.
Implementation notes #
We define Cardinal.ofENat
as a function instead of a bundled homomorphism
so that we can use it as a coercion and delaborate its application to ↑n
.
We define Cardinal.toENat
as a bundled homomorphism
so that we can use all the theorems about homomorphisms without specializing them to this function.
Since it is not registered as a coercion, the argument about delaboration does not apply.
Keywords #
set theory, cardinals, extended natural numbers
Coercion ℕ∞ → Cardinal
. It sends natural numbers to natural numbers and ⊤
to ℵ₀
.
See also Cardinal.ofENatHom
for a bundled homomorphism version.
Equations
Instances For
Alias of the reverse direction of Cardinal.ofENat_lt_ofENat
.
Alias of the reverse direction of Cardinal.ofENat_le_ofENat
.
Projection from cardinals to ℕ∞
. Sends all infinite cardinals to ⊤
.
We define this function as a bundled monotone ring homomorphism.
Equations
Instances For
The coercion Cardinal.ofENat
and the projection Cardinal.toENat
form a Galois connection.
See also Cardinal.gciENat
.
The coercion Cardinal.ofENat
and the projection Cardinal.toENat
form a Galois coinsertion.
Equations
Instances For
Alias of the reverse direction of Cardinal.ofENat_toENat_eq_self
.