Zulip Chat Archive

Stream: new members

Topic: Definition of set.finite

Marcus Rossel (May 29 2021 at 17:25):

Why is docs#set.finite defined as nonempty (fintype ...)? Why is it important that the set is not empty?

Justus Springer (May 29 2021 at 17:34):

The nonempty here refers to docs#nonempty, which is a predicate on types, not on sets. It means that there exists a term of type fintype ↥s. Such a term consists of a finset together with a proof that these exhaust all of s (see docs#fintype).

Marcus Rossel (May 29 2021 at 17:57):

I'm not sure how the lifting from set to types works, but since s.finite = nonempty (fintype ↥s)I'm guessing that ↥s lifts s to the type level.
And I'm not sure if this is the part I don't understand, but I thought that this means that s = ∅ iff ↥s is uninhabited.
Would this equivalence then also extend to fintype ↥s?
That is, does it hold that for a finite set s: s = ∅ iff ↥s is uninhabited iff fintype ↥s is uninhabited?

Justus Springer (May 29 2021 at 18:27):

Exactly, ↥s is the coercion of s to a type. Namely, ↥s is the subtype {x // x ∈ s} of all elements x contained in s (see docs#set.has_coe_to_sort).

Justus Springer (May 29 2021 at 18:29):

s=∅ iff ↥s is uninhabited sounds good to me. I'm not sure about your second iff: fintype ↥s is inhabited iff s is finite, by definition. Therefore fintype ↥s is uninhabited iff s is infinite.

Last updated: Dec 20 2023 at 11:08 UTC