0. Set of symbols
1. Alphabet
2. Deduction system
3. Theory
4. Zermelo-Fraenkel set theory
5. Set
6. Binary cartesian set product
7. Binary relation
8. Map
9. Function
10. Real function
11. Euclidean real function
12. Basic real function
13. Basic rational function
14. Basic integer function
15. Basic natural number function
16. Basic boolean function
Indicator function
Formulation 0
Let $X$ be a D11: Set.
The indicator function on $X$ with respect to $E \subseteq X$ is the D992: Function \begin{equation} X \to \{ 0, 1 \}, \quad x \mapsto \begin{cases} 1, \quad & x \in E \\ 0, \quad & x \in X \setminus E \end{cases} \end{equation}
Conventions
Convention 0 (Notation for indicator function) : Let $X$ be a D11: Set. We denote the D41: Indicator function on $X$ with respect to $E \subseteq X$ by $I_E$.
Subdefinitions
» D382: Heaviside function
Child definitions
» D4210: Indicator function operator
Results
» R1194: Indicator function of complement
» R3531: Pointwise product with indicator function is lower bound for unsigned basic function
» R1868: Composition of indicator function with set endomorphism
» R1193: Finite product of indicator functions equals indicator of intersection
» R4333: Binary product of indicator functions equals indicator of intersection
» R2370: Basic real arithmetic expression for cardinality of countable set
» R4565: Countable indicator partition of a euclidean real function
» R4566: Countable indicator partition of a complex function
» R4567: Countable indicator partition of a random euclidean real number
» R4568: Countable indicator partition of a random complex number
» R2966: Indicator function under scaling of the argument