Theorem Cardinal.toNat_inj_of_lt_aleph0

Modification history