:: 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;

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.[ )

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;

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
end;

definition

coherence

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

;

end;

func Sorgenfrey-plane -> non empty strict TopSpace equals :: TOPGEN_6:def 1

[:Sorgenfrey-line,Sorgenfrey-line:];

correctness [:Sorgenfrey-line,Sorgenfrey-line:];

coherence

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

;

:: deftheorem defines Sorgenfrey-plane TOPGEN_6:def 1 :

Sorgenfrey-plane = [:Sorgenfrey-line,Sorgenfrey-line:];

Sorgenfrey-plane = [:Sorgenfrey-line,Sorgenfrey-line:];

definition

coherence

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

end;

func real-anti-diagonal -> Subset of [:REAL,REAL:] equals :: TOPGEN_6:def 2

{ [x,y] where x, y is Real : y = - x } ;

correctness { [x,y] where x, y is Real : y = - x } ;

coherence

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

proof end;

:: deftheorem defines real-anti-diagonal TOPGEN_6:def 2 :

real-anti-diagonal = { [x,y] where x, y is Real : y = - x } ;

real-anti-diagonal = { [x,y] where x, y is Real : y = - x } ;

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;

Lm12: not Sorgenfrey-plane is Lindelof

proof end;

registration
end;

Lm13: not Sorgenfrey-plane is normal

proof end;