Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-08 20:32 7bb2d89f

View on Github →

feat(dynamics/fixed_points/topology): new file (#2991)

  • Move is_fixed_pt_of_tendsto_iterate from topology.metric_space.contracting, reformulate it without ∃.
  • Add is_closed_fixed_points.
  • Move dynamics.fixed_points to dynamics.fixed_points.basic.

Estimated changes

added theorem is_closed_fixed_points
added theorem continuous_at.tendsto