set.finite

A set is finite if the subtype is a fintype, i.e. there is a list that enumerates its members.

set.infinite

A set is infinite if it is not finite.

set.finite.to_finset

Get a finset from a finite set

set.decidable_mem_of_fintype

Membership of a subset of a finite type is decidable.

Using this as an instance leads to potential loops with subtype.fintype under certain decidability assumptions, so it should only be declared a local instance.

set.finite_subsets_of_finite

There are finitely many subsets of a given finite set