Zulip Chat Archive

Stream: general

Topic: Cardinality


view this post on Zulip Huyen Chau Nguyen (Jun 22 2018 at 08:01):

Hey guys, I want to ask about the cardinality of sets. I'm totally newbie to Lean so the questions might be trivial and silly. Still, I need your help.

I would like to ask what is the function in mathlib that returns the number of elements of a set (of type set \N and not finset, but this set surely has a finite number of elements, it's not infinite set like R or N) and also which file i should have to import.

Thank you for your responses.

P.S.: I'm from Vn so please excuse-me for my English too.

view this post on Zulip Sean Leather (Jun 22 2018 at 08:06):

I haven't used set myself, but I think an answer can be found in data/set/finite.lean in mathlib:

def finite (s : set α) : Prop := nonempty (fintype s)

Then, looking at data/fintype.lean, we see:

class fintype (α : Type*) :=
(elems : finset α)
(complete :  x : α, x  elems)

view this post on Zulip Huyen Chau Nguyen (Jun 22 2018 at 08:20):

My prob is that i have to define my set as a set and not finset and then i need to count its size.
Thank you very much for your answer. I dont totally understand it yet but i would explore your hint with those files first and might ask you guys more later ^^.

view this post on Zulip Sean Leather (Jun 22 2018 at 08:29):

You might want to think how you would define cardinality yourself. Consider the definition of set:

def set (α : Type u) := α  Prop

Without additional information, how do you count the number of elements? How do you even know a given s : set α is finite? For example, is s : set ℕ (whose type reduces to ℕ → Prop) finite?

view this post on Zulip Chris Hughes (Jun 22 2018 at 08:50):

fintype.card is the function you want.

view this post on Zulip Huyen Chau Nguyen (Jun 22 2018 at 09:24):

@Sean Leather : my set is constructed from an argument n of integer, if n tends to inifinity then the set's number of element could tend to be infinite, but for any given n, the number of elements of that set is guaranteed to be bounded ( Im wondering if i misunderstood the notion of being finite :-? ).

@Chris Hughes okie thank you I'll check that out too .

view this post on Zulip Johannes Hölzl (Jun 22 2018 at 15:00):

If you know your set is bound by a natural number n you can write ((finset.range n).filter (λi, i < 3)).card, i.e. you first generate the finite set of all natural numbers up to n and then filter on a predicate (in this casei < 3). Then using card we compute the cardinality.

view this post on Zulip Johannes Hölzl (Jun 22 2018 at 15:02):

If you have a proof that a s : set α is finite (i.e. finite s), then you can use set.finite.to_finset to get the finset of a set.


Last updated: May 17 2021 at 22:15 UTC