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
| $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