countably infinite type ≃ ℕ

Stream: Is there code for X?

[Violeta Hernández]

@Yury G. Kudryashov do we have this yet?

[Junyan Xu]

There are docs#denumerable.eqv, docs#denumerable.of_encodable_of_infinite, docs#encodable.nonempty_encodable

[Patrick Johnson]

import tactic

noncomputable example {α : Type*} [countable α] [infinite α] : α ≃ ℕ :=
begin
  haveI := encodable.of_countable α,
  haveI := denumerable.of_encodable_of_infinite α,
  exact denumerable.eqv α,
end

[Violeta Hernández]

Oh nice, didn't know about denumerable