# Group of Homography in Real Projective Plane

Formalized Mathematics (2017)

- Volume: 25, Issue: 1, page 55-62
- ISSN: 1426-2630

## Access Full Article

top## Abstract

top## How to cite

topRoland Coghetto. "Group of Homography in Real Projective Plane." Formalized Mathematics 25.1 (2017): 55-62. <http://eudml.org/doc/288134>.

@article{RolandCoghetto2017,

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].},

author = {Roland Coghetto},

journal = {Formalized Mathematics},

keywords = {projectivity; projective transformation; real projective plane; group of homography},

language = {eng},

number = {1},

pages = {55-62},

title = {Group of Homography in Real Projective Plane},

url = {http://eudml.org/doc/288134},

volume = {25},

year = {2017},

}

TY - JOUR

AU - Roland Coghetto

TI - Group of Homography in Real Projective Plane

JO - Formalized Mathematics

PY - 2017

VL - 25

IS - 1

SP - 55

EP - 62

AB - 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].

LA - eng

KW - projectivity; projective transformation; real projective plane; group of homography

UR - http://eudml.org/doc/288134

ER -

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.