Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/5558
Tytuł: | Homography in ℝℙ |
Autorzy: | Coghetto, Roland |
Słowa kluczowe: | projectivity projective transformation projective collineation real projective plane Grassmann-Plücker relation |
Data wydania: | 2016 |
Data dodania: | 2-cze-2017 |
Wydawca: | De Gruyter Open |
Źródło: | Formalized Mathematics, Volume 24, Issue 4, pp. 239-252 |
Abstrakt: | The real projective plane has been formalized in Isabelle/HOL by Timothy Makarios [13] and in Coq by Nicolas Magaud, Julien Narboux and Pascal Schreck [12].Some definitions on the real projective spaces were introduced early in the Mizar Mathematical Library by Wojciech Leonczuk [9], Krzysztof Prazmowski [10] and by Wojciech Skaba [18].In this article, we check with the Mizar system [4], some properties on the determinants and the Grassmann-Plücker relation in rank 3 [2], [1], [7], [16], [17].Then we show that the projective space induced (in the sense defined in [9]) by ℝ3 is a projective plane (in the sense defined in [10]).Finally, in the real projective plane, we define the homography induced by a 3-by-3 invertible matrix and we show that the images of 3 collinear points are themselves collinear. |
Afiliacja: | Rue de la Brasserie 5, 7100 La Louvière, Belgium |
URI: | http://hdl.handle.net/11320/5558 |
DOI: | 10.1515/forma-2016-0020 |
ISSN: | 1426-2630 1898-9934 |
Typ Dokumentu: | Article |
Występuje w kolekcji(ach): | Formalized Mathematics, 2016, Volume 24, Issue 4 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma-2016-0020.pdf | 275,26 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL