Definition of set.finite

Stream: new members

[Marcus Rossel]

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

[Justus Springer]

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]

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]

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]

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.