### Abstract

The Poincaré-Bendixson theorem is a classical result in the study of (continuous) dynamical systems. Colloquially, it restricts the possible behaviors of planar dynamical systems: such systems cannot be chaotic. In practice, it is a useful tool for proving the existence of (limiting) periodic behavior in planar systems. The theorem is an interesting and challenging benchmark for formalized mathematics because proofs in the literature rely on geometric sketches and only hint at symmetric cases. It also requires a substantial background of mathematical theories, e.g., the Jordan curve theorem, real analysis, ordinary differential equations, and limiting (long-term) behavior of dynamical systems.

### License

BSD License

### Topics

- Mathematics/Analysis

### Session Poincare_Bendixson

- Analysis_Misc
- ODE_Misc
- Invariance
- Limit_Set
- Periodic_Orbit
- Poincare_Bendixson
- Affine_Arithmetic_Misc
- Examples

### Depends on

- Ordinary Differential Equations

### Used by

- Pick’s Theorem

### Auto-related entries

- Matrices for ODEs

## Cite

×

Poincare_Bendixson-AFP

    @article{Poincare_Bendixson-AFP,
      author  = {Fabian Immler and Yong Kiam Tan},
      title   = {The Poincaré-Bendixson Theorem},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Poincare_Bendixson.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Dec 18, 2019 : Isabelle2019