Formalization of the Poincaré Disc Model of Hyperbolic Geometry

Simić, Danijela
Marić, Filip
Boutry, Pierre

Open link

Publication date

April 2020

DOI

10.1007/s10817-020-09551-2

Publisher

Springer Verlag

Abstract

International audienceWe describe formalization of the Poincaré disc model of hyperbolic geometry within the Isabelle/HOL proof assistant. The model is defined within the complex projective line ℂP1 and is shown to satisfy Tarski's axioms except for Euclid's axiom — it is shown to satisfy it's negation, and, moreover, to satisfy the existence of limiting parallels axiom

Extracted data

We use cookies to provide a better user experience.

Data Protection

Formalization of the Poincaré Disc Model of Hyperbolic Geometry

Abstract

Extracted data

Formalization of the Poincaré Disc Model of Hyperbolic Geometry

Abstract

Extracted data

Related items

Related items