Zulip Chat Archive

Stream: new members

Topic: Cardinality of set


view this post on Zulip 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.

view this post on Zulip Jalex Stark (Jul 10 2020 at 03:52):

s.card = \u n?

view this post on Zulip Jalex Stark (Jul 10 2020 at 03:52):

(deleted)

view this post on Zulip ROCKY KAMEN-RUBIO (Jul 10 2020 at 03:54):

This errors for me

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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