The nonwandering set of a homeomorphism is invariant: $f(\Omega(f))=\Omega(f)$

Proved

PughClosingLemma.image_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$ a homeomorphism. Then the nonwandering set is invariant under $f$ :

f(\Omega(f))=\Omega(f).

Invariance makes $\Omega(f)$ a closed invariant set carrying the recurrent dynamics of $f$ , the set on which the closing lemma operates.

Preamble

import Mathlib
import Definitions.Def_PughClosingLemma_nonwandering

open scoped Topology

Formal statement

namespace PughClosingLemma

theorem image_nonwanderingSet {X : Type*} [TopologicalSpace X] (f : X ≃ₜ X) :
    f '' nonwanderingSet f = 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 homeomorphism $f\colon X\to X$ (a continuous bijection with continuous inverse), the image under $f$ of $\Omega(f)$ equals $\Omega(f)$ , where $\Omega(f)$ is the nonwandering set of the underlying map of $f$ : the set of $x$ such that every neighbourhood $U$ of $x$ admits $n\ge 1$ with $f^n(U)\cap U\neq\emptyset$ . Both inclusions are asserted (equality of sets).

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 of a homeomorphism is invariant: f(Ω(f))=Ω(f)f(\Omega(f))=\Omega(f)f(Ω(f))=Ω(f)

The nonwandering set of a homeomorphism is invariant: $f(\Omega(f))=\Omega(f)$