Zulip Chat Archive

Stream: general

Topic: equiv (fin n x nat) nat


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 27 2021 at 09:21):

And maybe generalizes docs#fin_prod_fin_equiv

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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))

view this post on Zulip Johan Commelin (Feb 27 2021 at 09:40):

@Chris Hughes Nice! Thanks


Last updated: May 14 2021 at 04:22 UTC