{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T00:08:41Z","timestamp":1783901321180,"version":"3.55.0"},"reference-count":10,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2019,4,1]],"date-time":"2019-04-01T00:00:00Z","timestamp":1554076800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,4,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>Using Mizar [1], in the context of a real vector space, we introduce the concept of affine ratio of three aligned points (see [5]).<\/jats:p>\n                  <jats:p>\n                    It is also equivalent to the notion of \u201cMesure alg\u00e8brique\u201d\n                    <jats:sup>1<\/jats:sup>\n                    , to the opposite of the notion of Teilverh\u00e4ltnis\n                    <jats:sup>2<\/jats:sup>\n                    or to the opposite of the ordered length-ratio [9].\n                  <\/jats:p>\n                  <jats:p>In the second part, we introduce the classic notion of \u201ccross-ratio\u201d of 4 points aligned in a real vector space.<\/jats:p>\n                  <jats:p>\n                    Finally, we show that if the real vector space is the real line, the notion corresponds to the classical notion\n                    <jats:sup>3<\/jats:sup>\n                    [9]:\n                  <\/jats:p>\n                  <jats:p>\n                    The cross-ratio of a quadruple of distinct points on the real line with coordinates\n                    <jats:italic>x<\/jats:italic>\n                    <jats:sub>1<\/jats:sub>\n                    ,\n                    <jats:italic>x<\/jats:italic>\n                    <jats:sub>2<\/jats:sub>\n                    ,\n                    <jats:italic>x<\/jats:italic>\n                    <jats:sub>3<\/jats:sub>\n                    ,\n                    <jats:italic>x<\/jats:italic>\n                    <jats:sub>4<\/jats:sub>\n                    is given by:\n                  <\/jats:p>\n                  <jats:p>\n                    <jats:disp-formula>\n                      <jats:alternatives>\n                        <jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/j_forma-2019-0005_eq_001.png\"\/>\n                        <m:math xmlns:m=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <m:mrow>\n                            <m:mo>(<\/m:mo>\n                            <m:msub>\n                              <m:mrow>\n                                <m:mi>x<\/m:mi>\n                              <\/m:mrow>\n                              <m:mn>1<\/m:mn>\n                            <\/m:msub>\n                            <m:mo>,<\/m:mo>\n                            <m:msub>\n                              <m:mrow>\n                                <m:mi>x<\/m:mi>\n                              <\/m:mrow>\n                              <m:mn>2<\/m:mn>\n                            <\/m:msub>\n                            <m:mo>;<\/m:mo>\n                            <m:msub>\n                              <m:mrow>\n                                <m:mi>x<\/m:mi>\n                              <\/m:mrow>\n                              <m:mn>3<\/m:mn>\n                            <\/m:msub>\n                            <m:mo>,<\/m:mo>\n                            <m:msub>\n                              <m:mrow>\n                                <m:mi>x<\/m:mi>\n                              <\/m:mrow>\n                              <m:mn>4<\/m:mn>\n                            <\/m:msub>\n                            <m:mo>)<\/m:mo>\n                            <m:mo>=<\/m:mo>\n                            <m:mfrac>\n                              <m:mrow>\n                                <m:msub>\n                                  <m:mrow>\n                                    <m:mi>x<\/m:mi>\n                                  <\/m:mrow>\n                                  <m:mn>3<\/m:mn>\n                                <\/m:msub>\n                                <m:mo>-<\/m:mo>\n                                <m:msub>\n                                  <m:mrow>\n                                    <m:mi>x<\/m:mi>\n                                  <\/m:mrow>\n                                  <m:mn>1<\/m:mn>\n                                <\/m:msub>\n                              <\/m:mrow>\n                              <m:mrow>\n                                <m:msub>\n                                  <m:mrow>\n                                    <m:mi>x<\/m:mi>\n                                  <\/m:mrow>\n                                  <m:mn>3<\/m:mn>\n                                <\/m:msub>\n                                <m:mo>-<\/m:mo>\n                                <m:msub>\n                                  <m:mrow>\n                                    <m:mi>x<\/m:mi>\n                                  <\/m:mrow>\n                                  <m:mn>2<\/m:mn>\n                                <\/m:msub>\n                              <\/m:mrow>\n                            <\/m:mfrac>\n                            <m:mo>.<\/m:mo>\n                            <m:mfrac>\n                              <m:mrow>\n                                <m:msub>\n                                  <m:mrow>\n                                    <m:mi>x<\/m:mi>\n                                  <\/m:mrow>\n                                  <m:mn>4<\/m:mn>\n                                <\/m:msub>\n                                <m:mo>-<\/m:mo>\n                                <m:msub>\n                                  <m:mrow>\n                                    <m:mi>x<\/m:mi>\n                                  <\/m:mrow>\n                                  <m:mn>2<\/m:mn>\n                                <\/m:msub>\n                              <\/m:mrow>\n                              <m:mrow>\n                                <m:msub>\n                                  <m:mrow>\n                                    <m:mi>x<\/m:mi>\n                                  <\/m:mrow>\n                                  <m:mn>4<\/m:mn>\n                                <\/m:msub>\n                                <m:mo>-<\/m:mo>\n                                <m:msub>\n                                  <m:mrow>\n                                    <m:mi>x<\/m:mi>\n                                  <\/m:mrow>\n                                  <m:mn>1<\/m:mn>\n                                <\/m:msub>\n                              <\/m:mrow>\n                            <\/m:mfrac>\n                          <\/m:mrow>\n                        <\/m:math>\n                        <jats:tex-math>$$({x_1},{x_2};{x_3},{x_4}) = {{{x_3} - {x_1}} \\over {{x_3} - {x_2}}}.{{{x_4} - {x_2}} \\over {{x_4} - {x_1}}}$$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:disp-formula>\n                  <\/jats:p>\n                  <jats:p>\n                    In 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 authors\n                    <jats:sup>4<\/jats:sup>\n                    [7]. The definitions can be directly linked in the HTMLized version of the Mizar library\n                    <jats:sup>5<\/jats:sup>\n                    .\n                  <\/jats:p>\n                  <jats:p>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].<\/jats:p>","DOI":"10.2478\/forma-2019-0005","type":"journal-article","created":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T05:33:51Z","timestamp":1558071231000},"page":"47-60","source":"Crossref","is-referenced-by-count":0,"title":["Cross-Ratio in Real Vector Space"],"prefix":"10.2478","volume":"27","author":[{"given":"Roland","family":"Coghetto","sequence":"first","affiliation":[{"name":"Rue de la Brasserie 5, 7100 La Louvi\u00e8re , Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"374","published-online":{"date-parts":[[2019,5,16]]},"reference":[{"key":"2026071214315383436_j_forma-2019-0005_ref_001_w2aab3b7b4b1b6b1ab1ab1Aa","doi-asserted-by":"crossref","unstructured":"[1] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, 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\u2013279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007\/978-3-319-20615-8_17.10.1007\/978-3-319-20615-8_17","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"2026071214315383436_j_forma-2019-0005_ref_002_w2aab3b7b4b1b6b1ab1ab2Aa","doi-asserted-by":"crossref","unstructured":"[2] Roland Coghetto. Klein-Beltrami model. Part I. Formalized Mathematics, 26(1):21\u201332, 2018. doi:10.2478\/forma-2018-0003.10.2478\/forma-2018-0003","DOI":"10.2478\/forma-2018-0003"},{"key":"2026071214315383436_j_forma-2019-0005_ref_003_w2aab3b7b4b1b6b1ab1ab3Aa","doi-asserted-by":"crossref","unstructured":"[3] Roland Coghetto. Klein-Beltrami model. Part II. Formalized Mathematics, 26(1):33\u201348, 2018. doi:10.2478\/forma-2018-0004.10.2478\/forma-2018-0004","DOI":"10.2478\/forma-2018-0004"},{"key":"2026071214315383436_j_forma-2019-0005_ref_004_w2aab3b7b4b1b6b1ab1ab4Aa","unstructured":"[4] Noboru Endou. Complex linear space and complex normed space. Formalized Mathematics, 12(2):93\u2013102, 2004."},{"key":"2026071214315383436_j_forma-2019-0005_ref_005_w2aab3b7b4b1b6b1ab1ab5Aa","unstructured":"[5] 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\u20132):33\u201342, 2003."},{"key":"2026071214315383436_j_forma-2019-0005_ref_006_w2aab3b7b4b1b6b1ab1ab6Aa","unstructured":"[6] Eugeniusz Kusak, Wojciech Leo\u0144czuk, and Micha\u0142 Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335\u2013342, 1990."},{"key":"2026071214315383436_j_forma-2019-0005_ref_007_w2aab3b7b4b1b6b1ab1ab7Aa","doi-asserted-by":"crossref","unstructured":"[7] 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\u2013347. Springer, Cham, 2015. doi:10.1007\/978-3-319-20615-8_25.10.1007\/978-3-319-20615-8_25","DOI":"10.1007\/978-3-319-20615-8_25"},{"key":"2026071214315383436_j_forma-2019-0005_ref_008_w2aab3b7b4b1b6b1ab1ab8Aa","doi-asserted-by":"crossref","unstructured":"[8] 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\u2013245, 2015.10.4171\/148-1\/9","DOI":"10.4171\/148-1\/9"},{"key":"2026071214315383436_j_forma-2019-0005_ref_009_w2aab3b7b4b1b6b1ab1ab9Aa","doi-asserted-by":"crossref","unstructured":"[9] J\u00fcrgen Richter-Gebert. Perspectives on projective geometry: a guided tour through real and complex geometry. Springer Science & Business Media, 2011.10.1007\/978-3-642-17286-1","DOI":"10.1007\/978-3-642-17286-1"},{"key":"2026071214315383436_j_forma-2019-0005_ref_010_w2aab3b7b4b1b6b1ab1ac10Aa","unstructured":"[10] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291\u2013296, 1990."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/27\/1\/article-p47.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2019-0005","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,12]],"date-time":"2026-07-12T23:29:35Z","timestamp":1783898975000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2019-0005"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4,1]]},"references-count":10,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2019,5,16]]},"published-print":{"date-parts":[[2019,4,1]]}},"alternative-id":["10.2478\/forma-2019-0005"],"URL":"https:\/\/doi.org\/10.2478\/forma-2019-0005","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2019,4,1]]}}}