ThmDex – An index of mathematical definitions, results, and conjectures.
Result R2959 on D3997: Even euclidean real function
Function even part is even
Formulation 0
Let $f : \mathbb{R}^n \to \mathbb{R}^m$ be a D4363: Euclidean real function such that
(i) $f_{\mathsf{even}} : \mathbb{R}^n \to \mathbb{R}^m$ is the D4692: Euclidean real function even part of $f$
Then $f_{\mathsf{even}}$ is an D3997: Even euclidean real function.
Formulation 1
Let $f : \mathbb{R}^n \to \mathbb{R}^m$ be a D4363: Euclidean real function such that
(i) \begin{equation} f_{\mathsf{even}} : \mathbb{R}^n \to \mathbb{R}^m, \quad f_{\mathsf{even}}(x) = \frac{1}{2} ( f(x) + f(-x)) \end{equation}
Then $f_{\mathsf{even}}$ is an D3997: Even euclidean real function.
Proofs
Proof 0
Let $f : \mathbb{R}^n \to \mathbb{R}^m$ be a D4363: Euclidean real function such that
(i) $f_{\mathsf{even}} : \mathbb{R}^n \to \mathbb{R}^m$ is the D4692: Euclidean real function even part of $f$
If $x \in \mathbb{R}$, then we may apply R480: Basic real addition is commutative to obtain \begin{equation} \begin{split} f_{\mathsf{even}}(-x) = \frac{f(-x) + f(x)}{2} = \frac{f(x) + f(-x)}{2} = f_{\mathsf{even}}(x) \end{split} \end{equation} $\square$