ThmDex – An index of mathematical definitions, results, and conjectures.
Result R1868 on D41: Indicator function
Composition of indicator function with set endomorphism
Formulation 0
Let $f : X \to X$ be a D2660: Set endomorphism such that
(i) $E \subseteq X$ is a D78: Subset of $X$
(ii) $I_E : X \to \{ 0, 1 \}$ is the D41: Indicator function of $E$ within $X$
Then \begin{equation} I_E \circ f = I_{f^{-1}(E)} \end{equation}
Formulation 1
Let $f : X \to X$ be a D2660: Set endomorphism such that
(i) $E \subseteq X$ is a D78: Subset of $X$
(ii) $I_E : X \to \{ 0, 1 \}$ is the D41: Indicator function of $E$ within $X$
Then \begin{equation} \forall \, x \in X : I_E(f(x)) = I_{f^{-1}(E)}(x) \end{equation}
Proofs
Proof 0
Let $f : X \to X$ be a D2660: Set endomorphism such that
(i) $E \subseteq X$ is a D78: Subset of $X$
(ii) $I_E : X \to \{ 0, 1 \}$ is the D41: Indicator function of $E$ within $X$
We understand both functions $I_E$ and $I_{f^{-1}(E)}$ as functions from $X$ to $\{ 0, 1 \}$. Since the domain and codomain sets are the same, it suffices to show that they attain the same values on $X$. Since the claim holds vacuously if $X$ is empty, we may further assume that $X$ is nonempty.

If $x \in X$, then one has the following chain of equivalencies \begin{equation} \begin{split} (I_E \circ f)(x) = I_E(f(x)) = 1 \quad & \iff \quad f(x) \in E \\ & \iff \quad x \in f^{-1}(E) \\ & \iff \quad I_{f^{-1}(E)}(x) = 1 \\ \end{split} \end{equation} The claim now follows from R5199: Indicator function on set is uniquely defined by its support. $\square$