# Zulip Chat Archive

## Stream: new members

### Topic: Cardinality of set

#### ROCKY KAMEN-RUBIO (Jul 10 2020 at 03:47):

I have a `set`

(not a `finset`

, because it might have infinitely many elements) and I want to state that its cardinality is n as a `Prop`

. I see how I could do this for small numbers by stating that every element of the set is equal to one of n choices, and even define something recursively for any nat, but this feels like something that should exist that I'm not seeing.

#### Jalex Stark (Jul 10 2020 at 03:52):

`s.card = \u n`

?

#### Jalex Stark (Jul 10 2020 at 03:52):

(deleted)

#### ROCKY KAMEN-RUBIO (Jul 10 2020 at 03:54):

This errors for me

```
example (s : set ℕ) : s.card = ↑2 := sorry
```

#### ROCKY KAMEN-RUBIO (Jul 10 2020 at 03:55):

This thread deals with a similar question and the solution @Mario Carneiro gave was to use finset. Is there a way around that? is the point of having both `set`

and `finset`

that if we know a set is finite, then we show it can be coerced into a finset and then we get all the finset theorems?

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Working.20with.20sets.20of.20finite.20cardinality/near/203326402

#### Mario Carneiro (Jul 10 2020 at 03:57):

I don't think `set.card`

exists, but you can get something pretty natural-looking using cardinality

#### Mario Carneiro (Jul 10 2020 at 03:58):

```
import set_theory.cardinal
example (s : set ℕ) := cardinal.mk s = 2
```

Last updated: May 10 2021 at 19:16 UTC