:: 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-2016 Association of Mizar Users

environ

vocabularies HIDDEN, TOPGEN_6, NUMBERS, SUBSET_1, XXREAL_0, ORDINAL1, FUNCT_1, RELAT_1, XBOOLE_0, TARSKI, ZFMISC_1, CARD_3, CARD_1, COMPLEX1, ARYTM_3, RCOMP_1, ORDINAL2, STRUCT_0, ARYTM_1, REAL_1, TOPGEN_3, CANTOR_1, SETFAM_1, RAT_1, TOPS_1, TOPGEN_1, XXREAL_1, RLVECT_3, PRE_TOPC, CARD_5, TOPMETR, METRIZTS;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, SUBSET_1, SETFAM_1, FUNCT_1, RELSET_1, ORDINAL1, CARD_1, CARD_2, CARD_3, NUMBERS, XCMPLX_0, COMPLEX1, REAL_1, XREAL_0, RAT_1, RCOMP_1, DOMAIN_1, FUNCT_2, STRUCT_0, PRE_TOPC, BORSUK_1, TOPS_1, TOPS_2, CANTOR_1, TOPMETR, TOPGEN_1, TOPGEN_3, XXREAL_0, METRIZTS;
definitions TARSKI, XBOOLE_0, FUNCT_1, WELLORD2, PRE_TOPC, SUBSET_1, STRUCT_0, COMPTS_1, METRIZTS, SETFAM_1, TOPS_2;
theorems TARSKI, XBOOLE_0, XBOOLE_1, ZFMISC_1, FUNCT_1, TOPGEN_3, XREAL_1, XREAL_0, ABSVALUE, YELLOW_9, NUMBERS, CARD_5, SUBSET_1, TOPS_1, PRE_TOPC, TOPGEN_1, RAT_1, CARD_1, CARD_2, CARD_3, CARD_4, BORSUK_1, TOPS_2, FUNCT_2, TOPMETR, XXREAL_1, RELAT_1, CANTOR_1, SETFAM_1, FRECHET, XXREAL_0, XTUPLE_0, METRIZTS, BORSUK_5, TREAL_1, TOPS_4, TOPGEN_5;
schemes CLASSES1, FUNCT_2;
registrations SUBSET_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, RAT_1, CARD_1, MEMBERED, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TOPMETR, RELSET_1, METRIZTS, TOPGEN_4, CARD_3, TOPGEN_5, NAT_1;
constructors HIDDEN, WELLORD2, REAL_1, COMPLEX1, CARD_2, RCOMP_1, TOPS_1, TOPGEN_2, TOPGEN_1, TOPGEN_3, METRIZTS, TOPGEN_5, TOPGEN_4, ORDINAL1, PCOMPS_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
equalities TARSKI, XBOOLE_0, FUNCT_1, WELLORD2, PRE_TOPC, SUBSET_1, STRUCT_0, COMPTS_1, METRIZTS, SETFAM_1, TOPS_2;
expansions XXREAL_0, PRE_TOPC;


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;