Homography in ℝℙ

• Autorzy: Roland Coghetto
• Języki publikacji: EN

Abstrakty

EN

The real projective plane has been formalized in Isabelle/HOL by Timothy Makarios [13] and in Coq by Nicolas Magaud, Julien Narboux and Pascal Schreck [12]. Some definitions on the real projective spaces were introduced early in the Mizar Mathematical Library by Wojciech Leonczuk [9], Krzysztof Prazmowski [10] and by Wojciech Skaba [18]. In this article, we check with the Mizar system [4], some properties on the determinants and the Grassmann-Plücker relation in rank 3 [2], [1], [7], [16], [17]. Then we show that the projective space induced (in the sense defined in [9]) by ℝ3 is a projective plane (in the sense defined in [10]). Finally, in the real projective plane, we define the homography induced by a 3-by-3 invertible matrix and we show that the images of 3 collinear points are themselves collinear.

Słowa kluczowe

EN

projectivity; projective transformation; projective collineation; real projective plane; Grassmann-Plücker relation

Kategorie tematyczne

• 03B35: Mechanization of proofs and logical operations
• 51N15: Projective analytic geometry

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2016
• Tom: 24
• Numer: 4
• Strony: 239-251

Daty

wydano

2016-12-01

otrzymano

2016-10-18

online

2017-02-23

Twórcy

autor

Roland Coghetto

• Rue de la Brasserie 5, 7100 La Louvière,

Identyfikatory

DOI

10.1515/forma-2016-0020