Revision #2532 → #3173 · back to history
modifiedLyapunov timedcc410097db0
| Field | From #2532 | To #3173 |
|---|
| note | Grep for 'Lyapunov' returned no dynamical-systems results in Mathlib. | Grep across Mathlib for 'Lyapunov' returned no dynamical-systems results. |
modifiedTopological transitivity14cb800b5cd1
| Field | From #2532 | To #3173 |
|---|
| note | Mathlib defines topological transitivity for monoid actions, generalizing the single-map open-set-overlap condition. | Mathlib defines topological transitivity as a class on monoid actions, generalizing the single-map open-set-overlap condition. |
addedSharkovskii's theorem63713f16a780
modifiedPoincaré–Bendixson theorem66bf4745e76a
| Field | From #2532 | To #3173 |
|---|
| note | The Poincaré–Bendixson theorem is not formalized in Mathlib (only an unrelated Poincaré conjecture file exists). | The Poincaré–Bendixson theorem is not formalized in Mathlib. |
addedCantor setc05d70de0e42
modifiedKoch curve / snowflakee927049a0a7b
| Field | From #2532 | To #3173 |
|---|
| mathlib.decl | Metric.Snowflaking | — |
| mathlib.module | Mathlib.Topology.MetricSpace.Snowflaking | — |
| note | Mathlib's Snowflaking construction is motivated by the von Koch snowflake in its docstring, but the Koch curve and its fractal dimension are not actually constructed or computed. | The Koch curve/snowflake and its fractal dimension are not constructed in Mathlib. |
| provenance | ai | ai-moderated |
| status | partial | not_formalized |