===== 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: [[http://mizar.org/JFM/Vol1/finsub_1.html|FINSUB_1]]

==== Parents ====
Set constructor
=== Related ===
[[Finite sequence]]