# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: cardinality of set of fintype?

#### Chase Norman (Sep 29 2020 at 05:23):

Is there a way to express the cardinality of a set of a fintype as a natural number? I have a Prop that I would like to use to filter elements of a fintype into a subset. How might I write an expression to denote the cardinality of this set? Do I need to prove that the set of a fintype can be converted to a finset? I am having trouble constructively building the finset because of a problem with has_sep being unproven. Any ideas?

#### Kyle Miller (Sep 29 2020 at 05:28):

You just need the set to be decidable:

```
example (α : Type*) [fintype α] (s : set α) [decidable_pred s] : fintype.card s ≥ 0
```

#### Kyle Miller (Sep 29 2020 at 05:29):

If you're doing classical reasoning (like with `open_locale classical`

) then the `decidable_pred`

isn't necessary.

#### Kyle Miller (Sep 29 2020 at 05:33):

Also, if you want a finset from a set, there's `set.to_finset`

in `data.fintype.basic`

. For example, you could write `s.to_finset.card`

instead of `fintype.card s`

.

#### Chase Norman (Sep 29 2020 at 05:39):

Thank you for your response. How does one prove that a predicate is decidable? Also, is it generally possible in mathematics for a finite set to not have a cardinality if the predicate is not decidable?

#### Kevin Buzzard (Sep 29 2020 at 05:52):

A finite set has a cardinality, it's just that there might not be an algorithm to count it. For example if X is the set $\{\pi^2/6,\sum_{n=1}^{\infty}n^{-2}\}$ then $X$ has a cardinality which is either 1 or 2 depending on whether the two terms are equal or not. There's no *algorithm* for checking if a random infinite sum equals a value so asking a computer what it is is asking too much

#### Kyle Miller (Sep 29 2020 at 05:54):

`decidable_pred s`

is essentially that for every `x`

, you can write a function that can calculate true or false depending on whether `x ∈ s`

(try following the definitions for `decidable_pred`

to see how it works!). It depends on knowing precisely how `s`

is defined. In fact, using typeclasses Lean is able to fill in this detail for you for many simple cases (for example with `{n : ℕ | n = 5}`

).

In mathematics, finite sets have a cardinality, but it might not be known since one only knows a bijection to $\{1,2,\dots,n\}$ exists for some $n$, but in Lean finite sets come with an explicit list of the elements, so the cardinality must be known ahead of time.

#### Kevin Buzzard (Sep 29 2020 at 05:56):

If you're a mathematician and are finding all this confusing then the answer is simply to switch on "classical logic mode" (the mode which mathematicians use to do mathematics) with `open_locale classical`

and just forget about it

#### Kyle Miller (Sep 29 2020 at 06:02):

(Does mean "no classical reasoning" or "eliminate double negation"?)

Last updated: May 07 2021 at 22:14 UTC