Sequence end
Function
context
$ X $ … set
definiendum
$ \mathrm{last}: \mathrm{FiniteSequence}(X)\to X $
definiendum
$ \mathrm{last}(S):= \pi_{\mathrm{length}(S)}(S) $
Discussion
Parents
Subset of
Surjective function
Context
Sequence length