The nonwandering set $\Omega(f)$ is closed

Proved

PughClosingLemma.isClosed_nonwanderingSet

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

dynamical-systems

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

Together with $\mathrm{Per}(f)\subseteq\Omega(f)$ this gives $\overline{\mathrm{Per}(f)}\subseteq\Omega(f)$ , the easy half of the equality asserted for generic diffeomorphisms by the General Density Theorem.

Preamble

import Mathlib
import Definitions.Def_PughClosingLemma_nonwandering

open scoped Topology

Formal statement

namespace PughClosingLemma

theorem isClosed_nonwanderingSet {X : Type*} [TopologicalSpace X] (f : X → X) :
    IsClosed (nonwanderingSet f) := 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$ and every function $f\colon X\to X$ (no continuity assumed), the set $\Omega(f)$ is a closed subset of $X$ . Here $\Omega(f)$ is the set of $x\in X$ such that for every neighbourhood $U$ of $x$ there is $n\ge 1$ with $f^n(U)\cap U\neq\emptyset$ .

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

The nonwandering set Ω(f)\Omega(f)Ω(f) is closed

The nonwandering set $\Omega(f)$ is closed