Sequence length

Set

context $ X $
definiendum $ \mathrm{length}: \mathrm{Sequence}(X)\to\mathbb N\cup\{\infty\} $
definiendum $ \mathrm{length}(S):= \left|\mathrm{dom}(S)\right|$

Discussion

Parents

Subset of

Injective function

Context

Sequence

Refinement of

Set cardinality