= Tagged encoding of a finite tuple
{title2=$(a_i)_{i=1}^n\longmapsto\{\langle t_i,a_i\rangle:1\le i\le n\}$}
Using distinct fixed tags $t_1,\ldots,t_n$, encode a <finite tuple>[tuple] $(a_1,\ldots,a_n)$ by the <set> $\{\langle t_i,a_i\rangle:1\le i\le n\}$. <injection>[Injectivity] of the <ordered pair>[ordered-pair construction] makes the unique member with first coordinate $t_i$ recover $a_i$. Thus a <set> can retain the order of a <finite tuple> when its entries are tagged, even if some coordinates coincide.
Back to article page
