equiv (fin n x nat) nat

Stream: general

[Johan Commelin]

What is the best way to get an equiv between fin n \times nat and nat? I don't really care about any properties.

[Eric Wieser]

x.1 + n*x.2 and (y % n, y/n) feel like they should be easy to prove as inverses

[Eric Wieser]

And maybe generalizes docs#fin_prod_fin_equiv

[Chris Hughes]

import set_theory.cardinal_ordinal
import tactic

noncomputable example (n : nat) (h : 0 < n): fin n × ℕ ≃ ℕ :=
classical.choice $ cardinal.eq.1
  (begin
    rw [← cardinal.lift_id (cardinal.mk ℕ),
      cardinal.mk_prod, ← cardinal.omega, cardinal.mul_eq_right];
    simp [le_of_lt (cardinal.nat_lt_omega _), le_refl],
    norm_cast,
    omega
  end)

[Chris Hughes]

If you only need coutanble or less than

import data.equiv.encodable.basic

instance (n : ℕ) : encodable (fin n × ℕ) :=
by apply_instance

[Chris Hughes]

import data.equiv.denumerable

instance (n : ℕ) (h : 0 < n) : denumerable (fin n × ℕ) :=
@denumerable.of_encodable_of_infinite _ _
  (infinite.of_injective (λ i : nat, (fin.mk 0 h, i))
    (λ _ _, by simp))

[Johan Commelin]

@Chris Hughes Nice! Thanks