Faces of the unit ball contained in the sphere, and the conclusions of the face theorem

Definition

Plasticity_Faces

by scanstone · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

Let $E$ be a real normed space with closed unit ball $B$ and unit sphere $S$ . A sphere face (IsSphereFace C) is a nonempty convex set $C\subseteq S$ that is an extreme subset of $B$ : whenever a point of $C$ lies in the open segment between two points of $B$ , both points lie in $C$ . Its dimension is $\dim\operatorname{span}(C-C)$ , written Module.finrank ℝ (vectorSpan ℝ C); its relative boundary $\partial C$ and relative interior are taken in its affine hull (intrinsicFrontier, intrinsicInterior).

For a map $F$ from the unit ball of $X$ to that of $Y$ and a sphere face $C$ of $B_Y$ , MatchesFace F C states, for $D=B_X\cap F^{-1}(C)$ : $D$ is a compact sphere face of $B_X$ of the same finite dimension as $C$ ; $B_X\cap F^{-1}(-C)=-D$ ; $B_X\cap F^{-1}(\partial C)=\partial D$ ; $B_X\cap F^{-1}(\operatorname{ext}C)=\operatorname{ext}D$ ; and $F(tD)=tC$ for $0\le t\le1$ . It bundles the conclusions of the face theorem (card Plasticity.Faces.matchesFace_of_finiteDimensional) for use in lemma cards.

Definition code

import Mathlib.Analysis.Normed.Module.Basic
import Mathlib.Analysis.Convex.Extreme
import Mathlib.Analysis.Convex.Intrinsic
import Mathlib.LinearAlgebra.FiniteDimensional.Defs

/-!
# Plasticity: faces of the unit ball

A *sphere face* of the closed unit ball `B` of a real normed space is a nonempty convex subset
`C` of the unit sphere that is an extreme subset of `B`: if a point of `C` lies in the open
segment between two points of `B`, both points lie in `C`.
Its dimension is that of its affine span, `Module.finrank ℝ (vectorSpan ℝ C)`, and its relative
boundary and relative interior are Mathlib's `intrinsicFrontier ℝ C` and `intrinsicInterior ℝ C`.

`MatchesFace F C` collects, for a map `F` between unit balls and a face `C` of the target ball,
the conclusions of the face theorem about `D = B_X ∩ F⁻¹(C)`; it is used by the lemma cards of
the face theorem.
-/

namespace Plasticity

open scoped Pointwise

