mathlib3
7bb2d89f - feat(dynamics/fixed_points/topology): new file (#2991)

Commit
5 years ago
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`.
Author
Parents
Loading