Cross-Ratio in Real Vector Space

Using Mizar [1], in the context of a real vector space, we introduce the concept of affine ratio of three aligned points (see [5]).It is also equivalent to the notion of “Mesure algèbrique”1, to the opposite of the notion of Teilverhältnis2 or to the opposite of the ordered length-ratio [9].In the second part, we introduce the classic notion of “cross-ratio” of 4 points aligned in a real vector space.Finally, we show that if the real vector space is the real line, the notion corresponds to the classical notion3 [9]:The cross-ratio of a quadruple of distinct points on the real line with coordinates x1, x2, x3, x4 is given by:(x1,x2;x3,x4)=x3-x1x3-x2.x4-x2x4-x1In the Mizar Mathematical Library, the vector spaces were first defined by Kusak, Leonczuk and Muzalewski in the article [6], while the actual real vector space was defined by Trybulec [10] and the complex vector space was defined by Endou [4]. Nakasho and Shidama have developed a solution to explore the notions introduced by different authors4 [7]. The definitions can be directly linked in the HTMLized version of the Mizar library5.The study of the cross-ratio will continue within the framework of the Klein- Beltrami model [2], [3]. For a generalized cross-ratio, see Papadopoulos [8].Rue de la Brasserie 5, 7100 La Louvière, BelgiumGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, 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.Roland Coghetto. Klein-Beltrami model. Part I. Formalized Mathematics, 26(1):21–32, 2018. doi:10.2478/forma-2018-0003.Roland Coghetto. Klein-Beltrami model. Part II. Formalized Mathematics, 26(1):33–48, 2018. doi:10.2478/forma-2018-0004.Noboru Endou. Complex linear space and complex normed space. Formalized Mathematics, 12(2):93–102, 2004.Jadwiga Knop. About a certain generalization of the affine ratio of three points and unharmonic ratio of four points. Bulletin of the Section of Logic, 32(1–2):33–42, 2003.Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.Kazuhisa Nakasho and Yasunari Shidama. Documentation generator focusing on symbols for the HTML-ized Mizar library. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, CICM 2015, volume 9150 of Lecture Notes in Computer Science, pages 343–347. Springer, Cham, 2015. doi:10.1007/978-3-319-20615-8_25.Athanase Papadopoulos and Sumio Yamada. On the projective geometry of constant curvature spaces. Sophus Lie and Felix Klein: The Erlangen Program and Its Impact in Mathematics and Physics, 23:237–245, 2015.Jürgen Richter-Gebert. Perspectives on projective geometry: a guided tour through real and complex geometry. Springer Science & Business Media, 2011.Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291–296, 1990.271476