
Poincaré
Disc
Model
Title: 
Poincaré Disc Model 
Authors:

Danijela Simić,
Filip Marić (filip /at/ matf /dot/ bg /dot/ ac /dot/ rs) and
Pierre Boutry (boutry /at/ unistra /dot/ fr)

Submission date: 
20191216 
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). 
BibTeX: 
@article{Poincare_DiscAFP,
author = {Danijela Simić and Filip Marić and Pierre Boutry},
title = {Poincaré Disc Model},
journal = {Archive of Formal Proofs},
month = dec,
year = 2019,
note = {\url{http://isaafp.org/entries/Poincare_Disc.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Complex_Geometry 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

