:: 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-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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 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;
constructors WELLORD2, REAL_1, COMPLEX1, CARD_2, RCOMP_1, TOPS_1, TOPGEN_2,
TOPGEN_1, TOPGEN_3, METRIZTS, TOPGEN_5, TOPGEN_4, ORDINAL1, PCOMPS_1;
registrations SUBSET_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;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, FUNCT_1, WELLORD2, PRE_TOPC, COMPTS_1, METRIZTS,
SETFAM_1, TOPS_2;
equalities XBOOLE_0, SUBSET_1, STRUCT_0;
expansions XXREAL_0, PRE_TOPC;
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;
begin :: Preliminaries
:: The beginning of TOPS_2 belongs to SETFAM_1
Lm1:
for f being Function, x, y being set st x in f"{y} holds f.x = y
proof
let f be Function, x,y be set such that
A1: x in f"{y};
f.x in {y} by A1, FUNCT_1:def 7;
hence f.x = y by TARSKI:def 1;
end;
reserve T for TopSpace,
x, y, a, b, U, Ux, rx for set,
p, q for Rational,
F, G for Subset-Family of T,
Us, I for Subset-Family of Sorgenfrey-line;
:: This theorem is a slightly modified version of the proof of T_1 found
:: in topgen_5
Lm2: Sorgenfrey-line is T_2
proof
set T = Sorgenfrey-line;
consider B being Subset-Family of REAL such that
A1: the topology of Sorgenfrey-line = UniCl B and
A2: B = {[.x,q.[ where x,q is Real: x < q & q is rational} by TOPGEN_3:def 2;
let x,y be Point of T;
reconsider a = x, b = y as Element of REAL by TOPGEN_3:def 2;
A3: B c= the topology of T by A1,CANTOR_1:1;
assume
A4: x <> y;
per cases by A4,XXREAL_0:1;
suppose
A5: a < b;
consider q being Rational such that
A6: b < q and
q < b+1 by RAT_1:7, XREAL_1:29;
[.b,q.[ in B by A2,A6; then
A7: [.b,q.[ in the topology of T by A3;
consider w being Rational such that
A8: a < w and
A9: w < b by A5,RAT_1:7;
[.a,w.[ in B by A2,A8;
then [.a,w.[ in the topology of T by A3;
then reconsider U = [.a,w.[, V = [.b,q.[ as open Subset of T by A7,
PRE_TOPC:def 2;
take U,V;
A10: U /\ V = {}
proof
thus U /\ V c= {}
proof
let p be object;
assume A11: p in U /\ V; then
reconsider d = p as ExtReal;
d in [.a,w.[ & d in [.b,q.[ by XBOOLE_0:def 4, A11; then
d < w & b <= d by XXREAL_1:3;
hence p in {} by A9, XXREAL_0:2;
end;
thus {} c= U /\ V by XBOOLE_1:2;
end;
thus U is open & V is open;
thus thesis by A6, A8, XXREAL_1:3, A10, XBOOLE_0:def 7;
end;
suppose
A12: a > b;
consider q being Rational such that
A13: a < q and
q < a+1 by RAT_1:7, XREAL_1:29;
[.a,q.[ in B by A2,A13; then
A14: [.a,q.[ in the topology of T by A3;
consider w being Rational such that
A15: b < w and
A16: w < a by A12,RAT_1:7;
[.b,w.[ in B by A2,A15;
then [.b,w.[ in the topology of T by A3;
then reconsider V = [.b,w.[, U = [.a,q.[ as open Subset of T by A14,
PRE_TOPC:def 2;
take U,V;
A17: U /\ V = {}
proof
thus U /\ V c= {}
proof
let p be object;
assume A18: p in U /\ V; then
reconsider d = p as ExtReal;
d in [.a,q.[ & d in [.b,w.[ by XBOOLE_0:def 4, A18; then
d < w & a <= d by XXREAL_1:3;
hence p in {} by A16, XXREAL_0:2;
end;
thus {} c= U /\ V
proof
let p be object;
assume p in {};
hence thesis;
end;
end;
thus U is open & V is open;
thus thesis by A15,A13,XXREAL_1:3, A17, XBOOLE_0:def 7;
end;
end;
registration
cluster Sorgenfrey-line -> T_2;
coherence by Lm2;
end;
theorem Th1:
for x, a, b being Real st x in ].a,b.[
ex p,r being Rational st x in ].p,r.[ & ].p,r.[ c= ].a,b.[
proof
let x,a,b be Real such that
A1: x in ].a,b.[;
A2: x > a & x < b by XXREAL_1:4, A1;
consider p being Rational such that A3: p > a & x > p by A2, RAT_1:7;
consider r being Rational such that A4: x < r & r < b by A2, RAT_1:7;
take p,r;
thus x in ].p, r.[ by A3, A4, XXREAL_1:4;
thus ].p, r.[ c= ].a,b.[
proof
let y be object; assume
A5: y in ].p, r.[; then
reconsider y1 = y as Element of REAL;
y1 > p & y1 < r by XXREAL_1:4, A5; then
y1 > a & y1 < b by A3, A4, XXREAL_0:2;
hence y in ].a, b.[ by XXREAL_1:4;
end;
end;
Lm3:
for T being SubSpace of R^1 holds T is Lindelof
proof
let T be SubSpace of R^1;
let U be Subset-Family of T such that
A1: U is open and
A2: U is Cover of T;
per cases;
suppose A3: the carrier of T = {};
reconsider G = {} as Subset-Family of T by XBOOLE_1:2;
take G;
thus G c= U by XBOOLE_1:2;
thus G is Cover of T
proof
let x be object;
assume x in the carrier of T;
hence thesis by A3;
end;
thus G is countable;
end;
suppose A4: the carrier of T <> {};
A5: card [:RAT, RAT:] c= omega by CARD_3:def 14, CARD_4:7;
set Q = the set of all ].p,r.[ where p,r is Rational ;
defpred P[object,object] means
ex a, b being Rational st $1 = ].a,b.[ & $2 = [a,b];
A6: for x being object st x in Q
ex y being object st y in [:RAT,RAT:] & P[x,y]
proof
let x be object;
assume x in Q;
then consider a, b being Rational such that
A7: x = ].a,b.[;
take y = [a,b];
a in RAT & b in RAT by RAT_1:def 2;
hence y in [:RAT,RAT:] by ZFMISC_1:def 2;
thus P[x,y] by A7;
end;
consider h being Function of Q,[:RAT,RAT:] such that
A8: for x being object st x in Q holds P[x,h.x] from FUNCT_2:sch 1(A6);
A9: rng h c= [:RAT,RAT:];
A10: dom h = Q by FUNCT_2:def 1;
h is one-to-one
proof
let x1,x2 be object such that
A11: x1 in dom h and
A12: x2 in dom h and
A13: h.x1 = h.x2;
consider p1,r1 being Rational such that
A14: x1 = ].p1,r1.[ and A15: h.x1 = [p1,r1] by A8, A11;
consider p2,r2 being Rational such that
A16: x2 = ].p2,r2.[ and A17: h.x2 = [p2,r2] by A8, A12;
p1 = p2 & r1 = r2 by XTUPLE_0:1, A13, A15, A17;
hence x1 = x2 by A14, A16;
end;
then card Q c= card [:RAT,RAT:] by CARD_1:10, A9, A10;
then
A18: Q is countable by CARD_3:def 14, A5, XBOOLE_1:1;
defpred Pf[object,object] means
ex S being set st S = $2 & $1 in S & $2 in U;
A19: for x being object st x in the carrier of T
ex y being object st y in U & Pf[x,y]
proof
let x be object such that
A20: x in the carrier of T;
x in union U by SETFAM_1:def 11, A2, A20, TARSKI:def 3; then
consider Ux being set such that A21: x in Ux & Ux in U by TARSKI:def 4;
thus thesis by A21;
end;
consider f being Function of the carrier of T,U such that
A22: for x being object st x in the carrier of T holds
Pf[x,f.x] from FUNCT_2:sch 1(A19);
A23: U <> {}
proof
assume
A24: U = {};
the carrier of T c= union U by A2, SETFAM_1:def 11;
hence contradiction by A24, ZFMISC_1:2, A4;
end;
defpred Pf1[object,object] means
ex S being set st S = $2 & $2 in Q & $1 in S & (S /\ [#] T) c= f.$1;
A25: for x being object st x in the carrier of T
ex y being object st y in Q & Pf1[x,y]
proof
let x be object such that
A26: x in the carrier of T;
A27: Pf[x, f.x] by A22, A26;
reconsider Ux = f.x as Subset of T by A27;
Ux is open by A27, A1, TOPS_2:def 1; then
consider Vx being Subset of R^1 such that
A28: Vx in the topology of R^1 &
Ux = Vx /\ [#] T by PRE_TOPC:def 4;
reconsider x as Real by A26;
Ux c= Vx by A28, XBOOLE_1:17; then
consider r1 being Real such that
A29: r1 > 0 & ].(x-r1),(x+r1).[ c= Vx
by A27, FRECHET:8, A28, PRE_TOPC:def 2;
set a = x-r1, b = x+r1;
A30: x < x+r1 by XREAL_1:29, A29;
x > x-r1 by XREAL_1:44, A29;
then consider p1, p2 being Rational such that
A31: x in ].p1,p2.[ & ].p1,p2.[ c= ].a,b.[ by Th1, A30, XXREAL_1:4;
set q = ].p1,p2.[;
A32: q c= Vx by A29, A31, XBOOLE_1:1;
take q;
thus q in Q;
take q;
thus thesis by A28, A31, A32, XBOOLE_1:26;
end;
consider f1 being Function of the carrier of T, Q such that
A33: for x being object st x in the carrier of T
holds Pf1[x,f1.x] from FUNCT_2:sch 1(A25);
deffunc F(object) = f.the Element of f1"{$1};
].2,1.[ in Q; then
A34: dom f1 = the carrier of T by FUNCT_2:def 1;
A35: for x being object st x in rng f1 holds F(x) in U
proof
let x be object such that
A36: x in rng f1;
f1"{x} <> {} by A36, FUNCT_1:72; then
A37: the Element of f1"{x} in f1"{x};
the Element of f1"{x} in the carrier of T by A37; then
the Element of f1"{x} in dom f by A23, FUNCT_2:def 1; then
F(x) in rng f by FUNCT_1:3;
hence thesis;
end;
consider g being Function of rng f1, U such that
A38: for q being object st q in rng f1 holds g.q = F(q)
from FUNCT_2:sch 2(A35);
A39: card rng f1 c= omega by CARD_3:def 14, A18;
A40: dom g = rng f1 by FUNCT_2:def 1, A23; then
A41: card rng g c= card rng f1 by CARD_1:12;
reconsider G = rng g as Subset-Family of T by TOPS_2:2;
take G;
thus G c= U;
thus G is Cover of T
proof
let x be object;
assume A42: x in the carrier of T;
set q = f1.x;
A43: [x,q] in f1 by FUNCT_1:def 2, A42, A34;
A44: q in {q} by TARSKI:def 1;
A45: q in rng f1 by FUNCT_1:3, A34, A42;
A46: Pf1[x,f1.x] by A33, A42;
set y = the Element of f1"{q};
A47: f1"{q} <> {} by A45, A43, A44, RELAT_1:131; then
A48: x in f1.y by A46, Lm1;
A49: f.y = g.q by A38, FUNCT_1:3, A34, A42;
y in f1"{q} by A47; then
A50: Pf1[y,f1.y] by A33;
A51: x in f1.y /\ [#] T by A42, A48, XBOOLE_0:def 4;
g.q in rng g by FUNCT_1:3, A45, A40;
hence x in union G by A51, TARSKI:def 4, A49, A50;
end;
thus G is countable by A41, CARD_3:def 14, A39, XBOOLE_1:1;
end;
end;
registration
cluster -> Lindelof for SubSpace of R^1;
coherence by Lm3;
end;
Lm4:
for p,r being Real st r > p holds ex q being Rational st q in [.p,r.[
proof
let p,r be Real such that
A1: r > p;
consider q being Rational such that
A2: p < q & q < r by A1, RAT_1:7;
thus thesis by A2, XXREAL_1:3;
end;
:: LEM3 through LEM6 are from from TOPGEN_3
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,def 2,TOPS_2:64;
Lm9:
Sorgenfrey-line is Lindelof
proof
set S = Sorgenfrey-line;
let U be Subset-Family of S such that
A1: U is open and
A2: U is Cover of S;
A3: U <> {}
proof
assume
A4: U = {};
the carrier of S c= union U by SETFAM_1:def 11, A2;
hence contradiction by A4, ZFMISC_1:2;
end;
set V = { Int u where u is Subset of R^1 : u in U};
set W = union V;
reconsider K = [#] S \ W as set;
V is non empty Subset-Family of R^1
proof
consider u being object such that
A5: u in U by XBOOLE_0:def 1, A3;
reconsider u as Subset of R^1 by TOPGEN_3:def 2, TOPMETR:17, A5;
set v = Int u;
A6: V c= bool [#] R^1
proof
let x be object such that
A7: x in V;
consider u being Subset of R^1 such that
A8: Int u = x and u in U by A7;
thus x in bool [#] R^1 by A8;
end;
v in V by A5;
hence thesis by A6;
end;
then reconsider V as non empty Subset-Family of R^1;
W c= [#] R^1
proof
let x be object;
assume x in W; then
consider v being set such that
A9: x in v and
A10: v in V by TARSKI:def 4;
thus x in [#] R^1 by A9, A10;
end;
then
reconsider W as Subset of R^1;
defpred Ph[object, object] means
ex y being Subset of R^1 st $2 = y & y in U & $1 = Int y;
A11: for x being object st x in V ex y being object st y in U & Ph[x,y]
proof
let x be object such that
A12: x in V;
consider u being Subset of R^1 such that
A13: x = Int u and
A14: u in U by A12;
take u;
thus u in U by A14;
thus Ph[x,u] by A13, A14;
end;
consider h being Function of V,U such that
A15: for x being object st x in V holds Ph[x,h.x] from FUNCT_2:sch 1(A11);
A16: for x being Element of V, hx being Subset of R^1 st hx = h.x holds
x = Int hx
proof
let x be Element of V, hx be Subset of R^1 such that
A17: hx = h.x;
consider y being Subset of R^1 such that
A18: h.x = y and
y in U and
A19: x = Int y by A15;
thus x = Int hx by A18, A19, A17;
end;
reconsider T = (R^1)|W as SubSpace of R^1;
V c= bool [#] T
proof
let x be object such that
A20: x in V;
reconsider xx=x as set by TARSKI:1;
xx c= W
proof
let y be object;
thus thesis by TARSKI:def 4, A20;
end;
then xx c= [#] T by PRE_TOPC:def 5;
hence x in bool [#] T;
end;
then reconsider V1 = V as non empty Subset-Family of T;
A21: V1 is open
proof
let v be Subset of T such that
A22: v in V1;
consider u being Subset of R^1 such that
A23: v = Int u and
u in U by A22;
A24: v in the topology of R^1 by A23, PRE_TOPC:def 2;
v /\ [#] T = v
proof
thus v /\ [#] T c= v by XBOOLE_1:17;
thus v c= v /\ [#] T by XBOOLE_1:19;
end;
hence v is open by A24,PRE_TOPC:def 4;
end;
A25: the carrier of T c= union V
proof
let x be object;
assume x in the carrier of T;
then x in [#] T;
hence x in union V by PRE_TOPC:def 5;
end;
consider B being Subset-Family of T such that
A26: B c= V and
A27: B is Cover of T and
A28: B is countable by METRIZTS:def 2, A21, A25,SETFAM_1:def 11;
deffunc Ff(object) = h.$1;
A29: for x being object st x in B holds Ff(x) in U
proof
let x be object;
assume x in B;
then h.x in rng h by A3, FUNCT_2:4, A26;
hence h.x in U;
end;
consider f being Function of B,U such that
A30: for x being object st x in B holds f.x = Ff(x) from FUNCT_2:sch 2(A29);
reconsider Y = rng f as Subset-Family of S by TOPS_2:2;
A31: Y is Cover of W
proof
let x be object; assume
A32: x in W;
B is Cover of [#] T by A27;
then B is Cover of W by PRE_TOPC:def 5;
then x in union B by A32, SETFAM_1:def 11, TARSKI:def 3;
then consider b being set such that
A33: x in b & b in B by TARSKI:def 4;
B = dom f by FUNCT_2:def 1, A3; then
A34: f.b in Y by FUNCT_1:3, A33;
b c= f.b
proof
let x be object such that
A35: x in b;
A36: f.b = h.b by A30, A33;
reconsider b1 = b as Element of (V qua set) by A26, A33;
h.b1 in U by A3;
then reconsider hb = h.b1 as Subset of R^1
by TOPGEN_3:def 2, TOPMETR:17;
A37: b1 = Int hb by A16;
b1 c= hb by A37, TOPS_1:16;
hence x in f.b by A36, A35;
end;
hence x in union Y by A34, TARSKI:def 4, A33;
end;
A38: card B c= omega by CARD_3:def 14, A28;
dom f = B by FUNCT_2:def 1, A3; then
card rng f c= card B by CARD_1:12;
then
A39: Y is countable by CARD_3:def 14,A38, XBOOLE_1:1;
:: Now, show K has countable subcover (Z)
defpred Pg[object, object] means ex S being set st S = $2 & $1 in S;
A40: for x being object st x in K ex y being object st y in U & Pg[x,y]
proof
let x be object;
assume x in K;
then x in union U by SETFAM_1:def 11, A2, TARSKI:def 3;
then consider Ux being set such that
A41: x in Ux and
A42: Ux in U by TARSKI:def 4;
take Ux;
thus Ux in U by A42;
thus Pg[x,Ux] by A41;
end;
consider g being Function of K, U such that
A43: for x being object st x in K holds Pg[x,g.x] from FUNCT_2: sch 1(A40);
set Q = { [.p,r.[ where p, r is Real : r > p};
defpred Pk[object, object] means
ex S being set st S = $2 &
S c= g.$1 & ex x, rx being Real st $1 = x & $2 = [.x,rx.[;
A44: for x being object st x in K ex y being object st y in Q & Pk[x,y]
proof
let x be object such that
A45: x in K;
g.x in U by FUNCT_2:5, A45, A3; then
reconsider gx = g.x as open Subset of S by A1, TOPS_2:def 1;
reconsider x1 = x as Point of S by A45;
Pg[x,g.x] by A43, A45;
then consider a being Subset of S such that
A46: a in BB and
A47: x1 in a and
A48: a c= gx by YELLOW_9:31, Lm8;
consider p,r being Real such that
A49: a = [.p, r.[ and r > p and r is rational by Lm7, A46;
reconsider x2 = x1 as Real by A47, A49;
A50: p <= x2 & x2 < r by A47, A49, XXREAL_1:3;
set y = [.x2,r.[;
take y;
A51: y c= a
proof
let z be object such that
A52: z in y;
reconsider z1 = z as Real by A52;
x2 <= z1 & z1 < r by A52, XXREAL_1:3; then
p <= z1 & z1 < r by A50, XXREAL_0:2;
hence z in a by A49, XXREAL_1:3;
end;
thus y in Q by A50;
thus Pk[x,y] by A51, A48, XBOOLE_1:1;
end;
consider k being Function of K, Q such that
A53: for x being object st x in K holds Pk[x,k.x] from FUNCT_2:sch 1(A44);
defpred Pj[object, object] means
ex S being set st S = $1 & $2 in S;
A54: for x being object st x in rng k
ex y being object st y in RAT & Pj[x,y]
proof
let x be object such that
A55: x in rng k;
x in Q by A55; then
consider p,r being Real such that
A56: x = [.p,r.[ and
A57: r > p;
reconsider xx=x as set by TARSKI:1;
consider y being Rational such that
A58: y in xx by A56, A57, Lm4;
take y;
thus y in RAT by RAT_1:def 2;
take xx;
thus thesis by A58;
end;
consider j being Function of rng k, RAT such that
A59: for x being object st x in rng k holds Pj[x,j.x] from FUNCT_2: sch 1(A54)
;
A60: for x,y being Element of S st x in K & y in K & x <> y holds k.x misses k.
y
proof
let x,y be Element of S such that
A61: x in K and
A62: y in K and
A63: x <> y;
A64: Pk[x,k.x] & Pk[y,k.y] by A53, A61, A62;
A65: g.x in U & g.y in U by A3, A61, A62, FUNCT_2:5;
thus k.x /\ k.y = {}
proof
assume not k.x /\ k.y = {}; then
consider l being object such that
A66: l in k.x /\ k.y by XBOOLE_0:7;
A67: l in k.x & l in k.y by XBOOLE_0:def 4, A66;
Pk[x,k.x] by A53, A61;
then consider x1, rx being Real such that
A68: x = x1 and
A69: k.x = [.x1,rx.[;
Pk[y,k.y] by A53, A62;
then consider y1, ry being Real such that
A70: y = y1 and
A71: k.y = [.y1, ry.[;
reconsider l as Real by A69, A66;
A72: x1 <= l & l < rx by A69, A67, XXREAL_1:3;
A73: y1 <= l & l < ry by A71, A67, XXREAL_1:3;
per cases by A63, XXREAL_0:1, A68, A70;
suppose
A74: x1 < y1;
y1 < rx by A72, A73, XXREAL_0:2; then
A75: y1 in ].x1,rx.[ by XXREAL_1:4, A74;
reconsider Y = ].x1,rx.[ as Subset of R^1 by TOPMETR:17;
Y c= k.x by XXREAL_1:22, A69; then
A76: Y c= g.x by A64, XBOOLE_1:1;
reconsider gx = g.x as Subset of R^1
by TOPGEN_3:def 2, TOPMETR:17, A65;
A77: y in Int gx by A76, BORSUK_5:40, A70, A75, TOPS_1:22;
Int gx in V by A65; then
y in union V by A77, TARSKI:def 4;
hence contradiction by A62, XBOOLE_0:def 5;
end;
suppose
A78: x1 > y1;
x1 < ry by A72, A73, XXREAL_0:2; then
A79: x1 in ].y1,ry.[ by XXREAL_1:4, A78;
reconsider X = ].y1,ry.[ as Subset of R^1 by TOPMETR:17;
X c= k.y by XXREAL_1:22, A71; then
A80: X c= g.y by A64, XBOOLE_1:1;
reconsider gy = g.y as Subset of R^1
by A65, TOPGEN_3:def 2, TOPMETR:17;
A81: x in Int gy by A80, BORSUK_5:40, A68, A79, TOPS_1:22;
Int gy in V by A65; then
x in union V by A81, TARSKI:def 4;
hence contradiction by A61, XBOOLE_0:def 5;
end;
end;
end;
A82: rng j c= RAT;
A83: dom j = rng k by FUNCT_2:def 1;
A84: j is one-to-one
proof
let x1, x2 be object such that
A85: x1 in dom j and
A86: x2 in dom j and
A87: j.x1 = j.x2;
reconsider x1,x2 as set by TARSKI:1;
consider y1 being object such that A88: y1 in dom k &
x1 = k.y1 by FUNCT_1:def 3, A85;
consider y2 being object such that A89: y2 in dom k &
x2 = k.y2 by FUNCT_1:def 3, A86;
A90: y1 in K & y2 in K by A88, A89;
Pj[x1,j.x1] & Pj[x2,j.x2] by A85, A86, A59;
then k.y1 /\ k.y2 <> {} by A88, A89, XBOOLE_0:def 4, A87;
hence thesis by A88, A89, A60, A90, XBOOLE_0:def 7;
end;
A91: card rng k c= omega by TOPGEN_3:17,CARD_1:10, A82, A83, A84;
A92: [.1,2.[ in Q; then
A93: dom k = K by FUNCT_2:def 1;
A94: k is one-to-one
proof
let x1, x2 be object such that
A95: x1 in dom k and
A96: x2 in dom k and
A97: k.x1 = k.x2;
A98: x1 in K & x2 in K by A95, A96;
k.x1 in rng k & k.x2 in rng k by A92, A95, A96, FUNCT_2:4; then
A99: k.x1 in Q & k.x2 in Q;
consider p1,r1 being Real such that
A100: k.x1 = [.p1,r1.[ and
A101: r1 > p1 by A99;
consider q being Rational such that
A102: q in k.x1 by A100, A101, Lm4;
q in k.x1 /\ k.x2 by A102, A97;
hence x1 = x2 by A60, XBOOLE_0:def 7, A98;
end;
A103: card K c= card rng k by CARD_1:10, A93, A94;
A104: card K c= omega by A103, A91, XBOOLE_1:1;
dom g = K by FUNCT_2:def 1, A3; then
card rng g c= card K by CARD_1:12; then
A105: rng g is countable by CARD_3:def 14,A104,XBOOLE_1:1;
reconsider Z = rng g as Subset-Family of S by TOPS_2:2;
A106: Z is Cover of K
proof
let x be object;
assume
A107: x in K;
then
A108: Pg[x,g.x] by A43;
x in dom g by A107, FUNCT_2:def 1, A3; then
g.x in Z by FUNCT_1:def 3;
hence x in union Z by TARSKI:def 4, A108;
end;
W c= [#] S
proof
let x be object;
assume x in W; then
x in [#] R^1;
hence x in [#] S by TOPMETR:17, TOPGEN_3:def 2;
end; then
A109: W \/ K = [#] S by XBOOLE_1:45;
A110: Z \/ Y is Cover of [#] S
proof
let x be object;
assume x in [#] S; then
x in W or x in K by XBOOLE_0:def 3, A109; then
x in union Y or x in union Z by A31, A106, TARSKI:def 3,
SETFAM_1:def 11; then
x in (union Y) \/ (union Z) by XBOOLE_0:def 3;
hence x in union (Z \/ Y) by ZFMISC_1:78;
end;
reconsider G = Z \/ Y as Subset-Family of S;
take G;
thus G c= U by XBOOLE_1:8;
thus G is Cover of S by A110;
thus G is countable by CARD_2:85, A105, A39;
end;
registration
cluster Sorgenfrey-line -> Lindelof;
coherence by Lm9;
end;
definition
func Sorgenfrey-plane -> non empty strict TopSpace equals
[:Sorgenfrey-line, Sorgenfrey-line:];
correctness;
end;
definition :: ? how to do it better
func real-anti-diagonal -> Subset of [:REAL,REAL:] equals
{[x,y] where x,y is Real : y = -x};
correctness proof
set L = {[x,y] where x,y is Real : y = -x};
L c= [:REAL, REAL:]
proof
let z be object;
assume z in L;
then consider x,y being Real such that
A1: z = [x,y] and y = -x;
x in REAL & y in REAL by XREAL_0:def 1;
hence z in [:REAL, REAL:] by A1,ZFMISC_1:87;
end;
hence L is Subset of [:REAL, REAL:];
end;
end;
theorem Th2:
[:RAT,RAT:] is dense Subset of Sorgenfrey-plane
proof
[:RAT, RAT:] c= [#] Sorgenfrey-plane
proof
let z be object;
assume z in [:RAT, RAT:]; then
consider x,y being object such that
A1: x in RAT & y in RAT and
A2: z = [x,y] by ZFMISC_1:def 2;
x in REAL & y in REAL by A1, NUMBERS:12; then
x in [#] Sorgenfrey-line &
y in [#] Sorgenfrey-line by TOPGEN_3:def 2; then
z in [:[#] Sorgenfrey-line, [#] Sorgenfrey-line:]
by A2, ZFMISC_1:def 2;
hence z in [#] Sorgenfrey-plane;
end;
then reconsider C = [:RAT, RAT:] as Subset of Sorgenfrey-plane;
for A being Subset of Sorgenfrey-plane st A <> {} & A is open
holds A meets C
proof
let A be Subset of Sorgenfrey-plane such that
A3: A <> {} and
A4: A is open;
consider B being Subset-Family of Sorgenfrey-plane such that
A5: A = union B and
A6: (for e being set st e in B holds ex X1 being Subset of Sorgenfrey-line,
Y1 being Subset of Sorgenfrey-line st (e = [:X1,Y1:] & X1 is open &
Y1 is open)) by BORSUK_1:5, A4;
now
assume A7: for e being set st e in B holds e = {};
union B c= {}
proof
let z be object;
assume z in union B; then
consider y being set such that
A8: z in y & y in B by TARSKI:def 4;
thus z in {} by A8, A7;
end;
hence contradiction by A5, A3;
end;
then
consider e being set such that
A9: e in B & e <> {};
consider X1,Y1 being Subset of Sorgenfrey-line such that
A10: e = [:X1,Y1:] and
A11: X1 is open & Y1 is open by A6, A9;
A12: X1 <> {} & Y1 <> {} by ZFMISC_1:90, A9, A10;
consider x1 being object such that
A13: x1 in X1 by A12, XBOOLE_0:7;
consider y1 being object such that
A14: y1 in Y1 by A12, XBOOLE_0:7;
consider ax being Subset of Sorgenfrey-line such that
A15: ax in BB and
x1 in ax and
A16: ax c= X1 by YELLOW_9:31, A11, A13, Lm8;
consider ay being Subset of Sorgenfrey-line such that
A17: ay in BB and
y1 in ay and
A18: ay c= Y1 by YELLOW_9:31, A11, A14, Lm8;
consider px,qx being Real such that
A19: ax = [.px,qx.[ and
A20: px < qx & qx is rational by A15, Lm7;
consider py,qy being Real such that
A21: ay = [.py,qy.[ and
A22: py < qy & qy is rational by A17, Lm7;
consider rx being Rational such that
A23: px < rx & rx < qx by RAT_1:7, A20;
A24: rx in ax by A23, XXREAL_1:3, A19;
consider ry being Rational such that
A25: py < ry & ry < qy by RAT_1:7, A22;
A26: ry in ay by A25, XXREAL_1:3, A21;
rx in RAT & ry in RAT by RAT_1:def 2; then
A27: [rx,ry] in C by ZFMISC_1:def 2;
[rx,ry] in [:X1,Y1:] by A24, A26, A16, A18, ZFMISC_1:def 2; then
A28: [rx,ry] in A by A5, A9, A10, TARSKI:def 4;
thus A meets C by A27, A28, XBOOLE_0:3;
end;
hence [:RAT, RAT:] is dense Subset of Sorgenfrey-plane by TOPS_1:45;
end;
theorem Th3:
card real-anti-diagonal = continuum
proof
REAL, real-anti-diagonal are_equipotent
proof
defpred P[object, object] means
ex x being Real st $1 = x & $2 = [x,-x];
A1: for r being object st r in REAL
ex a being object st a in real-anti-diagonal & P[r,a]
proof
let r be object;
assume r in REAL;
then reconsider r as Real;
set a = [r,-r];
a in real-anti-diagonal;
hence thesis;
end;
consider Z being Function of REAL, real-anti-diagonal such that
A2: for r being object st r in REAL holds P[r,Z.r] from FUNCT_2: sch 1(A1);
take Z;
A3: real-anti-diagonal <> {}
proof
reconsider x = 1, y = -1 as Element of REAL by XREAL_0:def 1;
set z = [x,y];
z in real-anti-diagonal;
hence real-anti-diagonal <> {};
end;
thus Z is one-to-one
proof
let r1,r2 be object such that
A4: r1 in dom Z & r2 in dom Z and
A5: Z.r1 = Z.r2;
consider x1 being Real such that
A6: r1 = x1 & Z.r1 = [x1,-x1] by A2, A4;
consider x2 being Real such that
A7: r2 = x2 & Z.r2 = [x2,-x2] by A2, A4;
thus r1 = r2 by A6, A7, A5, XTUPLE_0:1;
end;
thus dom Z = REAL by A3, FUNCT_2:def 1;
thus rng Z = real-anti-diagonal
proof
thus rng Z c= real-anti-diagonal;
thus real-anti-diagonal c= rng Z
proof
let z be object;
assume z in real-anti-diagonal; then
consider x,y being Real such that
A8: z = [x,y] and
A9: y = -x;
consider x1 being Real such that
A10: x = x1 & Z.x = [x1,-x1] by A2,XREAL_0:def 1;
thus z in rng Z by A10, A8, A9, FUNCT_2:4, A3,XREAL_0:def 1;
end;
end;
end;
hence card real-anti-diagonal = continuum by TOPGEN_3:def 4,CARD_1:5;
end;
theorem Th4:
real-anti-diagonal is closed Subset of Sorgenfrey-plane
proof
set L = real-anti-diagonal;
set S2 = Sorgenfrey-plane;
A1: L c= [#] S2
proof
let z be object;
assume z in L;
then consider x,y being Real such that
A2: z = [x,y] and y = -x;
x in REAL & y in REAL by XREAL_0:def 1; then
x in [#] Sorgenfrey-line & y in [#] Sorgenfrey-line by TOPGEN_3:def 2;
then [x,y] in [:[#] Sorgenfrey-line, [#] Sorgenfrey-line:]
by ZFMISC_1:def 2;
hence z in [#] Sorgenfrey-plane by A2;
end;
reconsider L = real-anti-diagonal as Subset of Sorgenfrey-plane by A1;
defpred Pf[object, object] means
ex x,y being Real st $1 = [x,y] & $2 = x+y;
A3: for z being object st z in the carrier of S2
ex u being object st u in the carrier of R^1 & Pf[z,u]
proof
let z be object;
assume z in the carrier of S2;
then z in [:the carrier of Sorgenfrey-line,
the carrier of Sorgenfrey-line:] by BORSUK_1:def 2;
then consider x,y being object such that
A4: x in the carrier of Sorgenfrey-line and
A5: y in the carrier of Sorgenfrey-line and
A6: z = [x,y] by ZFMISC_1:def 2;
reconsider x as Element of REAL by A4, TOPGEN_3:def 2;
reconsider y as Element of REAL by A5, TOPGEN_3:def 2;
set u = x+y;
u in the carrier of R^1 by TOPMETR:17;
hence thesis by A6;
end;
consider f being Function of S2, R^1 such that
A7: for z being object st z in the carrier of S2 holds Pf[z,f.z]
from FUNCT_2:sch 1(A3);
A8: for x,y being Element of REAL st [x,y] in the carrier of S2
holds f.([x,y]) = x + y
proof
let x,y be Element of REAL such that
A9: [x,y] in the carrier of S2;
consider x1,y1 being Real such that
A10: [x,y] = [x1,y1] & f.([x,y]) = x1+y1 by A9, A7;
x = x1 & y = y1 by A10, XTUPLE_0:1;
hence thesis by A10;
end;
for p being Point of S2, r being positive Real
ex W being open Subset of S2 st p in W & f.:W c= ].f.p-r,f.p+r.[
proof
let p be Point of S2;
let r be positive Real;
p in [#] S2; then
p in [:the carrier of Sorgenfrey-line, the carrier of Sorgenfrey-line:]
by BORSUK_1:def 2;
then consider x,y being object such that
A11: x in the carrier of Sorgenfrey-line and
A12: y in the carrier of Sorgenfrey-line and
A13: p = [x,y] by ZFMISC_1:def 2;
reconsider x as Element of REAL by A11, TOPGEN_3:def 2;
reconsider y as Element of REAL by A12, TOPGEN_3:def 2;
A14: f.p = x+y by A13, A8;
set U = ].f.p-r,f.p+r.[;
set W = [:[.x,x+(r/2).[ , [.y,y+(r/2).[:];
A15: W c= [#] S2
proof
let z be object;
assume z in W; then
consider u,v being object such that
A16: u in [.x,x+(r/2).[ & v in [.y,y+(r/2).[ and
A17: z = [u,v] by ZFMISC_1:def 2;
reconsider u,v as Element of [#] Sorgenfrey-line
by A16, TOPGEN_3:def 2;
u in [#] Sorgenfrey-line & v in [#] Sorgenfrey-line; then
z in [:[#] Sorgenfrey-line, [#] Sorgenfrey-line:] by
A17, ZFMISC_1:def 2;
hence z in [#] S2;
end;
reconsider W as Subset of S2 by A15;
reconsider X = [.x,x+(r/2).[ as Subset of Sorgenfrey-line by
TOPGEN_3:def 2;
reconsider Y = [.y,y+(r/2).[ as Subset of Sorgenfrey-line by
TOPGEN_3:def 2;
X is open & Y is open by TOPGEN_3:11; then
A18: W is open by BORSUK_1:6;
r/2 is positive;
then x < x+(r/2) & y < y+(r/2) by XREAL_1:29; then
x in [.x,x+(r/2).[ & y in [.y,y+(r/2).[ by XXREAL_1:3; then
A19: p in W by A13, ZFMISC_1:def 2;
f.:W c= U
proof
let z be object;
assume z in f.:W;
then consider w being object such that
w in dom f and
A20: w in W and
A21: z = f.w by FUNCT_1:def 6;
consider x1,y1 being object such that
A22: x1 in X & y1 in Y and
A23: w = [x1,y1] by A20, ZFMISC_1:def 2;
reconsider x1 as Element of REAL by A22;
reconsider y1 as Element of REAL by A22;
A24: x <= x1 & x1 < x+(r/2) & y <= y1 & y1 < y+(r/2) by A22, XXREAL_1:3;
A25: x+y <= x1+y1 by XREAL_1:7, A24;
x+y-r < x+y by XREAL_1:44,XXREAL_0:def 6; then
A26: x+y-r < x1+y1 by A25, XXREAL_0:2;
x1+y1 < (x+(r/2))+(y+(r/2)) by XREAL_1:8, A24; then
x1+y1 in U by A26, A14, XXREAL_1:4;
hence z in U by A23, A8, A20, A21;
end;
hence thesis by A19, A18;
end; then
A27: f is continuous by TOPS_4:21;
reconsider zz = 0 as Element of REAL by XREAL_0:def 1;
reconsider k = {zz} as Subset of R^1 by TOPMETR:17;
reconsider k1 = [.zz, zz.] as Subset of R^1 by TOPMETR:17;
A28: k = k1 by XXREAL_1:17;
L = f"k
proof
hereby
let z be object; assume
A29: z in L; then
consider x,y being Real such that
A30: z = [x,y] and
A31: y = -x;
reconsider x,y as Element of REAL by XREAL_0:def 1;
f.z = x + y by A8, A30, A29; then
f.z in k by TARSKI:def 1, A31;
hence z in f"k by FUNCT_2:38, A29;
end;
let z be object; assume z in f"k; then
A32: z in [#] S2 & f.z in k by FUNCT_2:38; then
A33: z in [:the carrier of Sorgenfrey-line, the carrier of Sorgenfrey-line
:]
by BORSUK_1:def 2;
consider x,y being object such that
A34: x in the carrier of Sorgenfrey-line and
A35: y in the carrier of Sorgenfrey-line and
A36: z = [x,y] by A33, ZFMISC_1:def 2;
reconsider x1 = x as Element of REAL by A34, TOPGEN_3:def 2;
reconsider y1 = y as Element of REAL by A35, TOPGEN_3:def 2;
f.z = x1 + y1 by A8, A36, A32; then
(x1 + y1) = 0 by A32, TARSKI:def 1;
then -x1 = y1;
hence z in L by A36;
end;
hence thesis by A28, A27, TREAL_1:1;
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
let x,y be Real;
assume [x,y] in real-anti-diagonal;
then consider x1,y1 being Real such that
A1: [x,y] = [x1,y1] and
A2: y1 = -x1;
x = x1 & y = y1 by A1, XTUPLE_0:1;
hence y = -x by A2;
end;
theorem Th5:
for A being Subset of Sorgenfrey-plane st A = real-anti-diagonal
holds Der A is empty
proof
let A be Subset of Sorgenfrey-plane such that
A1: A = real-anti-diagonal;
assume Der A is not empty; then
consider a being object such that
A2: a in Der A by XBOOLE_0:7;
a is_an_accumulation_point_of A by TOPGEN_1:def 3, A2; then
A3: a in Cl(A\{a}) by TOPGEN_1:def 2;
consider x,y being object such that
A4: x in REAL & y in REAL and
A5: a = [x,y] by ZFMISC_1:def 2, Lm10, A2;
reconsider x,y as Real by A4;
per cases;
suppose
A6: y >= -x;
set Gx = [.x,x+1.[;
set Gy = [.y,y+1.[;
reconsider Gx,Gy as Subset of Sorgenfrey-line by TOPGEN_3:def 2;
set G = [:Gx,Gy:];
reconsider G as Subset of Sorgenfrey-plane;
Gx is open & Gy is open by TOPGEN_3:11; then
A7: G is open by BORSUK_1:6;
x <= x & x < x+1 by XREAL_1:29; then
A8: x in Gx by XXREAL_1:3;
y <= y & y < y+1 by XREAL_1:29; then
y in Gy by XXREAL_1:3; then
A9: a in G by A5, A8, ZFMISC_1:def 2;
now
assume G /\ (A\{a}) <> {};
then consider z being object such that
A10: z in G /\ (A\{a}) by XBOOLE_0:def 1;
z in G & z in (A\{a}) by XBOOLE_0:def 4, A10; then
A11: z in G & z in A & not z in {a} by XBOOLE_0:def 5;
consider xz,yz being object such that
A12: xz in [.x,x+1.[ & yz in [.y,y+1.[ and
A13: z = [xz,yz] by ZFMISC_1:def 2, A11;
reconsider xz as Real by A12;
reconsider yz as Real by A12;
A14: x <= xz & y<= yz by A12, XXREAL_1:3;
A15: -x >= -xz & y <= -xz by A14, Lm11, A1, A11, A13, XREAL_1:24;
A16: -x >= y by XXREAL_0:2, A15;
A17: -x = y by A16, A6, XXREAL_0:1; then
A18: -x <= yz by A12, XXREAL_1:3;
A19: -x <= -xz by Lm11, A1, A11, A13, A18;
A20: x >= xz by XREAL_1:24, A19;
A21: x = xz by A20, A14, XXREAL_0:1; then
y = yz by A17, Lm11, A1, A11, A13;
hence contradiction by A11, TARSKI:def 1, A13, A5, A21;
end; then
G misses (A\{a}) by XBOOLE_0:def 7;
hence contradiction by A7, A9, A3, PRE_TOPC:def 7;
end;
suppose
A22: y < -x;
set Gx = [.x,x+(|.x+y.|/2).[;
set Gy = [.y,y+(|.x+y.|/2).[;
reconsider Gx, Gy as Subset of Sorgenfrey-line by TOPGEN_3:def 2;
reconsider G = [:Gx,Gy:] as Subset of Sorgenfrey-plane;
Gx is open & Gy is open by TOPGEN_3:11; then
A23: G is open by BORSUK_1:6;
A24: y + x < 0 by A22, XREAL_1:61;
A25: |.x+y.| = -(x+y) by ABSVALUE:def 1,A22, XREAL_1:61;
A26: |.x+y.| > 0 by A24, A25,XREAL_1:58;
then x < x+(|.x+y.|/2) by XREAL_1:29,139; then
A27: x in Gx by XXREAL_1:3;
y < y+(|.x+y.|/2) by XREAL_1:29, A26, XREAL_1:139; then
y in Gy by XXREAL_1:3; then
A28: a in G by A5, A27, ZFMISC_1:def 2;
now
assume G /\ (A\{a}) <> {};
then consider z being object such that
A29: z in G /\ (A\{a}) by XBOOLE_0:def 1;
z in G & z in (A\{a}) by A29, XBOOLE_0:def 4; then
A30: z in G & z in A & not z in {a} by XBOOLE_0:def 5;
consider xz,yz being object such that
A31: xz in [.x,x+(|.x+y.|/2).[ & yz in [.y,y+(|.x+y.|/2).[ and
A32: z = [xz,yz] by ZFMISC_1:def 2, A30;
reconsider xz,yz as Real by A31;
A33: yz = -xz by Lm11, A1, A30, A32;
A34: xz < x+(|.x+y.|/2) & yz < y+(|.x+y.|/2) by A31, XXREAL_1:3;
xz + yz < (x+(|.x+y.|/2)) + (y+(|.x+y.|/2)) by A34, XREAL_1:8;
hence contradiction by A33, A25;
end; then
G misses (A\{a}) by XBOOLE_0:def 7;
hence contradiction by A23, A28, A3, PRE_TOPC:def 7;
end;
end;
theorem Th6: :: following TOPGEN_5:42
for A being Subset of real-anti-diagonal
holds A is closed Subset of Sorgenfrey-plane
proof
reconsider B = real-anti-diagonal as closed Subset of
Sorgenfrey-plane by Th4;
let A be Subset of real-anti-diagonal;
A c= B;
then reconsider A as Subset of Sorgenfrey-plane by XBOOLE_1:1;
Der A c= Der B by TOPGEN_1:30;
then Der A c= {} by Th5;
then Der A = {};
then Cl A = A \/ {} by TOPGEN_1:29;
hence thesis;
end;
Lm12:
Sorgenfrey-plane is not Lindelof
proof
set S2 = Sorgenfrey-plane;
reconsider L = real-anti-diagonal as Subset of S2 by Lm10;
reconsider T = S2|L as SubSpace of S2;
A1: for v being Subset of T, z being set st v = {z} & z in L holds
v is open
proof
let v be Subset of T, z be set such that
A2: v = {z} and
A3: z in L;
consider x, y being Real such that
A4: z = [x,y] and
A5: y = -x by A3;
set Ux = [.x, x+1.[;
reconsider Ux as open Subset of Sorgenfrey-line by TOPGEN_3:11;
set Uy = [.y, y+1.[;
reconsider Uy as open Subset of Sorgenfrey-line by TOPGEN_3:11;
reconsider U2 = [:Ux,Uy:] as Subset of S2;
A6: U2 in the topology of S2 by BORSUK_1:6, PRE_TOPC:def 2;
A7: U2 /\ L = v
proof
hereby
let p be object; assume p in U2 /\ L; then
A8: p in U2 & p in L by XBOOLE_0:def 4; then
consider p1, p2 being object such that
A9: p1 in Ux & p2 in Uy and
A10: p = [p1, p2] by ZFMISC_1:def 2;
consider r1, r2 being Real such that
A11: p = [r1, r2] and
A12: r2 = -r1 by A8;
p1 = r1 & p2 = r2 by XTUPLE_0:1, A10, A11; then
A13: r1 >= x & r1 < x+1 & r2 >= y & r2 < y+1 by XXREAL_1:3, A9; then
r1 <= x by XREAL_1:24, A5, A12; then
A14: r1 = x by A13, XXREAL_0:1;
r2 <= y by XREAL_1:24, A12, A13, A5; then
r2 = y by A13, XXREAL_0:1;
hence p in v by A2, A14, A11, A4, TARSKI:def 1;
end;
let p be object;
assume p in v; then
A15: p = z by A2, TARSKI:def 1;
x < x+1 & y < y+1 by XREAL_1:29; then
x in Ux & y in Uy by XXREAL_1:3; then
p in U2 by ZFMISC_1:def 2, A15, A4;
hence p in U2 /\ L by XBOOLE_0:def 4, A15, A3;
end;
L = [#] T by PRE_TOPC:def 5;
hence v is open by A6, A7, PRE_TOPC:def 4;
end;
set V = {{v} where v is Element of S2 : v in L};
V c= bool [#] T
proof
let z be object;
reconsider zz=z as set by TARSKI:1;
assume z in V;
then consider v being Element of S2 such that
A16: z = {v} and
A17: v in L;
A18: v in [#] T by A17, PRE_TOPC:def 5;
zz c= [#] T
proof
let y be object;
assume y in zz;
hence y in [#] T by TARSKI:def 1, A16, A18;
end;
hence z in bool [#] T;
end;
then reconsider V as Subset-Family of T;
A19: V is open
proof
let u be Subset of T;
assume u in V;
then consider z being Element of S2 such that
A20: u = {z} and
A21: z in L;
thus u is open by A20, A21, A1;
end;
A22: V is Cover of T
proof
let z be object;
assume z in the carrier of T;
then z in [#] T; then
z in L by PRE_TOPC:def 5; then
{z} in V & z in {z} by TARSKI:def 1;
hence z in union V by TARSKI:def 4;
end;
defpred Pg[object, object] means
ex x,y being Real st $1 = x & $2 = {[x,y]};
A23: for r being object st r in REAL ex v being object st v in V & Pg[r,v]
proof
let r be object;
assume r in REAL;
then reconsider r as Real;
reconsider y = -r as Real;
set u = [r,y];
A24: u in L;
then reconsider u as Element of S2;
set v = {u};
v in V by A24;
hence thesis;
end;
consider g being Function of REAL, V such that
A25: for r being object st r in REAL holds Pg[r,g.r] from FUNCT_2:sch 1(A23);
reconsider x = 1 as Element of REAL by XREAL_0:def 1;
reconsider y = -1 as Element of REAL by XREAL_0:def 1;
set z = [x,y];
A26: z in L; then
reconsider z as Element of S2;
{z} in V by A26; then
A27: dom g = REAL by FUNCT_2:def 1;
A28: g is one-to-one
proof
let r1,r2 be object such that
A29: r1 in dom g and
A30: r2 in dom g and
A31: g.r1 = g.r2;
consider x1,y1 being Real such that
A32: r1 = x1 and
A33: g.r1 = {[x1,y1]} by A25, A29;
consider x2,y2 being Real such that
A34: r2 = x2 and
A35: g.r2 = {[x2,y2]} by A25, A30;
[x1,y1] = [x2,y2] by ZFMISC_1:3, A35, A33, A31;
hence r1 = r2 by A32, A34, XTUPLE_0:1;
end;
rng g c= V; then
A36: card REAL c= card V by CARD_1:10, A28, A27;
A37: not card V c= omega by A36, TOPGEN_3:30, TOPGEN_3:def 4;
A38: not ex G being Subset-Family of T st G c= V & G is Cover of T &
G is countable
proof
assume ex G being Subset-Family of T st G c= V & G is Cover of T &
G is countable;
then consider G being Subset-Family of T such that
A39: G c= V and
A40: G is Cover of T and
A41: G is countable;
per cases by A39, XBOOLE_0:def 8;
suppose
G c< V;
then consider u being object such that
A42: u in V and
A43: not u in G by XBOOLE_0:6;
consider v being Element of S2 such that
A44: u = {v} and
A45: v in L by A42;
A46: [#] T c= union G by SETFAM_1:def 11, A40;
v in [#] T by A45, PRE_TOPC:def 5;
then consider u1 being set such that
A47: v in u1 and
A48: u1 in G by TARSKI:def 4, A46;
u1 in V by A39, A48;
then consider v1 being Element of S2 such that
A49: u1 = {v1} and v1 in L;
thus contradiction by A43, A44, A49, A48, A47, TARSKI:def 1;
end;
suppose G = V;
hence contradiction by A37, CARD_3:def 14, A41;
end;
end;
thus S2 is not Lindelof by Th4, METRIZTS:def 2, A19, A22, A38;
::registration in METRIZTS after Lm11
end;
registration
cluster Sorgenfrey-plane -> non Lindelof;
coherence by Lm12;
end;
registration
cluster Sorgenfrey-line -> regular;
coherence by TOPGEN_5:59;
:: Since Tychonoff -> regular
end;
registration
cluster Sorgenfrey-line -> normal;
coherence;
end;
Lm13: :: Following TOPGEN_5:47
Sorgenfrey-plane is not normal
proof
set L = real-anti-diagonal;
set S2 = Sorgenfrey-plane;
reconsider C = [:RAT,RAT:] as dense Subset of Sorgenfrey-plane by Th2;
defpred P[object,object] means
ex S being set, U,V being open Subset of S2 st $1 = S &
$2 = U /\ C & S c= U & L \ S c= V & U misses V;
A1: exp(2, omega) in exp(2, exp(2, omega)) by CARD_5:14;
card C c= omega by CARD_3:def 14,CARD_4:7; then
A2: exp(2, card C) c= exp(2, omega) by CARD_2:93;
assume
A3: for W, V being Subset of S2 st W <> {} & V <> {} & W is closed & V is
closed & W misses V ex P, Q being Subset of S2 st P is open
& Q is open & W c= P & V c= Q & P misses Q;
A4: for a being object st a in bool L ex b being object st P[a,b]
proof
let a be object;
assume a in bool L;
then reconsider aa = a as Subset of L;
reconsider a9 = L \ aa as Subset of L by XBOOLE_1:36;
reconsider A = aa, B = a9 as closed Subset of S2 by Th6;
per cases;
suppose
A5: a = {};
take {},{};
take {}S2,[#]S2;
thus thesis by A5, Th4, XBOOLE_1:65;
end;
suppose
A6: a = L;
take ([#]S2)/\ C,L;
take [#]S2,{}S2;
thus thesis by A6, Th4, XBOOLE_1:37,65;
end;
suppose
A7: a <> {} & a <> L;
aa`` = a9`; then
A8: B <> {}L by A7;
A misses B by XBOOLE_1:79;
then consider P, Q being Subset of S2 such that
A9: P is open and
A10: Q is open and
A11: A c= P and
A12: B c= Q and
A13: P misses Q by A8,A3,A7;
take P /\ C;
thus thesis by A9,A10,A11,A12,A13;
end;
end;
consider G being Function such that
A14: dom G = bool L and
A15: for a being object st a in bool L holds P[a,G.a] from CLASSES1:
sch 1(A4);
G is one-to-one
proof
let x,y be object;
assume that
A16: x in dom G and
A17: y in dom G;
reconsider A = x, B = y as Subset of L by A16,A17,A14;
assume that
A18: G.x = G.y and
A19: x <> y;
consider z being object such that
A20: not (z in A iff z in B) by A19,TARSKI:2;
A21: z in A\B or z in B\A by A20,XBOOLE_0:def 5;
P[B,G.B] by A15;
then consider UB,VB being open Subset of S2 such that
A22: G.B = UB /\ C and
A23: B c= UB and
A24: L \ B c= VB and
A25: UB misses VB;
P[A,G.A] by A15;
then consider UA,VA being open Subset of S2 such that
A26: G.A = UA /\ C and
A27: A c= UA and
A28: L \ A c= VA and
A29: UA misses VA;
B\A = B/\A` by SUBSET_1:13; then
A30: B\A c= UB /\ VA by A28,A23,XBOOLE_1:27;
A\B = A/\B` by SUBSET_1:13;
then A\B c= UA /\ VB by A27,A24,XBOOLE_1:27;
then (ex z being object st z in C & z in UA /\ VB) or
ex z being object st z in C & z in UB /\ VA
by XBOOLE_0:3,A30,A21,TOPS_1:45;
then consider z being set such that
A31: z in C and
A32: z in UA /\ VB or z in UB /\ VA;
z in UA & z in VB or z in UB & z in VA by A32,XBOOLE_0:def 4;
then z in UA & not z in UB or z in UB & not z in UA by
A29,A25,XBOOLE_0:3;
then z in G.A & not z in G.B or z in G.B & not z in G.A by A26,A22,A31,
XBOOLE_0:def 4;
hence thesis by A18;
end; then
A33: card dom G c= card rng G by CARD_1:10;
rng G c= bool C
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
assume a in rng G;
then consider b being object such that
A34: b in dom G and
A35: a = G.b by FUNCT_1:def 3;
P[b,a] by A14,A15,A34,A35;
then aa c= C by XBOOLE_1:17;
hence thesis;
end;
then card rng G c= card bool C by CARD_1:11;
then card bool L c= card bool C by A33,A14,XBOOLE_1:1; then
A36:exp(2, continuum) c= card bool C by CARD_2:31, Th3;
card bool C = exp(2, card C) by CARD_2:31;
then exp(2, continuum) c= exp(2, omega) by A36,A2,XBOOLE_1:1;
then exp(2, omega) in exp(2, omega) by A1,TOPGEN_3:29;
hence contradiction;
end;
registration
cluster Sorgenfrey-plane -> non normal;
coherence by Lm13;
end;