cardinality of set of fintype?

Stream: Is there code for X?

[Chase Norman]

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]

You just need the set to be decidable:

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

[Kyle Miller]

If you're doing classical reasoning (like with open_locale classical) then the decidable_pred isn't necessary.

[Kyle Miller]

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]

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]

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]

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]

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]

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