:: 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 b1 being SubSpace of R^1 holds b1 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;