Zulip Chat Archive

Stream: Is there code for X?

Topic: cardinality of set of fintype?


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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 {π2/6,n=1n2}\{\pi^2/6,\sum_{n=1}^{\infty}n^{-2}\} then XX 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

view this post on Zulip 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,,n}\{1,2,\dots,n\} exists for some nn, but in Lean finite sets come with an explicit list of the elements, so the cardinality must be known ahead of time.

view this post on Zulip 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

view this post on Zulip Kyle Miller (Sep 29 2020 at 06:02):

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


Last updated: May 07 2021 at 22:14 UTC