Product as Selections (積 = 選択関数の集合) (Section IV.5)
- Product as Selections (積 = 選択関数の集合) (Section IV.5) #Card
- A selection of a relation $R \subset J \times X$ is a map $\varphi : J \to X$ with $\varphi \subset R$ (i.e. $\varphi(j) \in R_j$ for each $j$); the product $\prod_{j \in J} R_j$ is the set of all selections.
Let $R \subset J \times X$. A map $\varphi : J \to X$ is a selection of $R$ if $\varphi \subset R$（graph が $R$ に含まれる、つまり $\varphi(j) \in R_j$ for each $j \in J$）. The set of all selections is the product $$\prod R = \prod_{j \in J} R_j.$$
- 一般の積 $\prod_{j \in J} X_j$ = $\varphi : J \to \bigcup_j X_j$ with $\varphi(j) \in X_j$ の全体。$X_j$ は factor、$p_j(\varphi) := \varphi(j)$ が $j$-th projection。
- 全因子が等しい場合 $\prod_{j \in J} X = X^J$（$J$-power）。
- $R_j \neq \emptyset$（各 $j$）のとき積が非空であることは選択公理と同値（Chapter XXVII 参照）。
(j : J) → X j（依存関数型）；選択公理は Classical.choice