## 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?

(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