Closed mseri closed 1 month ago
The file contains nonwandering sets, recurrent sets and minimal sets. They should be split into meaningful functional bits. E.g.
topological/{nonWandering.lean, recurrent.lean, minimalSet.lean}
and polished so that they can be contributed back to Mathlib.Dynamics: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Dynamics/
Mathlib.Dynamics
The file contains nonwandering sets, recurrent sets and minimal sets. They should be split into meaningful functional bits. E.g.
topological/{nonWandering.lean, recurrent.lean, minimalSet.lean}and polished so that they can be contributed back to
Mathlib.Dynamics: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Dynamics/