On a nonempty compact space $\Omega(f)\neq\emptyset$

Proved

PughClosingLemma.nonwanderingSet_nonempty

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamical-systems

Let $X$ be a nonempty compact topological space and $f\colon X\to X$ any map. Then the nonwandering set $\Omega(f)$ is nonempty.

This guarantees that the hypothesis of the closing lemma is never vacuous: every diffeomorphism of a nonempty compact manifold has nonwandering points.

Formalization Note The statement is usually quoted for continuous $f$ ; continuity is not needed, so the Lean statement omits it (it is a stronger, still true statement). No Hausdorff assumption is made.

Preamble

import Mathlib
import Definitions.Def_PughClosingLemma_nonwandering

open scoped Topology

Formal statement

namespace PughClosingLemma

theorem nonwanderingSet_nonempty {X : Type*} [TopologicalSpace X] [CompactSpace X]
    [Nonempty X] (f : X → X) : (nonwanderingSet f).Nonempty := by sorry

end PughClosingLemma

Source

Standard property of the nonwandering set (not stated separately in the source article); context: Wikipedia, "Pugh's closing lemma", section "Formal statement" (revision oldid=1304222873, https://en.wikipedia.org/w/index.php?title=Pugh%27s_closing_lemma&oldid=1304222873), citing C. C. Pugh, "An Improved Closing Lemma and a General Density Theorem", Amer. J. Math. 89 (4) (1967), 1010-1021, https://doi.org/10.2307/2373414

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - same agent that drafted the statements; NON-BLIND

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements of this proposal, with full knowledge of the source and of the intended meaning. It is not a blind audit and must not be mistaken for independent testimony; reviewers should check the Lean code against the source themselves or obtain a blind read-back from an independent auditor.

For every topological space $X$ that is compact and nonempty, and every function $f\colon X\to X$ (no continuity assumed), the set $\Omega(f)$ is nonempty, i.e. there exists $x\in X$ such that for every neighbourhood $U$ of $x$ there is $n\ge 1$ with $f^n(U)\cap U\neq\emptyset$ . No separation axiom is assumed.

Human review

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

View graph

On a nonempty compact space Ω(f)≠∅\Omega(f)\neq\emptysetΩ(f)=∅

On a nonempty compact space $\Omega(f)\neq\emptyset$