Prove2Me

Periodic points are nonwandering: Per(f)⊆Ω(f)\mathrm{Per}(f)\subseteq\Omega(f)

Proved
PughClosingLemma.periodicPts_subset_nonwanderingSet

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

dynamical-systems

Let XX be a topological space and f ⁣:X→Xf\colon X\to X any map. Every periodic point of ff is nonwandering:

Per(f)={x:∃n≥1, fn(x)=x} ⊆ Ω(f).\mathrm{Per}(f)=\{x : \exists n\ge 1,\ f^n(x)=x\}\ \subseteq\ \Omega(f).

This is the elementary converse direction to the closing lemma: periodic points are always nonwandering, and the closing lemma says nonwandering points become periodic after a C1C^1-small perturbation.

Preamble
import Mathlib
import Definitions.Def_PughClosingLemma_nonwandering

open scoped Topology
Formal statement
namespace PughClosingLemma

theorem periodicPts_subset_nonwanderingSet {X : Type*} [TopologicalSpace X] (f : X → X) :
    Function.periodicPts 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 XX and every function f ⁣:X→Xf\colon X\to X (no continuity assumed): every point xx for which there exists n≥1n\ge 1 with fn(x)=xf^n(x)=x belongs to Ω(f)\Omega(f). Here Ω(f)\Omega(f) is the set of x∈Xx\in X such that for every neighbourhood UU of xx there is a natural number n≥1n\ge 1 with fn(U)∩U≠∅f^n(U)\cap U\neq\emptyset, fnf^n being the nn-fold composite. The period 00 is excluded from the hypothesis (a point with f0(x)=xf^0(x)=x only is not assumed periodic).

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