Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/13652
Tytuł: | Duality Notions in Real Projective Plane |
Autorzy: | Coghetto, Roland |
Słowa kluczowe: | Principle of Duality duality real projective plane converse theorem |
Data wydania: | 2021 |
Data dodania: | 22-lip-2022 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 29, Issue 4, Pages 161-173 |
Abstrakt: | In this article, we check with the Mizar system [1], [2], the converse of Desargues’ theorem and the converse of Pappus’ theorem of the real projective plane. It is well known that in the projective plane, the notions of points and lines are dual [11], [9], [15], [8]. Some results (analytical, synthetic, combinatorial) of projective geometry are already present in some libraries Lean/Hott [5], Isabelle/Hol [3], Coq [13], [14], [4], Agda [6], . . . . Proofs of dual statements by proof assistants have already been proposed, using an axiomatic method (for example see in [13] - the section on duality: “[...] For every theorem we prove, we can easily derive its dual using our function swap [...]2”). In our formalisation, we use an analytical rather than a synthetic approach using the definitions of Leończuk and Prażmowski of the projective plane [12]. Our motivation is to show that it is possible by developing dual definitions to find proofs of dual theorems in a few lines of code. In the first part, rather technical, we introduce definitions that allow us to construct the duality between the points of the real projective plane and the lines associated to this projective plane. In the second part, we give a natural definition of line concurrency and prove that this definition is dual to the definition of alignment. Finally, we apply these results to find, in a few lines, the dual properties and theorems of those defined in the article [12] (transitive, Vebleian, at_least_3rank, Fanoian, Desarguesian, 2-dimensional). We hope that this methodology will allow us to continued more quickly the proof started in [7] that the Beltrami-Klein plane is a model satisfying the axioms of the hyperbolic plane (in the sense of Tarski geometry [10]). |
Opis: | This work has been supported by the Centre autonome de formation et de recherche en mathematiques et sciences avec assistants de preuve, ASBL (non-profit organization). Enterprise number: 0777.779.751. Belgium |
URI: | http://hdl.handle.net/11320/13652 |
DOI: | 10.2478/forma-2021-0016 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
metadata.dc.identifier.orcid: | 0000-0002-4901-0766 |
Typ Dokumentu: | Article |
metadata.dc.rights.uri: | https://creativecommons.org/licenses/by-sa/3.0/ |
Właściciel praw: | © 2021 University of Białymstoku CC-BY-SA License ver. 3.0 or later |
Występuje w kolekcji(ach): | Formalized Mathematics, 2021, Volume 29, Issue 4 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
10.2478_forma-2021-0016.pdf | 267,11 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL