Zulip Chat Archive

Stream: maths

Topic: subsets of fintypes


Antoine Chambert-Loir (Dec 06 2021 at 19:46):

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 (Dec 06 2021 at 19:48):

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 (Dec 06 2021 at 19:49):

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 (Dec 06 2021 at 19:50):

Yup, it does

Eric Rodriguez (Dec 06 2021 at 19:51):

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

Kyle Miller (Dec 06 2021 at 19:55):

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

Antoine Chambert-Loir (Dec 06 2021 at 20:05):

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 (Dec 06 2021 at 20:09):

It's because of docs#set.fintype

Kevin Buzzard (Dec 06 2021 at 20:11):

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 (Dec 06 2021 at 20:21):

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

Johan Commelin (Dec 06 2021 at 20:22):

@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 (Dec 06 2021 at 20:22):

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

Kyle Miller (Dec 06 2021 at 20:25):

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

Kyle Miller (Dec 06 2021 at 20:26):

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

Kevin Buzzard (Dec 06 2021 at 20:26):

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 (Dec 06 2021 at 20:27):

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

Antoine Chambert-Loir (Dec 06 2021 at 20:27):

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

Yaël Dillies (Dec 06 2021 at 20:29):

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 (Dec 06 2021 at 21:08):

docs#set.finite.to_finset

Yakov Pechersky (Dec 06 2021 at 21:10):

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

Yakov Pechersky (Dec 06 2021 at 21:13):

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


Last updated: Dec 20 2023 at 11:08 UTC