## Stream: new members

### Topic: Working with sets of finite cardinality

#### Patrick Lutz (Jul 08 2020 at 21:33):

I am having trouble figuring out how to do something very basic when working with finite sets. The following is an illustration of the kind of thing I can't figure out how to do:

import data.fintype.basic
example (X : Type) [fintype X] (a b c : X) (h : fintype.card X = 2)
(h1 : a ≠ b) (h2 : a ≠ c) (h3 : b ≠ c) : false := sorry


What's the best way to prove this kind of thing?

#### Mario Carneiro (Jul 08 2020 at 21:36):

I would try to prove that [a,b,c] induces a finset of size 3

#### Mario Carneiro (Jul 08 2020 at 21:40):

import data.fintype.basic
example (X : Type) [fintype X] (a b c : X) (h : fintype.card X = 2)
(h1 : a ≠ b) (h2 : a ≠ c) (h3 : b ≠ c) : false :=
begin
let S : finset X := ⟨[a,b,c], by simp *⟩,
have : 3 ≤ _ := finset.card_le_of_subset (finset.subset_univ S),
rw [finset.card_univ, h] at this,
exact absurd this dec_trivial,
end


#### Patrick Lutz (Jul 08 2020 at 22:42):

Nice, thanks. That works

Last updated: May 15 2021 at 00:39 UTC