Group of Homography in Real Projective Plane

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

Abstrakty

EN

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

Słowa kluczowe

EN

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

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2017
• Tom: 25
• Numer: 1
• Strony: 55-62

Daty

wydano

2017-03-28

otrzymano

2017-03-17

online

2017-05-11

Twórcy

autor

Roland Coghetto

• , ,

Identyfikatory

DOI

10.1515/forma-2017-0005