equiv from countable

Stream: Is there code for X?

[Yaël Dillies]

How can I get an equivalence from the integers to any infinite countable type? The only way I can find so far is through cardinal, which makes it look like we're missing API.

import data.countable.defs

instance nonempty_equiv_of_countable {α β : Type*} [countable α] [infinite α] [countable β]
  [infinite β] : nonempty (α ≃ β) := sorry

[Jireh Loreaux]

not an answer, but there are typos above. Some αs should be βs.

[Junyan Xu]

You can get there with
docs#denumerable.eqv
docs#denumerable.of_encodable_of_infinite
docs#encodable.of_countable
but using cardinal is probably easier.

[Eric Wieser]

import data.countable.defs
import set_theory.cardinal.basic

open_locale cardinal
namespace cardinal

lemma mk_eq_aleph_0 (α : Type*) [countable α] [infinite α] : #α = ℵ₀ :=
mk_le_aleph_0.antisymm $ aleph_0_le_mk _

end cardinal

instance nonempty_equiv_of_countable {α β : Type*} [countable α] [infinite α] [countable β]
  [infinite β] : nonempty (α ≃ β) :=
quotient.exact $ (cardinal.mk_eq_aleph_0 _).trans (cardinal.mk_eq_aleph_0 _).symm

[Yaël Dillies]

Beware, this proof sneakily unifies universes.

[Yaël Dillies]

Even accounting for this, cardinals win.

variables {α β : Type*}

instance nonempty_equiv_of_countable [countable α] [infinite α] [countable β] [infinite β] :
  nonempty (α ≃ β) :=
begin
  casesI nonempty_encodable α,
  casesI nonempty_encodable β,
  haveI := denumerable.of_encodable_of_infinite α,
  haveI := denumerable.of_encodable_of_infinite β,
  exact ⟨(denumerable.eqv _).trans (denumerable.eqv _).symm⟩,
end

instance nonempty_equiv_of_countable' [countable α] [infinite α] [countable β] [infinite β] :
  nonempty (α ≃ β) :=
(cardinal.eq.1 $ by simp_rw cardinal.mk_eq_aleph_0).map $
 λ e : ulift.{u_2} α ≃ ulift.{u_1} β, equiv.ulift.symm.trans $ e.trans equiv.ulift