Some properties of the Sorgenfrey line and the Sorgenfrey plane. (English) Zbl 1298.54013

Summary: We first provide a modified version of the proof in [G. Bancerek, “Niemytzki plane – an example of Tychonoff space which is not \(T_4\)”, Formaliz. Math. 13, No. 4, 515–524 (2005)] that the Sorgenfrey line is \(T_{1}\). Here, we prove that it is in fact \(T_2\), a stronger result. Next, we prove that all subspaces of \(\mathbb{R}^{1}\) (that is the real line with the usual topology) are Lindelöf. We utilize this result in the proof that the Sorgenfrey line is Lindelöf, which is based on the proof found in [R. Engelking, Outline of general topology. Amsterdam: North-Holland (1968; Zbl 0157.53001)]. Next, we construct the Sorgenfrey plane, as the product topology of the Sorgenfrey line and itself. We prove that the Sorgenfrey plane is not Lindelöf, and therefore the product space of two Lindelöf spaces need not be Lindelöf. Further, we note that the Sorgenfrey line is regular, following from [Bancerek, loc. cit.]. Next, we observe that the Sorgenfrey line is normal since it is both regular and Lindelöf. Finally, we prove that the Sorgenfrey plane is not normal, and hence the product of two normal spaces need not be normal. The proof that the Sorgenfrey plane is not normal and many of the lemmas leading up to this result are modelled after the proof in [Bancerek, loc. cit.], that the Niemytzki plane is not normal. Information was also gathered from [L. A. Steen and J. A. Seebach jun., Counterexamples in topology. New York, Heidelberg, Berlin: Springer (1978; Zbl 0386.54001)].


54D15 Higher separation axioms (completely regular, normal, perfectly or collectionwise normal, etc.)
54B10 Product spaces in general topology
03B35 Mechanization of proofs and logical operations
Full Text: DOI


[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.;
[2] Grzegorz Bancerek. On constructing topological spaces and Sorgenfrey line. Formalized Mathematics, 13(1):171-179, 2005.;
[3] Grzegorz Bancerek. Niemytzki plane - an example of Tychonoff space which is not T4. Formalized Mathematics, 13(4):515-524, 2005.;
[4] Grzegorz Bancerek. Bases and refinements of topologies. Formalized Mathematics, 7(1): 35-43, 1998.;
[5] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.;
[6] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.;
[7] Agata Darmochwał and Yatsuka Nakamura. Metric spaces as topological spaces - fundamental concepts. Formalized Mathematics, 2(4):605-608, 1991.;
[8] Ryszard Engelking. Outline of General Topology. North-Holland Publishing Company, 1968.; · Zbl 0157.53001
[9] Adam Grabowski. On the boundary and derivative of a set. Formalized Mathematics, 13 (1):139-146, 2005.;
[10] Adam Grabowski. On the Borel families of subsets of topological spaces. Formalized Mathematics, 13(4):453-461, 2005.;
[11] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5): 841-845, 1990.;
[12] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223-230, 1990.;
[13] Karol Pak. Basic properties of metrizable topological spaces. Formalized Mathematics, 17(3):201-205, 2009. doi:10.2478/v10037-009-0024-8.;
[14] Konrad Raczkowski and Paweł Sadowski. Topological properties of subsets in real numbers. Formalized Mathematics, 1(4):777-780, 1990.;
[15] Lynn Arthur Steen and J. Arthur Jr. Seebach. Counterexamples in Topology. Springer- Verlag, 1978.; · Zbl 0386.54001
[16] Andrzej Trybulec. A Borsuk theorem on homotopy types. Formalized Mathematics, 2(4): 535-545, 1991.;
[17] Andrzej Trybulec. Subsets of complex numbers. Mizar Mathematical Library.; · Zbl 0343.02003
[18] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.; · Zbl 0725.65053
[19] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.;
[20] Mirosław Wysocki and Agata Darmochwał. Subsets of topological spaces. Formalized Mathematics, 1(1):231-237, 1990.;
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.