Characteristic Function (特性関数と $2^\kappa$) (Formula I.5.4)

• Characteristic Function (特性関数と $2^\kappa$) (Formula I.5.4) #Card
  • $\chi_A(x) := 1$ if $x \in A$, $0$ if $x \notin A$. なぜ $\operatorname{card} 2^X = \operatorname{card}({0,1}^X)$ か。

Back

The characteristic function of $A \subset X$: $$\chi_A(x) := \begin{cases} 1, & x \in A, \ 0, & x \notin A. \end{cases}$$

• $A \mapsto \chi_A$ が $2^X$（部分集合族）と ${0,1}^X$（写像空間）の全単射を与える。よって $\lambda^\kappa := \operatorname{card}(Y^X)$（$\lambda = \operatorname{card} Y$, $\kappa = \operatorname{card} X$）の記法で $2^\kappa = \operatorname{card} 2^X$。
• 測度論では指示関数 (indicator) として単関数近似の出発点。
• 記法: $A \subset_{fin} X \iff A \subset X \wedge \operatorname{card} A < \infty$（有限部分集合、$[X]^{<\omega}$ と同じ）。

Lean

Set.indicator / 全単射は Equiv.setProdEquivSigma 系ではなく Equiv.setEquivBoolFun（Set X ≃ (X → Bool)）