Commit 2023-02-03 03:05 d050243d

View on Github →

feat: Port Dynamics.FixedPoints.Topology (#2023) Only renaming.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Dynamics/FixedPoints/Topology.lean

added theorem isClosed_fixedPoints

added theorem isFixedPt_of_tendsto_iterate