## Stream: maths

### Topic: find a term in a fintype

#### 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.

#### Kevin Buzzard (Apr 05 2020 at 16:50):

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

#### 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

#### Reid Barton (Apr 05 2020 at 16:50):

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

#### Kevin Buzzard (Apr 05 2020 at 16:51):

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

#### 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.

#### Kevin Buzzard (Apr 05 2020 at 16:52):

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

#### Kevin Buzzard (Apr 05 2020 at 16:52):

card >= 1 -> nonempty

#### Reid Barton (Apr 05 2020 at 16:52):

I'm not that familiar with the library either

#### Kevin Buzzard (Apr 05 2020 at 16:52):

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

#### 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

#### 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.

#### 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