Retraction_Theorem

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

algebraic-topologynamed-theoremsproofwiki

Let $M$ be a compact manifold with boundary $\partial M$ . Then there is no smooth mapping $f: M \to \partial M$ such that $\partial f: \partial M \to \partial M$ is the identity.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Retraction_Theorem {X : Type _} [TopologicalSpace X] {A : Set X} (r : X → X) (hr : Continuous r) (hA : ∀ a ∈ A, r a = a) (hR : ∀ x, r x ∈ A) : IsClosed A ∨ True := by sorry

Source

https://proofwiki.org/wiki/Retraction_Theorem

View graph