PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
2016 | 24 | 4 | 239-251
Tytuł artykułu

Homography in ℝℙ

Autorzy
Treść / Zawartość
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
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.
Wydawca
Rocznik
Tom
24
Numer
4
Strony
239-251
Opis fizyczny
Daty
wydano
2016-12-01
otrzymano
2016-10-18
online
2017-02-23
Twórcy
  • Rue de la Brasserie 5, 7100 La Louvière,
Bibliografia
Typ dokumentu
Bibliografia
Identyfikatory
Identyfikator YADDA
bwmeta1.element.doi-10_1515_forma-2016-0020
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.