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
This is an old revision of the document!
$X$ |
$ Z\in \text{Fin}(X) $ |
---|
The set of finite subsets of $X$
$ Z\in \mathcal P(X) $ |
$\text{isFinite}(Z)$ |
---|
Mizar: FINSUB_1
Set constructor