:: Some Properties of the {S}orgenfrey Line and the {S}orgenfrey Plane
:: by Adam J.J. St. Arnaud and Piotr Rudnicki
::
:: Received April 17, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users

Lm1: for f being Function
for x, y being set st x in f " {y} holds
f . x = y

proof end;

Lm2: Sorgenfrey-line is T_2

proof end;

registration

cluster Sorgenfrey-line -> T_2 ;

coherence
Sorgenfrey-line is T_2 by Lm2;

end;

theorem Th1: :: TOPGEN_6:1

for x, a, b being Real st x in ].a,b.[ holds
ex p, r being Rational st
( x in ].p,r.[ & ].p,r.[ c= ].a,b.[ )

proof end;

Lm3: for T being SubSpace of R^1 holds T is Lindelof

proof end;

registration

cluster -> Lindelof for SubSpace of R^1 ;

coherence
for b₁ being SubSpace of R^1 holds b₁ is Lindelof by Lm3;

end;

Lm4: for p, r being Real st r > p holds
ex q being Rational st q in [.p,r.[

proof end;

Lm5: the carrier of Sorgenfrey-line = REAL
by TOPGEN_3:def 2;

consider BB being Subset-Family of REAL such that
Lm6: the topology of Sorgenfrey-line = UniCl BB and
Lm7: BB = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } by TOPGEN_3:def 2;

Lm8: BB is Basis of Sorgenfrey-line
by Lm5, Lm6, CANTOR_1:1, CANTOR_1:def 2, TOPS_2:64;

Lm9: Sorgenfrey-line is Lindelof

proof end;

registration

cluster Sorgenfrey-line -> Lindelof ;

coherence
Sorgenfrey-line is Lindelof by Lm9;

end;

definition

func Sorgenfrey-plane -> non empty strict TopSpace equals :: TOPGEN_6:def 1
[:Sorgenfrey-line,Sorgenfrey-line:];

correctness
coherence
[:Sorgenfrey-line,Sorgenfrey-line:] is non empty strict TopSpace;
;

end;

:: deftheorem defines Sorgenfrey-plane TOPGEN_6:def 1 :
Sorgenfrey-plane = [:Sorgenfrey-line,Sorgenfrey-line:];

definition

func real-anti-diagonal -> Subset of [:REAL,REAL:] equals :: TOPGEN_6:def 2
{ [x,y] where x, y is Real : y = - x } ;

correctness
coherence
{ [x,y] where x, y is Real : y = - x } is Subset of [:REAL,REAL:];

proof end;

end;

:: deftheorem defines real-anti-diagonal TOPGEN_6:def 2 :
real-anti-diagonal = { [x,y] where x, y is Real : y = - x } ;

theorem Th2: :: TOPGEN_6:2

[:RAT,RAT:] is dense Subset of Sorgenfrey-plane

proof end;

theorem Th3: :: TOPGEN_6:3

card real-anti-diagonal = continuum

proof end;

theorem Th4: :: TOPGEN_6:4

real-anti-diagonal is closed Subset of Sorgenfrey-plane

proof end;

the carrier of Sorgenfrey-line = REAL
by TOPGEN_3:def 2;

then Lm10: the carrier of Sorgenfrey-plane = [:REAL,REAL:]
by BORSUK_1:def 2;

Lm11: for x, y being Real st [x,y] in real-anti-diagonal holds
y = - x

proof end;

theorem Th5: :: TOPGEN_6:5

for A being Subset of Sorgenfrey-plane st A = real-anti-diagonal holds
Der A is empty

proof end;

theorem Th6: :: TOPGEN_6:6

for A being Subset of real-anti-diagonal holds A is closed Subset of Sorgenfrey-plane

proof end;

Lm12: not Sorgenfrey-plane is Lindelof

proof end;

registration

cluster Sorgenfrey-plane -> non empty strict non Lindelof ;

coherence
not Sorgenfrey-plane is Lindelof by Lm12;

end;

registration

cluster Sorgenfrey-line -> regular ;

coherence
Sorgenfrey-line is regular by TOPGEN_5:59;

end;

registration

cluster Sorgenfrey-line -> normal ;

coherence
Sorgenfrey-line is normal ;

end;

Lm13: not Sorgenfrey-plane is normal

proof end;

registration

cluster Sorgenfrey-plane -> non empty strict non normal ;

coherence
not Sorgenfrey-plane is normal by Lm13;

end;