This is an old revision of the document!
Finite sequence
Definition
| $Y$ |
| $ \text{seq}\in \text{FinSeq}(Y) $ |
|---|
| $ n\in \mathbb N $ |
| $\text{seq}: \text{seg}(n)\to Y$ |
Ramifications
Reference
Mizar: FINSEQ_1
Context
Special case of
Parents
This is an old revision of the document!
| $Y$ |
| $ \text{seq}\in \text{FinSeq}(Y) $ |
|---|
| $ n\in \mathbb N $ |
| $\text{seq}: \text{seg}(n)\to Y$ |
Mizar: FINSEQ_1
