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