## Stream: general

### Topic: equiv (fin n x nat) nat

#### Johan Commelin (Feb 27 2021 at 09:14):

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 (Feb 27 2021 at 09:18):

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

#### Eric Wieser (Feb 27 2021 at 09:21):

And maybe generalizes docs#fin_prod_fin_equiv

#### Chris Hughes (Feb 27 2021 at 09:30):

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 (Feb 27 2021 at 09:32):

If you only need coutanble or less than

import data.equiv.encodable.basic

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


#### Chris Hughes (Feb 27 2021 at 09:35):

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 (Feb 27 2021 at 09:40):

@Chris Hughes Nice! Thanks

Last updated: Aug 03 2023 at 10:10 UTC