cardinality

Stream: new members

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