This is an old revision of the document!
Finite subset
Definition
| $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
Context
Set constructor
Subset of
Parents
