> [!definition]
>
> Let $E, F$ be [[Banach Space|Banach spaces]], $\mu \in E^*$, $U \subset E_\mu^+$ be [[Open Set|open]], and $f: U \to F$ be a mapping. If for each $x \in U$, there exists $V_x \in \cn^o(x)$ *open in* $E$, and a local extension $f_x: V_x \to F$ such that $f_x$ is [$C^p$](Space%20of%20Continuously%20Differentiable%20Functions) and $f_x|_{U \cap V_x} = f_{U \cap V_x}$, then $f \in C^p(E_\mu^+, F)$.
> [!theorem]
>
> Let $\mu \in E^*$, $U \subset E_\mu^+$ be [[Relative Topology|relatively open]], and $f: U \to F$.
> 1. If $U \subset (E_\mu^+)^o$, then $f \in C^p$ in the above definition if and only if $f \in C^p$ in the ordinary definition.
> 2. $f \in C^p$ if and only if $f|_V \in C^p$ for all $V \subset U$ open.
>
> *Proof*. Since $U \subset E_\mu^+$ is relatively open, there exists $V \subset E$ open such that $U = E_{\mu}^+ \cap V$. Given that $U \subset (E_\mu^+)^o$, $U = (E_\mu^+)^o \cap V$ and is open in $E$ itself. If $f \in C^p$ in the ordinary sense, then $f$ itself is the desired extension for the alternate definition. Suppose that $f \in C^p$ in the above definition, then for any $x \in X$, $V_x \in \cn^o(x)$, and $f_x: V_x \to F$, $f_x|_{V_x \cap U} = f|_{V_x \cap U} \in C^p$. Hence $f \in C^p$.
>
> Suppose that $f \in C^p$ and let $V \subset U$ be open. Let $x \in V$, then there exists $V_x \in \cn^o(x)$ and $f_x: V_x \to F$ of class $C^p$. Since $f_x|_{U \cap V_x} = f_{U \cap V_x}$ and $U \supset V$, $f_x|_{V \cap V_x} = f_{V \cap V_x}$. Therefore $f|_V \in C^p$ for all $V \subset U$ open.
> [!theorem]
>
> Let $\mu \in E^*$ and $U \subset E$. Denote $\inte(U) = U \cap (E_\mu^+)^o$ and $\partial U = U \cap \ker(\mu)$. Let $f: U \to F$ be $C^p$, and $g$ be a local $C^p$ extension of $f$ about $x \in U$. Define
> $
> D^kf(x) = D^kg(x)
> $
> If $h$ is another $C^k$-extension of $f$ about $x \in U$, then there exists a neighbourhood $V \in \cn^o(x)$ in $U$ such that $g = h$, hence this derivative is well-defined. Moreover, $D^kf: U \to L^k(E, F)$ is of class $C^{p - k}$.
>
> *Proof*. Assume without loss of generality that $g$ and $h$ are both defined on $W \in \cn^o(x)$, in which case $g|_{W \cap U} = h|_{W \cap U} = f|_{W \cap U}$ by requirement. If $V = W \cap \inte(U)$, then since $W$ is open in $E$ and $x \in U$, $V \ne \emptyset$.
>
> If $x \in \inte(U)$, then $V$ is the desired neighbourhood. Since $V$ is also open in $E$, we have $g = h$ on an open set and $D^kg(x) = D^kh(x)$, so $D^kf(x)$ is well-defined.
>
> If $x \in \partial U$ (this implies that $\mu \ne 0$), then $W \cap U$ is the desired neighbourhood. More importantly, $g|_V = h|_V$ still, and $D^kg|_V = D^kh|_V$. Since $\mu \ne 0$, there exists $v \in E$ such that $\mu(v) > 0$, and there exists $\varepsilon > 0$ such that $x + tv \in V$ for all $t \in [0, \varepsilon)$. This allows using the continuity to obtain
> $
> D^kg(x) = \lim_{t \to 0}D^kg(x + tv) = \lim_{t \to 0}D^kh(x + tv) = D^kh(x)
> $
> Hence $D^kf(x)$ is well-defined.
>
> Lastly, since $D^kf(x) = D^kg(x)$ on $W \cap U$, $D^kf(x)$ is continuous on $W \cap U$. Similarly, $D^kg \in C^{p - k}$ is a desired local extension, so $D^kf \in C^{p - k}$.
> [!definition]
>
> Let $E, F$ be Banach spaces, $\mu \in E^*$, $v \in F^*$, and $U \subset E_\mu^+$ and $V \subset F_\nu^+$ be relatively open. Let $\iota: F_\nu^+ \to F$ be the inclusion map, and $f: U \to V$ be a mapping, then $f \in C^p$ if $\iota \circ f$ is.
>
> $f$ is a $C^p$-isomorphism if it admits a $C^p$ inverse.
> [!theorem]
>
> Let $U \subset E$ be open, $\mu \in E^*$ with $\mu \ne 0$, and $f: U \to F_\mu^+$ be a $C^p$-morphism ($p \ge 1$). If $f(x) \in \ker(\mu)$, then $\mu \circ Df(x) = 0$.
>
> *Proof*. If $\mu = 0$ then we're done. Assume without loss of generality that $x = 0$ and $f(x) = 0$. Let $W \in \cn^o(0)$, and $v \in E$ such that $\mu \circ Df(0)v \ne 0$, then for sufficiently small $t$,
> $
> f(tv) = tDf(0)v + o(t)w_t \quad w_t \in W
> $
> Since $f(tv) \in F_\mu^+$,
> $
> \begin{align*}
> t\mu \circ Df(0)v + o(t) \mu(w_t) &\ge 0 \\
> \mu \circ Df(0)v &\ge -\frac{o(t)}{t}\mu(w_t)
> \end{align*}
> $
> and $f(-tv) \in F_\mu^+$ as well,
> $
> \begin{align*}
> -t\mu \circ Df(0)v + o(-t) \mu(w_t) &\ge 0 \\
> \mu \circ Df(0)v &\ge \frac{o(-t)}{t}\mu(w_t)
> \end{align*}
> $
> Sending $t \to 0$ yields $\mu \circ Df(0)v = 0$, which contradicts with the assumption that $\mu \circ Df(0)v \ne 0$.
> [!theorem]
>
> Let $\lambda \in E^*$, $\mu \in F^*$, $U \subset E_\lambda^+$ relatively open, and $V \subset F_\mu^+$ relatively open, such that $U \cap \partial E_\lambda^+ \ne \emptyset$ and $V \cap \partial F_\mu^+ \ne \emptyset$. Let $f: U \to V$ be a $C^p$-isomorphism, then $\lambda \ne 0$ if and only if $\mu \ne 0$. If $\lambda \ne 0$ and $\mu \ne 0$, then $f$ induces a $C^p$-isomorphism of $\inte(U)$ on $\inte(V)$ and of $\partial U$ on $\partial V$.
>
> *Proof*. If $f$ is a $C^p$-isomorphism, then for any $x \in \inte{(U)}$, $Df(x)$ is a toplinear isomorphism, so $f(x) \in \text{int}(V)$. Thus the existence of the interior set in the domain and the target are equivalent, so $\lambda \ne 0$ if and only if $\mu \ne 0$. This induces a $C^p$ isomorphism $f|_{\inte(U)}: \inte(U) \to \inte(V)$.
>
> As for the boundary, $f|_{\partial U}: \partial U \to \partial V$ induces a bijection. By considering $\partial U$ and $\partial V$ as open subsets of $\ker (\mu)$, and splitting off a dimension, $f|_{\partial U}$ is a $C^p$-isomorphism.