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.
@article{bwmeta1.element.doi-10_1515_forma-2016-0020,
author = {Roland Coghetto},
title = {Homography in RP},
journal = {Formalized Mathematics},
volume = {24},
year = {2016},
pages = {239-251},
zbl = {1357.51021},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0020}
}
Roland Coghetto. Homography in ℝℙ. Formalized Mathematics, Tome 24 (2016) pp. 239-251. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0020/