Email Gateway (Aug 22 2022 at 21:16): Email Gateway (Aug 22 2022 at 21:16):From: Manuel Eberl <eberlm@in.tum.de>
We have another two new entries, and rather sizeable ones at that:
14,000 lines in the first one and another 10,000 in the second one:
Complex Geometry
https://www.isa-afp.org/entries/Complex_Geometry.html
by Filip Marić and Danijela Simić
A formalization of geometry of complex numbers is presented. Fundamental
objects that are investigated are the complex plane extended by a single
infinite point, its objects (points, lines and circles), and groups of
transformations that act on them (e.g., inversions and Möbius
transformations). Most objects are defined algebraically, but
correspondence with classical geometric definitions is shown.
Poincaré Disc Model
https://www.isa-afp.org/entries/Poincare_Disc.html
by Danijela Simić, Filip Marić, and Pierre Boutry
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).
Enjoy,
Manuel
Last updated: Apr 24 2024 at 04:17 UTC