Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/21437Pełny rekord metadanych
| Pole DC | Wartość | Język |
|---|---|---|
| dc.contributor.author | Bancerek, Grzegorz | - |
| dc.date.accessioned | 2026-11-05T09:32:35Z | - |
| dc.date.available | 2026-11-05T09:32:35Z | - |
| dc.date.issued | 2005 | - |
| dc.identifier.citation | Formalized Mathematics, Volume 13, Issue 1, Pages 171-179 | pl |
| dc.identifier.issn | 1426-2630 | - |
| dc.identifier.uri | http://hdl.handle.net/11320/21437 | - |
| dc.description.abstract | We continue Mizar formalization of General Topology according to the book [19] by Engelking. In the article the formalization of Section 1.2 is almost completed. Namely, we formalize theorems on introduction of topologies by bases, neighborhood systems, closed sets, closure operator, and interior operator. The Sorgenfrey line is defined by a basis. It is proved that the weight of it is continuum. Other techniques are used to demonstrate introduction of discrete and anti-discrete topologies. | pl |
| dc.language.iso | en | pl |
| dc.publisher | University of Białystok | pl |
| dc.rights | CC BY-SA 4.0 | - |
| dc.rights.uri | https://creativecommons.org/licenses/by-sa/4.0/ | - |
| dc.title | On Constructing Topological Spaces and Sorgenfrey Line | pl |
| dc.type | Article | pl |
| dc.rights.holder | © 2005 University of Białystok | pl |
| dc.rights.holder | This work is licensed under the Creative Commons License. | pl |
| dc.description.Affiliation | Białystok Technical University | pl |
| dc.description.references | Grzegorz Bancerek. Arithmetic of non negative rational numbers. To appear in Formalized Mathematics. | pl |
| dc.description.references | Grzegorz Bancerek. Cardinal arithmetics. Formalized Mathematics, 1(3):543–547, 1990. | pl |
| dc.description.references | Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990. | pl |
| dc.description.references | Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990. | pl |
| dc.description.references | Grzegorz Bancerek. König’s theorem. Formalized Mathematics, 1(3):589–593, 1990. | pl |
| dc.description.references | Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990. | pl |
| dc.description.references | Grzegorz Bancerek. Sequences of ordinal numbers. Formalized Mathematics, 1(2):281-290, 1990. | pl |
| dc.description.references | Grzegorz Bancerek. Countable sets and Hessenberg’s theorem. Formalized Mathematics, 2(1):65–69, 1991. | pl |
| dc.description.references | Grzegorz Bancerek. On the characteristic and weight of a topological space. Formalized Mathematics, 13(1):163–169, 2005. | pl |
| dc.description.references | Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990. | pl |
| dc.description.references | Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Formalized Mathematics, 5(4):485–492, 1996. | pl |
| dc.description.references | Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481-485, 1991. | pl |
| dc.description.references | Czesław Byliński. A classical first order language. Formalized Mathematics, 1(4):669–676, 1990. | pl |
| dc.description.references | Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507–513, 1990. | pl |
| dc.description.references | Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990 | pl |
| dc.description.references | Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990. | pl |
| dc.description.references | Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990. | pl |
| dc.description.references | Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990. | pl |
| dc.description.references | Ryszard Engelking. General Topology, volume 60 of Monografie Matematyczne. PWN Polish Scientific Publishers, Warsaw, 1977. | pl |
| dc.description.references | Mariusz Giero. Hierarchies and classifications of sets. Formalized Mathematics, 9(4):865-869, 2001. | pl |
| dc.description.references | Zbigniew Karno. On discrete and almost discrete topological spaces. Formalized Mathematics, 3(2):305–310, 1992. | pl |
| dc.description.references | Zbigniew Karno. Maximal discrete subspaces of almost discrete topological spaces. Formalized Mathematics, 4(1):125–135, 1993. | pl |
| dc.description.references | Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5):841–845, 1990. | pl |
| dc.description.references | Jarosław Kotowicz. Monotone real sequences. Subsequences. Formalized Mathematics, 1(3):471–475, 1990. | pl |
| dc.description.references | Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269–272, 1990. | pl |
| dc.description.references | Jarosław Kotowicz. The limit of a real function at infinity. Formalized Mathematics, 2(1):17–28, 1991 | pl |
| dc.description.references | Rafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887–890, 1990. | pl |
| dc.description.references | Robert Milewski. Bases of continuous lattices. Formalized Mathematics, 7(2):285–294, 1998. | pl |
| dc.description.references | Yatsuka Nakamura. Half open intervals in real numbers. Formalized Mathematics, 10(1):21–22, 2002. | pl |
| dc.description.references | Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147–152, 1990. | pl |
| dc.description.references | Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990. | pl |
| dc.description.references | Konrad Raczkowski. Integer and rational exponents. Formalized Mathematics, 2(1):125-130, 1991. | pl |
| dc.description.references | Konrad Raczkowski and Andrzej Nędzusiak. Series. Formalized Mathematics, 2(4):449-452, 1991. | pl |
| dc.description.references | Konrad Raczkowski and Paweł Sadowski. Topological properties of subsets in real numbers. Formalized Mathematics, 1(4):777–780, 1990. | pl |
| dc.description.references | Piotr Rudnicki and Andrzej Trybulec. Abian’s fixed point theorem. Formalized Mathematics, 6(3):335–338, 1997. | pl |
| dc.description.references | Alexander Yu. Shibakov and Andrzej Trybulec. The Cantor set. Formalized Mathematics, 5(2):233–236, 1996. | pl |
| dc.description.references | Andrzej Trybulec. Subsets of complex numbers. To appear in Formalized Mathematics. | pl |
| dc.description.references | Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990. | pl |
| dc.description.references | Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990. | pl |
| dc.description.references | Andrzej Trybulec. Many-sorted sets. Formalized Mathematics, 4(1):15–22, 1993. | pl |
| dc.description.references | Andrzej Trybulec. Many-sorted sets. Formalized Mathematics, 4(1):15–22, 1993. | pl |
| dc.description.references | Andrzej Trybulec and Czeslaw Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990. | pl |
| dc.description.references | Andrzej Trybulec and Agata Darmochwał. Boolean domains. Formalized Mathematics, 1(1):187–190, 1990. | pl |
| dc.description.references | Micha l J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990. | pl |
| dc.description.references | Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990. | pl |
| dc.description.references | Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990. | pl |
| dc.description.references | Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990. | pl |
| dc.description.references | Mirosław Wysocki and Agata Darmochwał. Subsets of topological spaces. Formalized Mathematics, 1(1):231–237, 1990. | pl |
| dc.identifier.eissn | 1898-9934 | - |
| dc.description.volume | 13 | pl |
| dc.description.issue | 1 | pl |
| dc.description.firstpage | 171 | pl |
| dc.description.lastpage | 179 | pl |
| dc.identifier.citation2 | Formalized Mathematics | pl |
| Występuje w kolekcji(ach): | Formalized Mathematics, 2005, Volume 13, Issue 1 | |
Pliki w tej pozycji:
| Plik | Opis | Rozmiar | Format | |
|---|---|---|---|---|
| On_Constructing_Topological_Spaces.pdf | 122,48 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL
