Klein-Beltrami model. II

DOI10.2478/forma-2018-0004zbMath1401.51002OpenAlexW4239806157WikidataQ129426153 ScholiaQ129426153MaRDI QIDQ1796768

Roland Coghetto

Publication date: 17 October 2018

Published in: Formalized Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2478/forma-2018-0004

zbMATH Keywords

foundations of geometryTarski's geometry axiomsKlein-Beltrami model

Mathematics Subject Classification ID

Hyperbolic and elliptic geometries (general) and generalizations (51M10) Mechanization of proofs and logical operations (03B35) General theory of linear incidence geometry and projective geometries (51A05)

Related Items (4)

Klein-Beltrami model. III ⋮ Klein-Beltrami model. IV ⋮ Cross-ratio in real vector space ⋮ Formalization of the Poincaré disc model of hyperbolic geometry

Uses Software

• Isabelle/HOL
• Mizar
• HOL Light

Cites Work

• Four decades of {\textsc{Mizar}}. Foreword
• Homography in \(\mathbb{R}\mathbb{P}^2\)
• Klein-Beltrami model. I
• Group of homography in real projective plane
• Pascal's theorem in real projective plane
• Mizar: State-of-the-art and Beyond
• Unnamed Item

This page was built for publication: Klein-Beltrami model. II