0. The Precise Statement Proved🔗

Some conventions, making the terms of the statement precise.

The Lean definitions in this chapter are the trusted part of the benchmark statement (the file ChallengeDeps.lean): they pin down what the theorems assert. We show them alongside the informal conventions they encode. First, the ambient setup — everything lives over a compact space X, a target T, and index type \iota:

open Set unitInterval Geometry
open scoped Topology

namespace FamiliesOfMapsB01

variable {k : ℕ} {ι X T : Type*}
  [TopologicalSpace X] [TopologicalSpace T]

A family f : P' \times X \to T (for any parameter space P') is supported on S \subseteq X if f(p,x) = f(p',x) for all p, p' whenever x \notin S. It is adapted to \mathcal U (with constant k) if it is supported on the union of at most k of the U_\alpha.

/-- `Supported f S`: outside `S ⊆ X`, the family `f : P × X → T` is
parameter-independent. -/
def Supported {P : Type*} (f : P × X → T) (S : Set X) : Prop :=
  ∀ p p' : P, ∀ x ∉ S, f (p, x) = f (p', x)

/-- `AdaptedTo U k f`: `f` is supported on the union of at most `k` of the
sets `U α`. -/
def AdaptedTo {P : Type*} (U : ι → Set X) (k : ℕ) (f : P × X → T) : Prop :=
  ∃ A : Finset ι, A.card ≤ k ∧ Supported f (⋃ α ∈ A, U α)

A (polyhedral) subdivision of P is a finite geometric simplicial complex K in \mathbb R^k whose underlying space (the union of the closed simplices) is exactly P. A geometric simplicial complex is a collection of nonempty finite affinely independent vertex sets ("faces"), closed under passing to nonempty subsets, such that for any two faces \sigma, \tau one has \operatorname{conv}(\sigma) \cap \operatorname{conv}(\tau) \subseteq \operatorname{conv}(\sigma \cap \tau) (simplices meet along common faces). A facet is a face maximal under inclusion; its closed cell is its convex hull.

/-- A *convex linear polyhedron* in `ℝᵏ`: the convex hull of a finite set
(equivalently, a bounded intersection of finitely many half-spaces). -/
def IsPolyhedron (P : Set (Fin k → ℝ)) : Prop :=
  ∃ S : Finset (Fin k → ℝ), P = convexHull ℝ (S : Set _)

/-- A *polyhedral subdivision* of a polyhedron `P ⊆ ℝᵏ`: a finite geometric
simplicial complex whose underlying space equals `P`. -/
structure Subdivision (P : Set (Fin k → ℝ)) where
  complex      : SimplicialComplex ℝ (Fin k → ℝ)
  faces_finite : complex.faces.Finite
  space_eq     : complex.space = P

/-- The closed cell associated with a face `D`, as a subset of `P`. -/
def closedCell (P : Set (Fin k → ℝ)) (D : Finset (Fin k → ℝ)) : Set P :=
  { p | (p : Fin k → ℝ) ∈ convexHull ℝ (D : Set (Fin k → ℝ)) }

An extreme subset (or face) of P is a subset Q \subseteq P such that whenever a point of Q is written as ta + (1-t)b with a, b \in P and 0 < t < 1, both a and b lie in Q.

(In the Lean development this is Mathlib's IsExtreme ℝ P Q.)

A boundary subpolyhedron of P is a subset Q \subseteq P such that Q is the convex hull of a finite set, Q is contained in the intrinsic frontier of P (the frontier of P inside its affine span), and Q is an extreme subset of P. This is the precise reading of "convex linear subpolyhedron of \partial P". The extremality condition matters: without it, every singleton \{q\} with q a non-vertex boundary point would qualify; a family with one-point parameter space is supported on the empty set, so clause (4) below would force F(\cdot, q, \cdot) to be constant in the time direction at every boundary point q — and a homotopy frozen on all of \partial P cannot in general achieve the adaptation of clause (2), making the statement false under the weaker reading.

/-- A *boundary subpolyhedron* of `P`: a **face** of `P` (an `IsExtreme`
subset, the paper's "convex linear subpolyhedron of `∂P`") whose image in
`ℝᵏ` is a polyhedron and lies in the *intrinsic* frontier of `P`. The
face condition is what the construction keeps invariant (`u (I × Q × X) ⊆
Q`); without it single interior points of `∂P` would qualify and condition
4 would vacuously force the homotopy to freeze them in time. -/
def IsBoundarySubpolyhedron {P : Set (Fin k → ℝ)} (Q : Set P) : Prop :=
  (∃ S : Finset (Fin k → ℝ),
      ((↑) : P → Fin k → ℝ) '' Q = convexHull ℝ (S : Set (Fin k → ℝ))) ∧
    ((↑) : P → Fin k → ℝ) '' Q ⊆ intrinsicFrontier ℝ P ∧
    IsExtreme ℝ P (((↑) : P → Fin k → ℝ) '' Q)





end FamiliesOfMapsB01

Theorem A (continuous case)🔗

Theorem A (continuous case). For every continuous f : P \times X \to T there is a continuous F : [0,1] \times P \times X \to T such that:

F(0, \cdot, \cdot) = f;
there is a subdivision K of P such that for every facet D of K, the restriction of F(1,\cdot,\cdot) to \operatorname{conv}(D) \times X is adapted to \mathcal U with constant k;
if f is supported on S \subseteq X, then F, as a family parametrized by [0,1]\times P, is supported on S;
for every boundary subpolyhedron Q \subseteq P: if f|_{Q\times X} is supported on S' \subseteq X, then F|_{[0,1]\times Q\times X} is supported on S'.

Theorem B (bi-Lipschitz case)🔗

Theorem B (bi-Lipschitz case). Let in addition X, T be metric spaces (X compact), and give P \times X the metric d((p,x),(p',x')) = \max(d(p,p'), d(x,x')). Suppose each slice f(p,\cdot) : X \to T is a homeomorphism \mathrm{slice}(p), that f is (jointly) Lipschitz with constant L, and that all the inverses \mathrm{slice}(p)^{-1} are Lipschitz with the same constant L. Then there are F as in Theorem A, a constant L', and homeomorphisms \mathrm{Slice}(t,p) : X \to T, such that:

F(0,\cdot,\cdot) = f;
F(t,p,x) = \mathrm{Slice}(t,p)(x) for all t, p, x;
adaptation at time 1 on the facets of a subdivision, as in Theorem A(2);
global support preservation, as in Theorem A(3);
boundary support preservation, as in Theorem A(4);
every \mathrm{Slice}(t,p) is L'-Lipschitz;
every \mathrm{Slice}(t,p)^{-1} is L'-Lipschitz.

The formal statements of Theorems A and B — with the homotopy bundled as a continuous map, the clauses as the conjunctions displayed above, and (for Theorem B) the slices bundled as homeomorphisms — appear as the final theorems in the main theorems chapter, where they are proved by assembling everything that follows.