Formalization of the Poincaré Disc Model of Hyperbolic Geometry
Abstract
We 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.
Origin : Files produced by the author(s)