Zulip Chat Archive

Stream: Is there code for X?

Topic: nat.eq_of_fin_equiv


view this post on Zulip Adam Topaz (Oct 27 2020 at 19:52):

Do we have something like this?

example {m n : } : fin m  fin n  m = n := sorry

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 19:58):

It seems that we don't have it. The proof can be extracted from src#invariant_basis_number_field

view this post on Zulip Adam Topaz (Oct 27 2020 at 19:58):

example {m n : } : fin m  fin n  m = n := λ h,
begin
  rw (show m = fintype.card (fin m), by simp),
  rw (show n = fintype.card (fin n), by simp),
  apply fintype.card_congr h
end

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 19:58):

or just by simpa using card_congr h

view this post on Zulip Adam Topaz (Oct 27 2020 at 20:06):

Okay, I'll add it as part of a PR for the category of finite sets. I need that lemma to show that the "Skeleton" is actually skeletal :)

view this post on Zulip Mario Carneiro (Oct 27 2020 at 20:07):

iff is better!

view this post on Zulip Adam Topaz (Oct 27 2020 at 20:07):

But how?! (the equivalence is not a prop)

view this post on Zulip Mario Carneiro (Oct 27 2020 at 20:08):

hm, good point

view this post on Zulip Adam Topaz (Oct 27 2020 at 20:09):

I also wanted to make it an iff. I guess using nonempty?

view this post on Zulip Mario Carneiro (Oct 27 2020 at 20:09):

yeah, at that point it's basically the same as the lemma in cardinal

view this post on Zulip Adam Topaz (Oct 27 2020 at 20:10):

Which lemma?

view this post on Zulip Mario Carneiro (Oct 27 2020 at 20:12):

src#cardinal.nat_cast_inj is the nearest

view this post on Zulip Adam Topaz (Oct 27 2020 at 20:12):

Oh, I see.

view this post on Zulip Adam Topaz (Oct 27 2020 at 20:18):

Okay, so you think the following is better?

lemma nat.fin_equiv_iff_eq {m n : } : nonempty (fin m  fin n)  m = n :=
  λ h⟩, by simpa using fintype.card_congr h, λ h, equiv.cast $ h  rfl  

view this post on Zulip Eric Wieser (Oct 28 2020 at 21:41):

The non-prop form of iff is (fin m ≃ fin n) ≃ (m = n), right?

view this post on Zulip Floris van Doorn (Oct 28 2020 at 21:42):

No, since fin n ≃ fin n has cardinality n! and n = n has cardinality 1.

view this post on Zulip Eric Wieser (Oct 28 2020 at 21:43):

Oops

view this post on Zulip Yury G. Kudryashov (Oct 28 2020 at 22:38):

The on-prop form is trunc (fin m ≃ fin n) ≃ (m = n)


Last updated: May 17 2021 at 16:26 UTC