Zulip Chat Archive

Stream: Is there code for X?

Topic: enumerating a fintype


view this post on Zulip 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```

view this post on Zulip 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

view this post on Zulip Jalex Stark (Apr 23 2020 at 05:05):

wow, thanks!

view this post on Zulip Mario Carneiro (Apr 23 2020 at 05:05):

the key fact is finset.card_univ_diff

view this post on Zulip Mario Carneiro (Apr 23 2020 at 05:06):

there is also a constructive proof but meh

view this post on Zulip 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