Poincaré Disc Model (Q7361445)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Poincare_Disc
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Poincaré Disc Model |
AFP entry Poincare_Disc |
Statements
16 December 2019
0 references
Danijela Simić
0 references
Filip Marić
0 references
Pierre Boutry
0 references
Poincaré Disc Model (English)
0 references
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).
0 references
