# 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