{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T01:16:20Z","timestamp":1777425380066,"version":"3.51.4"},"reference-count":11,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2017,3,28]],"date-time":"2017-03-28T00:00:00Z","timestamp":1490659200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-sa\/3.0\/legalcode"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,3,28]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p> Using the Mizar system [2], we formalized that homographies of the projective real plane (as defined in [5]), form a group.<\/jats:p>\n               <jats:p>Then, we prove that, using the notations of Borsuk and Szmielew in [3]<\/jats:p>\n               <jats:p>\u201cConsider in space \u211d\u2119<jats:sup>2<\/jats:sup> points P<jats:sub>1<\/jats:sub>, P<jats:sub>2<\/jats:sub>, P<jats:sub>3<\/jats:sub>, P<jats:sub>4<\/jats:sub> of which three points are not collinear and points Q<jats:sub>1<\/jats:sub>,Q<jats:sub>2<\/jats:sub>,Q<jats:sub>3<\/jats:sub>,Q<jats:sub>4<\/jats:sub> each three points of which are also not collinear. There exists one homography h of space \u211d\u2119<jats:sup>2<\/jats:sup> such that h(P<jats:sub>i<\/jats:sub>) = Q<jats:sub>i<\/jats:sub> for i = 1, 2, 3, 4.\u201d<\/jats:p>\n               <jats:p>(Existence Statement 52 and Existence Statement 53) [3]. Or, using notations of Richter [11]<\/jats:p>\n               <jats:p>\u201cLet [a], [b], [c], [d] in \u211d\u2119<jats:sup>2<\/jats:sup> be four points of which no three are collinear and let [a\u2032],[b\u2032],[c\u2032],[d\u2032] in \u211d\u2119<jats:sup>2<\/jats:sup> be another four points of which no three are collinear, then there exists a 3 \u00d7 3 matrix M such that [Ma] = [a\u2032], [Mb] = [b\u2032], [Mc] = [c\u2032], and [Md] = [d\u2032]\u201d<\/jats:p>\n               <jats:p>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].<\/jats:p>","DOI":"10.1515\/forma-2017-0005","type":"journal-article","created":{"date-parts":[[2017,5,19]],"date-time":"2017-05-19T10:01:47Z","timestamp":1495188107000},"page":"55-62","source":"Crossref","is-referenced-by-count":2,"title":["Group of Homography in Real Projective Plane"],"prefix":"10.1515","volume":"25","author":[{"given":"Roland","family":"Coghetto","sequence":"first","affiliation":[{"name":"Rue de la Brasserie 5, 7100 , La Louvi\u00e8re , Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2017,5,11]]},"reference":[{"key":"2021040815464630763_j_forma-2017-0005_ref_001_w2aab2b8b6b1b7b1ab1ab1Aa","unstructured":"[1] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990."},{"key":"2021040815464630763_j_forma-2017-0005_ref_002_w2aab2b8b6b1b7b1ab1ab2Aa","doi-asserted-by":"crossref","unstructured":"[2] Grzegorz Bancerek, Czes\u0142aw Bylinski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261-279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi: 10.1007\/978-3-319-20615-8 17.","DOI":"10.1007\/978-3-319-20615-8"},{"key":"2021040815464630763_j_forma-2017-0005_ref_003_w2aab2b8b6b1b7b1ab1ab3Aa","unstructured":"[3] Karol Borsuk and Wanda Szmielew. Foundations of Geometry. North Holland, 1960."},{"key":"2021040815464630763_j_forma-2017-0005_ref_004_w2aab2b8b6b1b7b1ab1ab4Aa","unstructured":"[4] Czes\u0142aw Byli\u0144ski. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661-668, 1990."},{"key":"2021040815464630763_j_forma-2017-0005_ref_005_w2aab2b8b6b1b7b1ab1ab5Aa","doi-asserted-by":"crossref","unstructured":"[5] Roland Coghetto. Homography in RP2. Formalized Mathematics, 24(4):239-251, 2016. doi: 10.1515\/forma-2016-0020.","DOI":"10.1515\/forma-2016-0020"},{"key":"2021040815464630763_j_forma-2017-0005_ref_006_w2aab2b8b6b1b7b1ab1ab6Aa","unstructured":"[6] Agata Darmochwa\u0142. The Euclidean space. Formalized Mathematics, 2(4):599-603, 1991."},{"key":"2021040815464630763_j_forma-2017-0005_ref_007_w2aab2b8b6b1b7b1ab1ab7Aa","unstructured":"[7] Kanchun, Hiroshi Yamazaki, and Yatsuka Nakamura. Cross products and tripple vector products in 3-dimensional Euclidean space. Formalized Mathematics, 11(4):381-383, 2003."},{"key":"2021040815464630763_j_forma-2017-0005_ref_008_w2aab2b8b6b1b7b1ab1ab8Aa","unstructured":"[8] Wojciech Leo\u0144czuk and Krzysztof Prazmowski. A construction of analytical projective space. Formalized Mathematics, 1(4):761-766, 1990."},{"key":"2021040815464630763_j_forma-2017-0005_ref_009_w2aab2b8b6b1b7b1ab1ab9Aa","unstructured":"[9] Timothy James McKenzie Makarios. The independence of Tarski\u2019s Euclidean Axiom. Archive of Formal Proofs, October 2012."},{"key":"2021040815464630763_j_forma-2017-0005_ref_010_w2aab2b8b6b1b7b1ab1ac10Aa","unstructured":"[10] Timothy James McKenzie Makarios. A mechanical verification of the independence of Tarski\u2019s Euclidean Axiom. Victoria University of Wellington, New Zealand, 2012. Master\u2019s thesis."},{"key":"2021040815464630763_j_forma-2017-0005_ref_011_w2aab2b8b6b1b7b1ab1ac11Aa","doi-asserted-by":"crossref","unstructured":"[11] J\u00fcrgen Richter-Gebert. Perspectives on projective geometry: a guided tour through real and complex geometry. Springer Science & Business Media, 2011.","DOI":"10.1007\/978-3-642-17286-1"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/25\/1\/article-p55.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2017-0005","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,9]],"date-time":"2021-04-09T20:15:57Z","timestamp":1617999357000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2017-0005"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,28]]},"references-count":11,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2017,5,11]]},"published-print":{"date-parts":[[2017,3,28]]}},"alternative-id":["10.1515\/forma-2017-0005"],"URL":"https:\/\/doi.org\/10.1515\/forma-2017-0005","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,3,28]]}}}