<abstract xmlns="http://www.w3.org/1999/xhtml"> Using the Mizar system [2], we formalized that homographies of the projective real plane (as defined in [5]), form a group.Then, we prove that, using the notations of Borsuk and Szmielew in [3]“Consider in space ℝℙ2 points P1, P2, P3, P4 of which three points are not collinear and points Q1,Q2,Q3,Q4 each three points of which are also not collinear. There exists one homography h of space ℝℙ2 such that h(Pi) = Qi for i = 1, 2, 3, 4.”(Existence Statement 52 and Existence Statement 53) [3]. Or, using notations of Richter [11]“Let [a], [b], [c], [d] in ℝℙ2 be four points of which no three are collinear and let [a′],[b′],[c′],[d′] in ℝℙ2 be another four points of which no three are collinear, then there exists a 3 × 3 matrix M such that [Ma] = [a′], [Mb] = [b′], [Mc] = [c′], and [Md] = [d′]”Makarios has formalized the same results in Isabelle/Isar (the collineations form a group, lemma statement52-existence and lemma statement 53-existence) and published it in Archive of Formal Proofs [10], [9].</abstract>

Using the Mizar system [2], we formalized that homographies of the projective real plane (as defined in [5]), form a group.Then, we prove that, using the notations of Borsuk and Szmielew in [3]“Consider in space ℝℙ2 points P1, P2, P3, P4 of which three points are not collinear and points Q1,Q2,Q3,Q4 each three points of which are also not collinear. There exists one homography h of space ℝℙ2 such that h(Pi) = Qi for i = 1, 2, 3, 4.”(Existence Statement 52 and Existence Statement 53) [3]. Or, using notations of Richter [11]“Let [a], [b], [c], [d] in ℝℙ2 be four points of which no three are collinear and let [a′],[b′],[c′],[d′] in ℝℙ2 be another four points of which no three are collinear, then there exists a 3 × 3 matrix M such that [Ma] = [a′], [Mb] = [b′], [Mc] = [c′], and [Md] = [d′]”Makarios has formalized the same results in Isabelle/Isar (the collineations form a group, lemma statement52-existence and lemma statement 53-existence) and published it in Archive of Formal Proofs [10], [9].

Group of Homography in Real Projective Plane

Formalized Mathematics

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License.

{"article-title":"Group of Homography in Real Projective Plane"}

Using the Mizar system [2], we formalized that homographies of the projective real plane (as defined in [5]), form a group.Then, we prove that, using the...

Group of Homography in Real Projective Plane

Published Online: May 11, 2017

Page range: 55 - 62

Received: Mar 17, 2017

DOI: https://doi.org/10.1515/forma-2017-0005

Keywords
projectivity, projective transformation, real projective plane, group of homography

© by Roland Coghetto

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License.

Group of Homography in Real Projective Plane

Published Online: May 11, 2017

Page range: 55 - 62

Received: Mar 17, 2017

DOI: https://doi.org/10.1515/forma-2017-0005

Keywordsprojectivity, projective transformation, real projective plane, group of homography

© by Roland Coghetto

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License.

Keywords
projectivity, projective transformation, real projective plane, group of homography