## Stream: Is there code for X?

### Topic: enumerating a fintype

#### Jalex Stark (Apr 23 2020 at 04:58):

I have a fintype of known cardinality, and I have a proposed enumeration of its elements. I want to show that this enumeration covers everything. I think I want the following theorem, which I don't understand fintype well enough to find / prove:

import tactic
example (α : Type) [fintype α] (X : finset α) (h : finset.card X = fintype.card α) : ∀ x : α, x ∈ X := begin
sorry
end


#### Mario Carneiro (Apr 23 2020 at 05:04):

I don't think we have this particular proof but it is not hard:

example (α : Type) [fintype α] (X : finset α) (h : finset.card X = fintype.card α) : ∀ x : α, x ∈ X :=
begin
suffices : finset.univ ⊆ X, {exact λ x, this (finset.mem_univ _)},
classical,
rw [← finset.sdiff_eq_empty_iff_subset, ← finset.card_eq_zero, finset.card_univ_diff],
simp [h]
end


wow, thanks!

#### Mario Carneiro (Apr 23 2020 at 05:05):

the key fact is finset.card_univ_diff

#### Mario Carneiro (Apr 23 2020 at 05:06):

there is also a constructive proof but meh

#### Mario Carneiro (Apr 23 2020 at 05:21):

actually there is an even better match, finset.eq_of_subset_of_card_le:

example (α : Type) [fintype α] (X : finset α) (h : finset.card X = fintype.card α) : ∀ x : α, x ∈ X :=
by rw finset.eq_of_subset_of_card_le (finset.subset_univ _) (ge_of_eq h);
apply finset.mem_univ
`

Last updated: May 07 2021 at 22:14 UTC