/-- `C` is a face of the closed unit ball of `E` contained in the unit sphere. -/
def IsSphereFace {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (C : Set E) : Prop :=
  C.Nonempty ∧ Convex ℝ C ∧ C ⊆ Metric.sphere (0 : E) 1 ∧
    IsExtreme ℝ (Metric.closedBall (0 : E) 1) C

/-- The conclusions of the face theorem for a face `C` of the unit ball of `Y` and the set
`D = B_X ∩ F⁻¹(C)`: `D` is a compact sphere face of the same finite dimension,
`B_X ∩ F⁻¹(-C) = -D`, `F` matches relative boundaries and extreme points, and `F` maps `t • D`
onto `t • C` for `0 ≤ t ≤ 1`. -/
def MatchesFace {X Y : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    [NormedAddCommGroup Y] [NormedSpace ℝ Y] (F : X → Y) (C : Set Y) : Prop :=
  IsSphereFace (Metric.closedBall (0 : X) 1 ∩ F ⁻¹' C) ∧
    IsCompact (Metric.closedBall (0 : X) 1 ∩ F ⁻¹' C) ∧
    FiniteDimensional ℝ (vectorSpan ℝ (Metric.closedBall (0 : X) 1 ∩ F ⁻¹' C)) ∧
    Module.finrank ℝ (vectorSpan ℝ (Metric.closedBall (0 : X) 1 ∩ F ⁻¹' C)) =
      Module.finrank ℝ (vectorSpan ℝ C) ∧
    Metric.closedBall (0 : X) 1 ∩ F ⁻¹' (-C) = -(Metric.closedBall (0 : X) 1 ∩ F ⁻¹' C) ∧
    Metric.closedBall (0 : X) 1 ∩ F ⁻¹' (intrinsicFrontier ℝ C) =
      intrinsicFrontier ℝ (Metric.closedBall (0 : X) 1 ∩ F ⁻¹' C) ∧
    Metric.closedBall (0 : X) 1 ∩ F ⁻¹' (C.extremePoints ℝ) =
      (Metric.closedBall (0 : X) 1 ∩ F ⁻¹' C).extremePoints ℝ ∧
    ∀ t ∈ Set.Icc (0 : ℝ) 1, F '' (t • (Metric.closedBall (0 : X) 1 ∩ F ⁻¹' C)) = t • C

end Plasticity

Source

This repository: expositions/faces/codirected_compactness.md §1 (faces, extreme subsets), expositions/faces/finite_faces_boundary_crossing.md §1 (Theorem 1); Mathlib's IsExtreme, Set.extremePoints, intrinsicFrontier and vectorSpan

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back. The file makes two definitions.

Sphere face. For a real normed space $E$ and a set $C \subseteq E$ , " $C$ is a sphere face" means all of:

$C \neq \emptyset$ ;
$C$ is convex;
$C \subseteq S_E$ ;
$C$ is an extreme subset of $B_E$ : $C \subseteq B_E$ , and for all $y_1, y_2 \in B_E$ and $c \in C$ , if $c$ lies in the open segment between $y_1$ and $y_2$ , then $y_1 \in C$ and $y_2 \in C$ .

No closedness and no finite-dimensionality is required. In the zero space $S_E = \emptyset$ , so no set is a sphere face there.

Face matching. For real normed spaces $X, Y$ (completeness not assumed), any function $F : X \to Y$ (no Lipschitz, injectivity or surjectivity condition) and any set $C \subseteq Y$ , put

D := B_X \cap F^{-1}(C).

" $F$ matches the face $C$ " means all eight of:

$D$ is a sphere face of $B_X$ (nonempty, convex, $D \subseteq S_X$ , extreme subset of $B_X$ );
$D$ is compact;
the linear span of $D - D$ is finite-dimensional;
$d(D) = d(C)$ (no finite-dimensionality of $C$ is required, so if the span of $C - C$ is infinite-dimensional the right side is $0$ );
$B_X \cap F^{-1}(-C) = -D$ ;
$B_X \cap F^{-1}(\operatorname{relbd} C) = \operatorname{relbd} D$ ;
$B_X \cap F^{-1}(\operatorname{ext} C) = \operatorname{ext} D$ ;
for every $t \in [0,1]$ , $F(tD) = tC$ (image of the set $tD$ ).

Since $D \subseteq B_X$ and $t \in [0,1]$ , only the values of $F$ on $B_X$ enter.

Flags.

Lean conventions. In item 4, for a $C$ whose span of $C - C$ is infinite-dimensional, $d(C) = 0$ , so the predicate would force $D$ to be a single point: a junk reading. In item 6, $\operatorname{relbd} C$ of a non-closed $C$ contains points outside $C$ . Both are harmless in every use in these cards, because the predicate is only applied to faces $C$ (or $C' \subseteq C$ ) with finite-dimensional span, and such sphere faces are compact (card isCompact_and_eq_closedBall_inter_affineSpan); $D$ is compact by item 2. Item 8 at $t = 0$ says $F(0) = 0$ whenever $D \ne \emptyset$ (which item 1 guarantees).
Names. IsSphereFace is accurate: a nonempty convex extreme subset of the ball lying in the sphere, i.e. a proper nonempty face. MatchesFace is generic: it does not say that the object is the preimage $B_X \cap F^{-1}(C)$ ; a name such as PreimageMatchesFace would describe it better (minor).
Docstrings. The docstrings agree with the code.
Truth. Definitions; nothing to prove. Convexity (item 2 of the sphere face) is a genuine extra condition, since extreme subsets need not be convex.

View graph