subsets of fintypes

Stream: maths

[Antoine Chambert-Loir]

If αis a fintype and s : set α, how can one talk about the cardinality of s, for example, compare it to fintype.card α?
I skimmed through docs#finset and docs#fintype but couldn't guess the relevant coercion functions…

[Kevin Buzzard]

There is also docs#nat.card which will take an arbitrary type, and of course there's a coercion which will take the term s to the corresponding type (a subtype of alpha). But who knows if it will be nice to work with...

[Kevin Buzzard]

Alternatively you could probably noncomputably convert s into a finset. Is there docs#set.to_finset or docs#finset.of_set ? Aah, the first one exists but it needs a fintype instance on the coercion. Is it there? Note that I just guessed the name of the function instead of looking through the files ;-)

[Yaël Dillies]

Yup, it does

[Eric Rodriguez]

and to tie everything together there's docs#set.to_finset_card

[Kyle Miller]

If you have [decidable_eq α] (or have things suitably classical) then you should be able to do fintype.card s too.

[Antoine Chambert-Loir]

What I don't understand with these functions is that all of them have as an argument (sometimes implicit) the fact that ↥s is a fintype, so I even didn't try using them ? How does Lean guess about this ?
Actually, none of the following works :

import data.fintype.basic

variables (α : Type*) [decidable_eq α] [fintype α]

example (s : set α) :
  fintype.card s ≤ fintype.card α := sorry

example (s : set α) :
  fintype.card (set_fintype s) ≤ fintype.card α := sorry

example (s : set α) :
  fintype.card (set.to_fintype s) ≤ fintype.card α := sorry

example (s : set α) :
  fintype.card (finset.subtype s)  ≤ fintype.card α := sorry

[Yaël Dillies]

It's because of docs#set.fintype

[Kevin Buzzard]

Lean doesn't do magic -- any question you have about how something happens, you can find out from Lean by asking it directly.

[Kevin Buzzard]

set.fintype says that the "power set" of a finite type is finite.

[Johan Commelin]

@Antoine Chambert-Loir This works

import data.fintype.basic

variables (α : Type*) [fintype α]

open_locale classical

example (s : set α) :
  fintype.card s ≤ fintype.card α := sorry

[Johan Commelin]

To do it without open_locale classical you probably need to know that membership of s is decidable.

[Kyle Miller]

I forgot you needed [decidable_pred (∈ s)], not decidable_eq. Sorry for the incorrect advice

[Kyle Miller]

@Yaël Dillies That's for fintype (set α) -- docs#subtype.fintype is what gives individual sets their fintype instance

[Kevin Buzzard]

Yes Antoine you're not classical enough yet. If you write

import data.fintype.basic

variables (α : Type*) [fintype α]

open_locale classical

example (s : set α) :
  fintype.card s ≤ fintype.card α :=
begin
  sorry
end

and then click on fintype.card ↥s in the infoview you can see that it's using docs#subtype.fintype , and if you click on that you can see it is using classical.prop_decidable (a ∈ s), so now we know you can do

import data.fintype.basic

variables (α : Type*) [fintype α]

example (s : set α) [∀ a, decidable (a ∈ s)]:
  fintype.card s ≤ fintype.card α :=
begin
  sorry
end

[Kevin Buzzard]

and as Kyle says, [∀ a, decidable (a ∈ s)] is usually abbreviated [decidable_pred (∈ s)]

[Antoine Chambert-Loir]

Oh, I see! Actually, I'm glad to have fallen on a constructivism problem… Thanks to all of you.

[Yaël Dillies]

Kyle Miller said:

Yaël Dillies That's for fintype (set α) -- docs#subtype.fintype is what gives individual sets their fintype instance

Sorry, I meant docs#set_fintype. docs#subtype.fintype is defeq to it, but won't fire here.

[Yakov Pechersky]

docs#set.finite.to_finset

[Yakov Pechersky]

One can use that, and you know that s.finite by s.finite.of_fintype

[Yakov Pechersky]

The linking lemma to the approaches mentioned previously is docs#set.finite.card_to_finset