Finite subset

Set

$X$
$ Z\in \text{Fin}(X) $

The set of finite subsets of $X$

$ Z\in \mathcal P(X) $
$\text{isFinite}(Z)$

Ramifications

Reference

Mizar: FINSUB_1

Parents

Set constructor

Finite sequence