Every finite-dimensional face of the target ball is carried onto a face of the same dimension

Read-back. Let $X$ and $Y$ be arbitrary real normed spaces, and let $F:X\to Y$ be any function. Assume that $F$ restricts to a bijection of $B_X$ onto $B_Y$: $F(B_X)\subseteq B_Y$, $F$ is injective on $B_X$, and every point of $B_Y$ has a preimage in $B_X$. Assume that $F$ is $1$-Lipschitz on $B_X$: $\|F(x)-F(x')\|\le\|x-x'\|$ for all $x,x'\in B_X$. Let $C\subseteq Y$ be a sphere face of $B_Y$: $C$ is nonempty, convex, contained in $S_Y$, and whenever $y_1,y_2\in B_Y$ and a point of $C$ lies in $]y_1,y_2[$, then $y_1,y_2\in C$. Assume that the vector span $\operatorname{span}\{c-c':c,c'\in C\}$ is finite-dimensional. Let $D$ be the set $D=\{x\in X:\|x\|\le1,\ F(x)\in C\}$. Then all eight of the following hold.

1. $D$ is a sphere face of $B_X$: $D$ is nonempty, convex, $D\subseteq S_X$, and whenever $x_1,x_2\in B_X$ and a point of $D$ lies in $]x_1,x_2[$, then $x_1,x_2\in D$.
2. $D$ is compact.
3. The vector span of $D$ is finite-dimensional.
4. The vector spans of $D$ and $C$ have the same dimension: $\dim D=\dim C$.
5. $\{x\in B_X:F(x)\in -C\}=-D$.
6. $\{x\in B_X:F(x)\in\partial C\}=\partial D$, where $\partial$ is the relative boundary inside the affine hull.
7. $\{x\in B_X:F(x)\in\operatorname{ext}C\}=\operatorname{ext}D$, where $\operatorname{ext}$ is the set of extreme points of the set itself.
8. For every $t\in[0,1]$,

The conjunction 1–8 is, conjunct by conjunct and in the same order, the definition of "$F$ matches $C$" (M1–M8), written out with $D$ in place of $B_X\cap F^{-1}(C)$.

Flags.

• Lean conventions. Set.BijOn bundles maps-into, injective-on, and surjective-onto; all three parts are hypotheses. LipschitzOnWith 1 is stated with extended distances, which for normed spaces is exactly $\|F(x)-F(x')\|\le\|x-x'\|$ on $B_X$. Module.finrank is $0$ for an infinite-dimensional space; the card guards against this junk value on both sides, by the hypothesis that $\operatorname{span}_\Delta C$ is finite-dimensional and by conclusion 3, so conclusion 4 is a genuine equality of finite dimensions. IsSphereFace does not ask for closedness; for a finite-dimensional sphere face closedness is automatic (pick $c\in\operatorname{ri}C$; for $x\in\overline C$ the point $c$ lies in $]x,\,c+\varepsilon(c-x)[$, so extremality puts $x$ in $C$), hence $C$ is compact. intrinsicFrontier is the frontier inside the affine hull; since $C$ is closed, $\partial C\subseteq C$. C.extremePoints ℝ means the extreme points of $C$ as a set, which for a face of $B_Y$ coincide with $\operatorname{ext}B_Y\cap C$. $D$ is introduced as a variable together with the equation $D=B_X\cap F^{-1}(C)$; this is a definition, not an extra assumption. Scalars are real; $X$ and $Y$ are normed spaces, not assumed to be Banach spaces, so the card asserts more than a Banach-space version would.
• Degenerate cases. The zero space makes the card vacuous, as noted in the standing hypotheses. If $\dim C=0$ then $C=\{e\}$ for an extreme point $e\in S_Y$ of $B_Y$; then $\partial C=\varnothing$, and the card says that $x_0=F^{-1}(e)$ is an extreme point of $B_X$ lying on $S_X$, that $B_X\cap F^{-1}(\{-e\})=\{-x_0\}$, and that $F(tx_0)=te$ for $t\in[0,1]$. At $t=0$ conclusion 8 says $F(0)=0$; at $t=1$ it says $F(D)=C$, which already follows from bijectivity. Conclusion 1 includes nonemptiness of $D$, which follows from surjectivity because $C\ne\varnothing$.
• Hypotheses, one by one. Bijectivity cannot be dropped. Without surjectivity, $F(x)=x/2$ on $X=Y$ gives $D=\varnothing$, not a sphere face. Without injectivity, the left shift $L(x_1,x_2,\dots)=(x_2,x_3,\dots)$ on $\ell_\infty$ maps $B_{\ell_\infty}$ onto itself and is $1$-Lipschitz; for $C=\{(1,1,1,\dots)\}$ (an extreme point, so a $0$-dimensional sphere face) one gets $D=\{(s,1,1,\dots):|s|\le1\}$, of dimension $1\ne0$. The Lipschitz bound cannot be dropped: on $X=Y=\mathbb R$, the bijection of $[-1,1]$ that swaps $0$ and $1$ and fixes all other points gives $D=\{0\}\not\subseteq S_X$ for $C=\{1\}$. The sphere-face hypothesis on $C$ is the subject of the statement; for $F=\mathrm{id}$ and $C=\{0\}$ conclusion 1 fails. Finite dimensionality of $\operatorname{span}_\Delta C$ cannot be dropped: for $F=\mathrm{id}$ on $\ell_\infty$ and the sphere face $C=\{y\in B_{\ell_\infty}:y_1=1\}$, conclusions 2 and 3 fail. There is no inductive-step input in this card; it is the unconditional main statement. No hypothesis is unused, and I see no missing hypothesis needed for the statement to make sense.
• Name. matchesFace_of_finiteDimensional describes the statement: the conclusion is exactly "$F$ matches $C$" unfolded, and "finiteDimensional" refers to the face $C$, not to the spaces. The card spells out the eight conjuncts rather than citing MatchesFace; this is a presentation choice and the two agree literally.
• Truth. I believe it is true as written, but I have not verified the general case, which is a substantial theorem. Checks I could make: the $0$-dimensional case reduces to facts I recall from the plasticity literature for nonexpansive bijections between unit balls ($F(0)=0$, $F^{-1}(S_Y)\subseteq S_X$, the preimage of an extreme point is extreme, and $F(ax)=aF(x)$ for $|a|\le1$ when $F(x)$ is extreme). The inclusion $F(tD)\subseteq tC$ follows directly from $F(0)=0$, the Lipschitz bound, and extremality of $C$. The structure is consistent with the finite-dimensional polyhedral-face results I recall for nonexpansive bijections, and with the strictly convex target case, where every sphere face is a point. I found no counterexample.