Some Properties of the Sorgenfrey Line and the Sorgenfrey Plane

Adam St. Arnaud; Piotr Rudnicki

Formalized Mathematics (2013)

  • Volume: 21, Issue: 2, page 83-85
  • ISSN: 1426-2630

Abstract

top
We first provide a modified version of the proof in [3] that the Sorgenfrey line is T1. Here, we prove that it is in fact T2, a stronger result. Next, we prove that all subspaces of ℝ1 (that is the real line with the usual topology) are Lindel¨of. We utilize this result in the proof that the Sorgenfrey line is Lindel¨of, which is based on the proof found in [8]. 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¨of, and therefore the product space of two Lindel¨of spaces need not be Lindel¨of. Further, we note that the Sorgenfrey line is regular, following from [3]:59. Next, we observe that the Sorgenfrey line is normal since it is both regular and Lindel¨of. 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 [3], that the Niemytzki plane is not normal. Information was also gathered from [15].

How to cite

top

Adam St. Arnaud, and Piotr Rudnicki. "Some Properties of the Sorgenfrey Line and the Sorgenfrey Plane." Formalized Mathematics 21.2 (2013): 83-85. <http://eudml.org/doc/267067>.

@article{AdamSt2013,
abstract = {We first provide a modified version of the proof in [3] that the Sorgenfrey line is T1. Here, we prove that it is in fact T2, a stronger result. Next, we prove that all subspaces of ℝ1 (that is the real line with the usual topology) are Lindel¨of. We utilize this result in the proof that the Sorgenfrey line is Lindel¨of, which is based on the proof found in [8]. 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¨of, and therefore the product space of two Lindel¨of spaces need not be Lindel¨of. Further, we note that the Sorgenfrey line is regular, following from [3]:59. Next, we observe that the Sorgenfrey line is normal since it is both regular and Lindel¨of. 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 [3], that the Niemytzki plane is not normal. Information was also gathered from [15].},
author = {Adam St. Arnaud, Piotr Rudnicki},
journal = {Formalized Mathematics},
keywords = {topological spaces; products of normal spaces; Sorgenfrey line; Sorgenfrey plane; Lindelöf spaces},
language = {eng},
number = {2},
pages = {83-85},
title = {Some Properties of the Sorgenfrey Line and the Sorgenfrey Plane},
url = {http://eudml.org/doc/267067},
volume = {21},
year = {2013},
}

TY - JOUR
AU - Adam St. Arnaud
AU - Piotr Rudnicki
TI - Some Properties of the Sorgenfrey Line and the Sorgenfrey Plane
JO - Formalized Mathematics
PY - 2013
VL - 21
IS - 2
SP - 83
EP - 85
AB - We first provide a modified version of the proof in [3] that the Sorgenfrey line is T1. Here, we prove that it is in fact T2, a stronger result. Next, we prove that all subspaces of ℝ1 (that is the real line with the usual topology) are Lindel¨of. We utilize this result in the proof that the Sorgenfrey line is Lindel¨of, which is based on the proof found in [8]. 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¨of, and therefore the product space of two Lindel¨of spaces need not be Lindel¨of. Further, we note that the Sorgenfrey line is regular, following from [3]:59. Next, we observe that the Sorgenfrey line is normal since it is both regular and Lindel¨of. 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 [3], that the Niemytzki plane is not normal. Information was also gathered from [15].
LA - eng
KW - topological spaces; products of normal spaces; Sorgenfrey line; Sorgenfrey plane; Lindelöf spaces
UR - http://eudml.org/doc/267067
ER -

References

top
  1. [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990. 
  2. [2] Grzegorz Bancerek. On constructing topological spaces and Sorgenfrey line. Formalized Mathematics, 13(1):171-179, 2005. 
  3. [3] Grzegorz Bancerek. Niemytzki plane - an example of Tychonoff space which is not T4. Formalized Mathematics, 13(4):515-524, 2005. 
  4. [4] Grzegorz Bancerek. Bases and refinements of topologies. Formalized Mathematics, 7(1): 35-43, 1998. 
  5. [5] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  6. [6] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  7. [7] Agata Darmochwał and Yatsuka Nakamura. Metric spaces as topological spaces - fundamental concepts. Formalized Mathematics, 2(4):605-608, 1991. 
  8. [8] Ryszard Engelking. Outline of General Topology. North-Holland Publishing Company, 1968. 
  9. [9] Adam Grabowski. On the boundary and derivative of a set. Formalized Mathematics, 13 (1):139-146, 2005. 
  10. [10] Adam Grabowski. On the Borel families of subsets of topological spaces. Formalized Mathematics, 13(4):453-461, 2005. 
  11. [11] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5): 841-845, 1990. 
  12. [12] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223-230, 1990. 
  13. [13] Karol Pak. Basic properties of metrizable topological spaces. Formalized Mathematics, 17(3):201-205, 2009. doi:10.2478/v10037-009-0024-8.[Crossref] 
  14. [14] Konrad Raczkowski and Paweł Sadowski. Topological properties of subsets in real numbers. Formalized Mathematics, 1(4):777-780, 1990. 
  15. [15] Lynn Arthur Steen and J. Arthur Jr. Seebach. Counterexamples in Topology. Springer- Verlag, 1978. Zbl0386.54001
  16. [16] Andrzej Trybulec. A Borsuk theorem on homotopy types. Formalized Mathematics, 2(4): 535-545, 1991. 
  17. [17] Andrzej Trybulec. Subsets of complex numbers. Mizar Mathematical Library. 
  18. [18] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  19. [19] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990. 
  20. [20] Mirosław Wysocki and Agata Darmochwał. Subsets of topological spaces. Formalized Mathematics, 1(1):231-237, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.