Set notation for Finsets

Stream: lean4

[Shreyas Srinivas]

I have been trying to work with Finsets for some CS related stuff. As a simple minimal example. I tried to define the following:

def card_n_subsets (n : ℕ) (X : Finset α) : Finset (Finset α) := {Y ∈ 𝒫 X | Y.card = n }

This throws an error since the set notation on the right of := means that Y is assumed to be a set. I get the error

invalid field 'card', the environment does not contain 'Set.card'
  Y
has type
  Set ?m.168`

Question : How can I smoothly use the set notation for Finsets?

[Yakov Pechersky]

The issue is in the powerset notation you used.

[Yakov Pechersky]

You should likely use docs#finset.powerset_len

[Shreyas Srinivas]

Thanks. Is there are a powerset notation for finite sets?

[Floris van Doorn]

There doesn't seem to be. Just use X.powerset.

[Kyle Miller]

There's not good support for using set notation for finsets.

One thing you can do is use set notation to create Sets and then use things such as docs4#Set.finite, docs4#Nat.card, docs4#finite, and docs4#Set.toFinset (among others)

[John Smith]

Hi, I'm new here and trying to learn Lean. Would anyone be willing to help me go through some problems?

[Jireh Loreaux]

@John Smith welcome! I suggest that you create a new thread to introduce yourself in the stream #new members. I'm sure there will be people who are happy to help. When you post there, why don't you indicate what sorts of problems you are interested in going through?