Cardinality

Stream: general

[Huyen Chau Nguyen]

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.

[Sean Leather]

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)

[Huyen Chau Nguyen]

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 ^^.

[Sean Leather]

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?

[Chris Hughes]

fintype.card is the function you want.

[Huyen Chau Nguyen]

@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 .

[Johannes Hölzl]

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.

[Johannes Hölzl]

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.