Absolute retracts

DefinitionAbsolute retract#✓fully proved

A topological space \(K\) is an absolute retract when \(K\) is compact and, for every separable metrizable space \(X\) and every topological embedding \(e \colon K \to X\), there is a continuous map \(r \colon X \to K\) with \(r(e(k)) = k\) for all \(k \in K\).

def IsAbsoluteRetract (K : Type*) [TopologicalSpace K] : Prop :=
  IsCompact (Set.univ : Set K) ∧
    ∀ (X : Type*) [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X]
      [TopologicalSpace.SeparableSpace X] (e : K → X), Topology.IsEmbedding e →
      ∃ r : X → K, Continuous r ∧ Function.LeftInverse r e

Used by 1

Used byEilenberg's theorem on compact convex absolute retracts

DefinitionWilson convexity#✓fully proved

A subset \(K\) of a pseudometric space \(X\) with distance \(d\) is convex in the sense of Wilson when for all \(x, y \in K\) and every real \(t\) with \(0 \le t \le 1\) there is exactly one \(z \in K\) with \(d(x, z) = t \, d(x, y)\) and \(d(z, y) = (1 - t) \, d(x, y)\).

def IsWilsonConvex (X : Type*) [PseudoMetricSpace X] (K : Set X) : Prop :=
  ∀ x ∈ K, ∀ y ∈ K, ∀ t : ℝ, 0 ≤ t → t ≤ 1 →
    ∃! z, z ∈ K ∧ dist x z = t * dist x y ∧ dist z y = (1 - t) * dist x y

Used by 1

Used byEilenberg's theorem on compact convex absolute retracts

TheoremEilenberg's theorem on compact convex absolute retracts#●ready to prove

(a) Every nonempty compact convex subset of a complete metrizable locally convex topological vector space over \(\mathbb{R}\) is an absolute retract. (b) Every nonempty compact subset of a pseudometric space that is convex in the sense of Wilson is an absolute retract.

The spaces in part (a) are the real Fréchet spaces, the spaces of type (B0).

theorem_wanted eilenbergCompactConvexAbsoluteRetract :
    (∀ (E : Type*) [AddCommGroup E] [Module ℝ E] [UniformSpace E] [IsUniformAddGroup E]
      [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [CompleteSpace E]
      [TopologicalSpace.MetrizableSpace E]
      (K : Set E), Convex ℝ K → K.Nonempty → IsCompact K → IsAbsoluteRetract ↥K) ∧
    ∀ (X : Type*) [PseudoMetricSpace X] (K : Set X),
      IsCompact K → K.Nonempty → IsWilsonConvex X K → IsAbsoluteRetract ↥K

Sources

• S. Eilenberg, Problem 138 of the Scottish Book; the typescript heads the entry "Theorem; Eilenberg" and states both (a) and (b) as theorems. Part (a) is also the Dugundji theorem, see the 2026 survey "90+ years of the Scottish Book" (arXiv:2603.27867), which notes that every nonempty convex subset of a locally convex metrizable topological vector space is an absolute retract.

Uses 2

Statement usesAbsolute retract · Wilson convexity

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.