:: Some Properties of the {S}orgenfrey Line and the {S}orgenfrey Plane
:: by Adam J.J. St. Arnaud and Piotr Rudnicki
::
:: 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:
proof end;

registration
coherence 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:
by TOPGEN_3:def 2;

consider BB being Subset-Family of REAL such that
Lm6: 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 ;

Lm9:
proof end;

registration
coherence by Lm9;
end;

definition
correctness
coherence ;
;
end;

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

definition
func real-anti-diagonal -> Subset of 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
;
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
proof end;

theorem Th3: :: TOPGEN_6:3
proof end;

theorem Th4: :: TOPGEN_6:4
proof end;

by TOPGEN_3:def 2;

then Lm10:
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:
proof end;

registration
coherence by Lm12;
end;

registration
coherence by TOPGEN_5:59;
end;

registration
coherence ;
end;

Lm13:
proof end;

registration
coherence by Lm13;
end;