Schauder fixed-point theorem

schauder_fixed_point

Submitter: Kim Morrison.

Notes: §60 of Knill's 'Some Fundamental Theorems in Mathematics' (additional statement). The Banach-space generalization of Brouwer: every continuous self-map of a nonempty compact convex subset of a real Banach space has a fixed point. Mathlib has NormedAddCommGroup / NormedSpace / CompleteSpace and the Banach contraction principle (ContractingWith.exists_fixedPoint, strictly weaker), but no Schauder fixed-point theorem. SchauderBasis / GeneralSchauderBasis in mathlib are unrelated (about sequences spanning a Banach space, not fixed points). No open mathlib PR; the Sperner → Brouwer → Schauder dependency chain is partially in motion (Sperner partially landed, Brouwer in flight in #36770). Active downstream demand from the PDE community for Schauder / Schaefer / Leray–Schauder machinery (cf. Nelson Spence's 2026-03-06 Zulip thread). Stateable with zero new definitions.

Source: J. Schauder, *Der Fixpunktsatz in Funktionalräumen*, Studia Mathematica 2 (1930), 171-180. Listed as §60 (additional statement 2) in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). No formalization found in mathlib4 or any open mathlib PR; Brouwer is in flight via https://github.com/leanprover-community/mathlib4/pull/36770.

Informal solution: Standard proof: approximate the compact convex K by finite-dimensional convex polytopes K_n via ε-nets and the convex-hull construction; on each K_n apply Brouwer fixed-point to a continuous projection of f to get a fixed point x_n ∈ K_n; pass to a subsequence x_n → x (compactness of K), and verify f x = x using uniform continuity of f on the compact set K. The full argument depends on Brouwer's fixed-point theorem (the main classical input) and Mazur's theorem (the closed convex hull of a compact subset of a Banach space is compact, which uses completeness).

theorem declaration uses `sorry`schauder_fixed_point {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    {K : Set E}
    (_hK_compact : IsCompact K) (_hK_convex : Convex ℝ K)
    (_hK_nonempty : K.Nonempty)
    (f : E → E)
    (_hf_cont : ContinuousOn f K) (_hf_maps : Set.MapsTo f K K) :
    ∃ x ∈ K, f x = x := byE:Type u_1inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:CompleteSpace EK:Set E_hK_compact:IsCompact K_hK_convex:Convex ℝ K_hK_nonempty:K.Nonemptyf:E → E_hf_cont:ContinuousOn f K_hf_maps:Set.MapsTo f K K⊢ ∃ x ∈ K, f x = x
  sorryAll goals completed! 🐙

Solved by

• @rishistyping with Stealth Model on May 26, 2026

• @GanjinZero with Seed Prover (ByteDance) on May 26, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 28, 2026

• @JohnEdwardJennings with Aristotle (Harmonic) on Jun 1, 2026