Cardinality of set

Stream: new members

[ROCKY KAMEN-RUBIO]

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]

s.card = \u n?

[Jalex Stark]

(deleted)

[ROCKY KAMEN-RUBIO]

This errors for me

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

[ROCKY KAMEN-RUBIO]

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]

I don't think set.card exists, but you can get something pretty natural-looking using cardinality

[Mario Carneiro]

import set_theory.cardinal

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