REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/21437
Pełny rekord metadanych
Pole DCWartośćJęzyk
dc.contributor.authorBancerek, Grzegorz-
dc.date.accessioned2026-11-05T09:32:35Z-
dc.date.available2026-11-05T09:32:35Z-
dc.date.issued2005-
dc.identifier.citationFormalized Mathematics, Volume 13, Issue 1, Pages 171-179pl
dc.identifier.issn1426-2630-
dc.identifier.urihttp://hdl.handle.net/11320/21437-
dc.description.abstractWe 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.isoenpl
dc.publisherUniversity of Białystokpl
dc.rightsCC BY-SA 4.0-
dc.rights.urihttps://creativecommons.org/licenses/by-sa/4.0/-
dc.titleOn Constructing Topological Spaces and Sorgenfrey Linepl
dc.typeArticlepl
dc.rights.holder© 2005 University of Białystokpl
dc.rights.holderThis work is licensed under the Creative Commons License.pl
dc.description.AffiliationBiałystok Technical Universitypl
dc.description.referencesGrzegorz Bancerek. Arithmetic of non negative rational numbers. To appear in Formalized Mathematics.pl
dc.description.referencesGrzegorz Bancerek. Cardinal arithmetics. Formalized Mathematics, 1(3):543–547, 1990.pl
dc.description.referencesGrzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.pl
dc.description.referencesGrzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.pl
dc.description.referencesGrzegorz Bancerek. König’s theorem. Formalized Mathematics, 1(3):589–593, 1990.pl
dc.description.referencesGrzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.pl
dc.description.referencesGrzegorz Bancerek. Sequences of ordinal numbers. Formalized Mathematics, 1(2):281-290, 1990.pl
dc.description.referencesGrzegorz Bancerek. Countable sets and Hessenberg’s theorem. Formalized Mathematics, 2(1):65–69, 1991.pl
dc.description.referencesGrzegorz Bancerek. On the characteristic and weight of a topological space. Formalized Mathematics, 13(1):163–169, 2005.pl
dc.description.referencesGrzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.pl
dc.description.referencesGrzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Formalized Mathematics, 5(4):485–492, 1996.pl
dc.description.referencesLeszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481-485, 1991.pl
dc.description.referencesCzesław Byliński. A classical first order language. Formalized Mathematics, 1(4):669–676, 1990.pl
dc.description.referencesCzesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507–513, 1990.pl
dc.description.referencesCzesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990pl
dc.description.referencesCzesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.pl
dc.description.referencesCzesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.pl
dc.description.referencesAgata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.pl
dc.description.referencesRyszard Engelking. General Topology, volume 60 of Monografie Matematyczne. PWN Polish Scientific Publishers, Warsaw, 1977.pl
dc.description.referencesMariusz Giero. Hierarchies and classifications of sets. Formalized Mathematics, 9(4):865-869, 2001.pl
dc.description.referencesZbigniew Karno. On discrete and almost discrete topological spaces. Formalized Mathematics, 3(2):305–310, 1992.pl
dc.description.referencesZbigniew Karno. Maximal discrete subspaces of almost discrete topological spaces. Formalized Mathematics, 4(1):125–135, 1993.pl
dc.description.referencesAndrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5):841–845, 1990.pl
dc.description.referencesJarosław Kotowicz. Monotone real sequences. Subsequences. Formalized Mathematics, 1(3):471–475, 1990.pl
dc.description.referencesJarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269–272, 1990.pl
dc.description.referencesJarosław Kotowicz. The limit of a real function at infinity. Formalized Mathematics, 2(1):17–28, 1991pl
dc.description.referencesRafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887–890, 1990.pl
dc.description.referencesRobert Milewski. Bases of continuous lattices. Formalized Mathematics, 7(2):285–294, 1998.pl
dc.description.referencesYatsuka Nakamura. Half open intervals in real numbers. Formalized Mathematics, 10(1):21–22, 2002.pl
dc.description.referencesBeata Padlewska. Families of sets. Formalized Mathematics, 1(1):147–152, 1990.pl
dc.description.referencesBeata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.pl
dc.description.referencesKonrad Raczkowski. Integer and rational exponents. Formalized Mathematics, 2(1):125-130, 1991.pl
dc.description.referencesKonrad Raczkowski and Andrzej Nędzusiak. Series. Formalized Mathematics, 2(4):449-452, 1991.pl
dc.description.referencesKonrad Raczkowski and Paweł Sadowski. Topological properties of subsets in real numbers. Formalized Mathematics, 1(4):777–780, 1990.pl
dc.description.referencesPiotr Rudnicki and Andrzej Trybulec. Abian’s fixed point theorem. Formalized Mathematics, 6(3):335–338, 1997.pl
dc.description.referencesAlexander Yu. Shibakov and Andrzej Trybulec. The Cantor set. Formalized Mathematics, 5(2):233–236, 1996.pl
dc.description.referencesAndrzej Trybulec. Subsets of complex numbers. To appear in Formalized Mathematics.pl
dc.description.referencesAndrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.pl
dc.description.referencesAndrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.pl
dc.description.referencesAndrzej Trybulec. Many-sorted sets. Formalized Mathematics, 4(1):15–22, 1993.pl
dc.description.referencesAndrzej Trybulec. Many-sorted sets. Formalized Mathematics, 4(1):15–22, 1993.pl
dc.description.referencesAndrzej Trybulec and Czeslaw Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.pl
dc.description.referencesAndrzej Trybulec and Agata Darmochwał. Boolean domains. Formalized Mathematics, 1(1):187–190, 1990.pl
dc.description.referencesMicha l J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990.pl
dc.description.referencesZinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.pl
dc.description.referencesEdmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.pl
dc.description.referencesEdmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990.pl
dc.description.referencesMirosław Wysocki and Agata Darmochwał. Subsets of topological spaces. Formalized Mathematics, 1(1):231–237, 1990.pl
dc.identifier.eissn1898-9934-
dc.description.volume13pl
dc.description.issue1pl
dc.description.firstpage171pl
dc.description.lastpage179pl
dc.identifier.citation2Formalized Mathematicspl
Występuje w kolekcji(ach):Formalized Mathematics, 2005, Volume 13, Issue 1

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
On_Constructing_Topological_Spaces.pdf122,48 kBAdobe PDFOtwórz
Pokaż uproszczony widok rekordu Zobacz statystyki


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