### Abstract

We describe formalization of the Poincaré disc model of hyperbolic geometry within the Isabelle/HOL proof assistant. The model is defined within the extended complex plane (one dimensional complex projectives space ℂP1), formalized in the AFP entry “Complex Geometry”. Points, lines, congruence of pairs of points, betweenness of triples of points, circles, and isometries are defined within the model. It is shown that the model satisfies all Tarski's axioms except the Euclid's axiom. It is shown that it satisfies its negation and the limiting parallels axiom (which proves it to be a model of hyperbolic geometry).

### License

BSD License

### Topics

- Mathematics/Geometry

### Session Poincare_Disc

- Hyperbolic_Functions
- Tarski
- Poincare_Lines
- Poincare_Lines_Ideal_Points
- Poincare_Distance
- Poincare_Circles
- Poincare_Between
- Poincare_Lines_Axis_Intersections
- Poincare_Perpendicular
- Poincare
- Poincare_Tarski

### Depends on

- Complex Geometry

## Cite

×

Poincare_Disc-AFP

    @article{Poincare_Disc-AFP,
      author  = {Danijela Simić and Filip Marić and Pierre Boutry},
      title   = {Poincaré Disc Model},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Poincare_Disc.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
- Jan 17, 2020 : Isabelle2019