List, length (LADR 1.8)
- List, length (LADR 1.8) #Card
- 長さ $n$ のリストとは？ 2つのリストが等しいのはいつ？ 集合との違いは？
非負整数 $n$ に対し、長さ $n$ のリストは $n$ 個の要素の順序づけられた集まり $(z_1,\dots,z_n)$。 2つのリストが等しい $\iff$ 長さが同じで、同じ要素が同じ順序で並ぶ。 集合との違い：リストでは順序が意味を持ち、重複も意味を持つ（$(3,5)\neq(5,3)$、$(4,4)\neq(4,4,4)$）。 長さは必ず有限の非負整数。$(x_1,x_2,\dots)$ は「無限長」でリストではない。$n$-tuple とも呼ぶ。
長さ $n$ のリストは Fin n → α（または List α で長さ固定）。順序対は Prod。