<abstract xmlns="http://www.w3.org/1999/xhtml">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 <italic>x</italic>1, <italic>x</italic>2, <italic>x</italic>3, <italic>x</italic>4 is given by:<disp-formula><alternatives><graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2019-0005_eq_001.png"></graphic><math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mrow><mo>(</mo><msub><mrow><mi>x</mi></mrow><mn>1</mn></msub><mo>,</mo><msub><mrow><mi>x</mi></mrow><mn>2</mn></msub><mo>;</mo><msub><mrow><mi>x</mi></mrow><mn>3</mn></msub><mo>,</mo><msub><mrow><mi>x</mi></mrow><mn>4</mn></msub><mo>)</mo><mo>=</mo><mfrac><mrow><msub><mrow><mi>x</mi></mrow><mn>3</mn></msub><mo>-</mo><msub><mrow><mi>x</mi></mrow><mn>1</mn></msub></mrow><mrow><msub><mrow><mi>x</mi></mrow><mn>3</mn></msub><mo>-</mo><msub><mrow><mi>x</mi></mrow><mn>2</mn></msub></mrow></mfrac><mo>.</mo><mfrac><mrow><msub><mrow><mi>x</mi></mrow><mn>4</mn></msub><mo>-</mo><msub><mrow><mi>x</mi></mrow><mn>2</mn></msub></mrow><mrow><msub><mrow><mi>x</mi></mrow><mn>4</mn></msub><mo>-</mo><msub><mrow><mi>x</mi></mrow><mn>1</mn></msub></mrow></mfrac></mrow></math><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}}}$$</tex-math></alternatives></disp-formula>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 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].</abstract>

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-x1$$({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}}}$$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 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].

Cross-Ratio in Real Vector Space

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 Public License.

{"article-title":"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...

Cross-Ratio in Real Vector Space

Published Online: May 16, 2019

Page range: 47 - 60

Accepted: Feb 27, 2019

DOI: https://doi.org/10.2478/forma-2019-0005

Keywords
affine ratio, cross-ratio, real vector space, geometry

© 2019 Roland Coghetto, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 Public License.

Cross-Ratio in Real Vector Space

Published Online: May 16, 2019

Page range: 47 - 60

Accepted: Feb 27, 2019

DOI: https://doi.org/10.2478/forma-2019-0005

Keywordsaffine ratio, cross-ratio, real vector space, geometry

© 2019 Roland Coghetto, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 Public License.

Keywords
affine ratio, cross-ratio, real vector space, geometry