Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
Tytuł: A Case Study of Transporting Urysohn’s Lemma from Topology via Open Sets into Topology via Neighborhoods
Autorzy: Coghetto, Roland
Słowa kluczowe: filter
topology via neighborhoods
transfer principle
transport of structure
Data wydania: 2020
Data dodania: 5-maj-2021
Wydawca: DeGruyter Open
Źródło: Formalized Mathematics, Volume 28, Issue 3, Pages 227-237
Abstrakt: Józef Białas and Yatsuka Nakamura has completely formalized a proof of Urysohn’s lemma in the article [4], in the context of a topological space defined via open sets. In the Mizar Mathematical Library (MML), the topological space is defined in this way by Beata Padlewska and Agata Darmochwał in the article [18]. In [7] the topological space is defined via neighborhoods. It is well known that these definitions are equivalent [5, 6]. In the definitions, an abstract structure (i.e. the article [17, STRUCT 0] and its descendants, all of them directly or indirectly using Mizar structures [3]) have been used (see [10], [9]). The first topological definition is based on the Mizar structure TopStruct and the topological space defined via neighborhoods with the Mizar structure: FMT Space Str. To emphasize the notion of a neighborhood, we rename FMT TopSpace (topology from neighbourhoods) to NTopSpace (a neighborhood topological space). Using Mizar [2], we transport the Urysohn’s lemma from TopSpace to NTop-Space. In some cases, Mizar allows certain techniques for transporting proofs, definitions or theorems. Generally speaking, there is no such automatic translating. In Coq, Isabelle/HOL or homotopy type theory transport is also studied, sometimes with a more systematic aim [14], [21], [11], [12], [8], [19]. In [1], two co-existing Isabelle libraries: Isabelle/HOL and Isabelle/Mizar, have been aligned in a single foundation in the Isabelle logical framework. In the MML, they have been used since the beginning: reconsider, registration, cluster, others were later implemented [13]: identify. In some proofs, it is possible to define particular functors between different structures, mainly useful when results are already obtained in a given structure. This technique is used, for example, in [15] to define two functors MXR2MXF and MXF2MXF between Matrix of REAL and Matrix of F-Real and to transport the definition of the addition from one structure to the other: [...] A + B -> Matrix of REAL equals MXF2MXR ((MXR2MXF A) + (MXR2MXF B)) [...]. In this paper, first we align the necessary topological concepts. For the formalization, we were inspired by the works of Claude Wagschal [20]. It allows us to transport more naturally the Urysohn’s lemma ([4, URYSOHN3:20]) to the topological space defined via neighborhoods. Nakasho and Shidama have developed a solution to explore the notions introduced in various ways [16]. The definitions can be directly linked in the HTML version of the Mizar library (example: Urysohn’s lemma
DOI: 10.2478/forma-2020-0020
ISSN: 1426-2630
e-ISSN: 1898-9934
metadata.dc.identifier.orcid: 0000-0002-4901-0766
Typ Dokumentu: Article
Właściciel praw: © 2020 University of Białymstoku;
CC-BY-SA License ver. 3.0 or later;
Występuje w kolekcji(ach):Formalized Mathematics, 2020, Volume 28, Issue 3

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
10.2478_forma-2020-0020.pdf297,38 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons