Mañé's theorem: $C^1$ structural stability implies Axiom A

Open

StabilityConjecture.mane_C1_stability

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-topologydynamical-systems

Let $M$ be a closed manifold: a compact Hausdorff smooth manifold without boundary, modelled on $\mathbb R^n$ . Let $f\in\mathrm{Diff}^1(M)$ be $C^1$ structurally stable. Then $f$ satisfies Axiom A: the nonwandering set $\Omega(f)$ is a hyperbolic set of $f$ and

\overline{\mathrm{Per}(f)}=\Omega(f).

This is the case $r=1$ of the $C^r$ stability conjecture, recorded as proved on the Open Problem Garden page.

Preamble

import Mathlib
import Definitions.Def_ClosingLemma_DiffeoCrTopology
import Definitions.Def_PughClosingLemma_nonwandering
import Definitions.Def_StabilityConjecture_Basic

open scoped Manifold ContDiff Topology

Formal statement

namespace StabilityConjecture

open ClosingLemma

theorem mane_C1_stability {n : ℕ} {M : Type*} [TopologicalSpace M] [T2Space M]
    [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsManifold (𝓡 n) ∞ M]
    (f : Diff n M 1) (hf : IsStructurallyStable 1 f) :
    SatisfiesAxiomA f := by sorry

end StabilityConjecture

Source

R. Mañé, A proof of the C^1 stability conjecture, Publ. Math. IHÉS 66 (1988). Recorded as the proved case r = 1 in Open Problem Garden, "C^r Stability Conjecture" (Conjecture, author(s) J. Palis and S. Smale; posted by m n, December 20th, 2007), https://www.openproblemgarden.org/op/c_r_stability_conjecture

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Mañé's theorem: C1C^1C1 structural stability implies Axiom A

Mañé's theorem: $C^1$ structural stability implies Axiom A