Zulip Chat Archive

Stream: maths

Topic: find a term in a fintype


view this post on Zulip Kevin Buzzard (Apr 05 2020 at 16:48):

example (X : Type) [fintype X] (h : fintype.card X > 1) (e : X) : ∃ (f : X), f ≠ e := sorry

I've not used fintypes before and I don't just want to blunder in if this kind of stuff is done already. I'll happily be classical and noncomputable or whatever.

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 16:50):

Oh it's not hard to reduce to (∀ (f : X), f = e) -> card X <= 1

view this post on Zulip Reid Barton (Apr 05 2020 at 16:50):

I started thinking the same way and now I wonder if it's going the wrong direction

view this post on Zulip Reid Barton (Apr 05 2020 at 16:50):

You might also want to prove exists a b, a \ne b

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 16:51):

subsingleton -> card <= 1? that sounds like it might be in the library

view this post on Zulip Reid Barton (Apr 05 2020 at 16:51):

I agree it's more likely to be in the library but if it's not I think it's the wrong logical direction for the proof.

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 16:52):

Your exists statement feels similar. How about card >= 1 -> exists x?

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 16:52):

card >= 1 -> nonempty

view this post on Zulip Reid Barton (Apr 05 2020 at 16:52):

I'm not that familiar with the library either

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 16:52):

These statements look natural, I'll have a look in data.fintype

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 16:55):

Bingo. Now I knew what to look for it's not hard to find. fintype.card_pos_iff and fintype.card_le_one_iff

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 16:57):

And to top it all, fintype.exists_ne_of_one_lt_card is the question I originally asked :-) But these three lemmas are the only ones of this nature.

view this post on Zulip Scott Morrison (Apr 05 2020 at 22:56):

It would be good to have a pool of examples of "near-misses" for library_search, so we can know which improvements are worth making.


Last updated: May 14 2021 at 20:13 UTC