Copyright (c) 1999 Association of Mizar Users
environ
vocabulary ARYTM, METRIC_1, PRE_TOPC, EUCLID, SQUARE_1, ARYTM_1, ARYTM_3,
RELAT_1, ABSVALUE, FINSEQ_2, FINSEQ_1, FUNCT_1, GROUP_1, RVSUM_1,
RCOMP_1, ORDINAL2, SEQ_2, LATTICES, FINSET_1, PCOMPS_1, RELAT_2,
SUBSET_1, BOOLE, CONNSP_1, COMPTS_1, T_0TOPSP, TOPS_2, SETFAM_1, TARSKI,
CARD_3, FUNCOP_1, CAT_1, COMPLEX1, RLVECT_1, MCART_1, TOPREAL1, PSCOMP_1,
JORDAN1, SPPOL_1, TOPREAL4, TOPREAL2, SPRECT_1, FUNCT_5, JORDAN2C, SEQ_1,
TOPMETR, CONNSP_2, TOPS_1, BORSUK_1, PARTFUN1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
FUNCT_3, BINOP_1, FINSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1,
SQUARE_1, NAT_1, ABSVALUE, BINARITH, CQC_LANG, FUNCT_4, SEQ_1, SEQ_2,
SEQ_4, STRUCT_0, GROUP_1, METRIC_1, TBSP_1, FINSEQ_1, FINSEQ_2, RVSUM_1,
NEWTON, CARD_3, FINSEQ_4, RCOMP_1, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1,
CONNSP_2, COMPTS_1, BORSUK_1, PCOMPS_1, EUCLID, WEIERSTR, TOPMETR,
TOPREAL1, TOPREAL2, T_0TOPSP, JORDAN1, TOPREAL4, PSCOMP_1, SPPOL_1,
JGRAPH_1, SPRECT_1, JORDAN2C;
constructors BINARITH, BORSUK_3, CARD_4, COMPTS_1, CONNSP_1, FINSEQOP,
FINSEQ_4, GOBOARD9, JORDAN1, JORDAN2C, LIMFUNC1, PSCOMP_1, RCOMP_1,
REAL_1, REALSET1, SPPOL_1, SPRECT_1, TBSP_1, TOPGRP_1, TOPREAL2,
TOPREAL4, TOPS_1, TOPS_2, WAYBEL_3, WEIERSTR, CQC_LANG, TOPRNS_1,
MEMBERED, PARTFUN1;
clusters SUBSET_1, XREAL_0, BORSUK_1, BORSUK_3, FUNCT_4, EUCLID, FINSET_1,
GOBOARD9, METRIC_1, PCOMPS_1, PRE_TOPC, PSCOMP_1, RCOMP_1, RELSET_1,
SPRECT_1, SPRECT_2, STRUCT_0, TEX_4, TOPGRP_1, TOPMETR, TOPS_1, WAYBEL_2,
WAYBEL12, YELLOW13, ARYTM_3, SQUARE_1, FINSEQ_5, MEMBERED, ZFMISC_1,
NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FUNCT_1, PRE_TOPC, TOPS_2, CONNSP_1, CONNSP_2, BORSUK_1,
GROUP_1, JORDAN1, JORDAN2C, SEQ_4, METRIC_6, PSCOMP_1, SPPOL_1, T_0TOPSP,
TOPREAL2, XBOOLE_0;
theorems ABSVALUE, AXIOMS, BORSUK_1, BORSUK_3, CARD_3, FUNCT_4, CATALG_1,
COMPTS_1, CONNSP_1, CONNSP_2, EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_3,
FUNCT_1, FUNCT_2, FUNCT_3, GOBOARD6, GOBOARD7, GOBOARD9, GROUP_7, HEINE,
JGRAPH_1, JORDAN1, JORDAN2C, JORDAN3, JORDAN4, JORDAN5A, JORDAN6,
METRIC_1, METRIC_6, NEWTON, NAT_1, PCOMPS_1, PRE_TOPC, PREPOWER,
PSCOMP_1, RCOMP_1, REAL_1, REAL_2, RELAT_1, RVSUM_1, SEQ_2, SEQ_4,
SPPOL_1, SPRECT_1, SQUARE_1, SUBSET_1, TARSKI, TBSP_1, TOPMETR, TOPREAL1,
TOPREAL3, TOPREAL4, TOPS_1, TOPS_2, WEIERSTR, YELLOW12, ZFMISC_1,
XREAL_0, AMI_1, CQC_LANG, TOPREAL5, SETFAM_1, XBOOLE_0, XBOOLE_1,
XCMPLX_0, XCMPLX_1;
schemes FINSET_1, NAT_1, FUNCT_2;
begin :: Real numbers
reserve a, b for real number,
r for Real,
i, j, n for Nat,
M for non empty MetrSpace,
p, q, s for Point of TOP-REAL 2,
e for Point of Euclid 2,
w for Point of Euclid n,
z for Point of M,
A, B for Subset of TOP-REAL n,
P for Subset of TOP-REAL 2,
D for non empty Subset of TOP-REAL 2;
Lm1: sqrt 2 > 0 by AXIOMS:22,SQUARE_1:84;
Lm2: Euclid 2 = MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
canceled 5;
theorem Th6:
0 <= a & 0 <= b implies sqrt(a+b) <= sqrt a + sqrt b
proof
assume
A1: 0 <= a & 0 <= b;
then A2: 0 + 0 <= a + b by REAL_1:55;
0 <= sqrt a & 0 <= sqrt b by A1,SQUARE_1:def 4;
then A3: 0 + 0 <= sqrt a + sqrt b by REAL_1:55;
A4: sqrt(a + 2*sqrt a*sqrt b + b)
= sqrt((sqrt a)^2 + 2*sqrt a*sqrt b + b) by A1,SQUARE_1:def 4
.= sqrt((sqrt a)^2 + 2*sqrt a*sqrt b + (sqrt b)^2) by A1,SQUARE_1:def 4
.= sqrt((sqrt a + sqrt b)^2) by SQUARE_1:63
.= sqrt a + sqrt b by A3,SQUARE_1:89;
0 <= a*b by A1,REAL_2:121;
then 0 <= sqrt(a*b) by SQUARE_1:def 4;
then 0 <= sqrt a*sqrt b by A1,SQUARE_1:97;
then 0 <= 2*(sqrt a*sqrt b) by REAL_2:121;
then 0 <= 2*sqrt a*sqrt b by XCMPLX_1:4;
then a + 0 <= a + 2*sqrt a*sqrt b by AXIOMS:24;
then a + b <= a + 2*sqrt a*sqrt b + b by AXIOMS:24;
hence thesis by A2,A4,SQUARE_1:94;
end;
theorem Th7:
0 <= a & a <= b implies abs(a) <= abs(b)
proof
assume
A1: 0 <= a & a <= b;
then abs(a) = a & abs(b) = b by ABSVALUE:def 1;
hence abs(a) <= abs(b) by A1;
end;
theorem Th8:
b <= a & a <= 0 implies abs(a) <= abs(b)
proof
assume that
A1: b <= a and
A2: a <= 0;
per cases by A2;
suppose a = 0;
then abs(a) = 0 by ABSVALUE:7;
hence thesis by ABSVALUE:5;
suppose
A3: a < 0;
then b < 0 by A1;
then abs(a) = -a & abs(b) = -b by A3,ABSVALUE:def 1;
hence abs(a) <= abs(b) by A1,REAL_1:50;
end;
theorem
Product(0|->r) = 1 by FINSEQ_2:72,RVSUM_1:124;
theorem Th10:
Product(1|->r) = r
proof
thus Product(1|->r) = Product<*r*> by FINSEQ_2:73
.= r by RVSUM_1:125;
end;
theorem
Product(2|->r) = r * r
proof
thus Product(2|->r) = Product<*r,r*> by FINSEQ_2:75
.= r * r by RVSUM_1:129;
end;
theorem Th12:
Product((n+1)|->r) = (Product(n|->r))*r
proof
thus Product((n+1)|->r) = (Product(n|->r))*(Product(1|->r)) by RVSUM_1:134
.= (Product(n|->r))*r by Th10;
end;
theorem Th13:
j <> 0 & r = 0 iff Product(j|->r) = 0
proof
set f = j|->r;
A1: dom f = Seg j by FINSEQ_2:68;
hereby
assume that
A2: j <> 0 and
A3: r = 0;
consider n such that
A4: j = n + 1 by A2,NAT_1:22;
1 <= j by A4,NAT_1:29;
then A5: 1 in Seg j by FINSEQ_1:3;
then f.1 = 0 by A3,FINSEQ_2:70;
hence Product f = 0 by A1,A5,RVSUM_1:133;
end;
assume Product f = 0;
then consider n such that
A6: n in dom f & f.n = 0 by RVSUM_1:133;
thus thesis by A1,A6,FINSEQ_1:4,FINSEQ_2:70;
end;
theorem Th14:
r <> 0 & j <= i implies Product((i-'j)|->r) = Product(i|->r) / Product(j|->r)
proof
assume that
A1: r <> 0 and
A2: j <= i;
A3: Product(j|->r) <> 0 by A1,Th13;
defpred P[Nat] means j <= $1 implies Product(($1-'j)|->r) =
Product($1|->r) / Product(j|->r);
A4: P[0]
proof
assume j <= 0;
then A5: j = 0 by NAT_1:19;
hence Product((0-'j)|->r)
= Product(0|->r) / Product<*>REAL by JORDAN3:2,RVSUM_1:124
.= Product(0|->r) / Product(j|->r) by A5,FINSEQ_2:72;
end;
A6: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume that
A7: P[n] and
A8: j <= n+1;
per cases by A8,NAT_1:26;
suppose
A9: j <= n;
Product((n-'j+1)|->r) = Product((n-'j)|->r)*Product(1|->r) by RVSUM_1:
134
.= Product(n|->r) / Product(j|->r) * r by A7,A9,Th10
.= Product(n|->r) * r / Product(j|->r) by XCMPLX_1:75
.= Product((n+1)|->r) / Product(j|->r) by Th12;
hence Product(((n+1)-'j)|->r) = Product((n+1)|->r) / Product(j|->r)
by A9,JORDAN4:3;
suppose
A10: j = n+1;
hence Product(((n+1)-'j)|->r)
= Product(0|->r) by GOBOARD9:1
.= 1 by FINSEQ_2:72,RVSUM_1:124
.= Product((n+1)|->r) / Product(j|->r) by A3,A10,XCMPLX_1:60;
end;
for n being Nat holds P[n] from Ind(A4,A6);
hence thesis by A2;
end;
theorem
r <> 0 & j <= i implies r|^(i-'j) = r|^i / r|^j
proof
assume
A1: r <> 0 & j <= i;
thus r|^i / r|^j = (Product(i |-> r)) / r|^j by NEWTON:def 1
.= (Product(i |-> r)) / (Product(j |-> r)) by NEWTON:def 1
.= Product((i-'j) |-> r) by A1,Th14
.= r|^(i-'j) by NEWTON:def 1;
end;
reserve a, b for Real;
theorem Th16:
sqr <*a,b*> = <*a^2,b^2*>
proof
dom sqrreal = REAL by FUNCT_2:def 1;
then A1: rng <*a,b*> c= dom sqrreal by FINSEQ_1:def 4;
A2: dom sqr <*a,b*>
= dom (sqrreal*<*a,b*>) by RVSUM_1:def 8
.= dom <*a,b*> by A1,RELAT_1:46
.= {1,2} by FINSEQ_1:4,FINSEQ_3:29;
A3: dom <*a^2,b^2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
for i being set st i in dom <*a^2,b^2*> holds (sqr <*a,b*>).i = <*a^2,b^2
*>.i
proof
let i be set; assume
A4: i in dom <*a^2,b^2*>;
A5: <*a,b*>.1 = a & <*a,b*>.2 = b by FINSEQ_1:61;
per cases by A3,A4,TARSKI:def 2;
suppose
A6: i = 1;
hence (sqr <*a,b*>).i
= a^2 by A5,RVSUM_1:78
.= <*a^2,b^2*>.i by A6,FINSEQ_1:61;
suppose
A7: i = 2;
hence (sqr <*a,b*>).i
= b^2 by A5,RVSUM_1:78
.= <*a^2,b^2*>.i by A7,FINSEQ_1:61;
end;
hence thesis by A2,A3,FUNCT_1:9;
end;
theorem Th17:
for F being FinSequence of REAL st i in dom abs F & a = F.i holds
(abs F).i = abs(a)
proof
let F be FinSequence of REAL such that
A1: i in dom abs F and
A2: a = F.i;
abs F = absreal*F & i in dom abs F by A1,EUCLID:def 3;
then (abs F).i = absreal.a by A2,FUNCT_1:22;
hence thesis by EUCLID:def 2;
end;
theorem
abs <*a,b*> = <*abs(a),abs(b)*>
proof
dom absreal = REAL by FUNCT_2:def 1;
then A1: rng <*a,b*> c= dom absreal by FINSEQ_1:def 4;
A2: dom abs <*a,b*>
= dom (absreal*<*a,b*>) by EUCLID:def 3
.= dom <*a,b*> by A1,RELAT_1:46
.= {1,2} by FINSEQ_1:4,FINSEQ_3:29;
A3: dom <*abs(a),abs(b)*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
for i being set st i in dom <*abs(a),abs(b)*> holds
(abs <*a,b*>).i = <*abs(a),abs(b)*>.i
proof
let i be set; assume
A4: i in dom <*abs(a),abs(b)*>;
A5: <*a,b*>.1 = a & <*a,b*>.2 = b by FINSEQ_1:61;
A6: 1 in {1,2} & 2 in {1,2} by TARSKI:def 2;
per cases by A3,A4,TARSKI:def 2;
suppose
A7: i = 1;
hence (abs <*a,b*>).i
= abs(a) by A2,A5,A6,Th17
.= <*abs(a),abs(b)*>.i by A7,FINSEQ_1:61;
suppose
A8: i = 2;
hence (abs <*a,b*>).i
= abs(b) by A2,A5,A6,Th17
.= <*abs(a),abs(b)*>.i by A8,FINSEQ_1:61;
end;
hence thesis by A2,A3,FUNCT_1:9;
end;
theorem
for a, b, c, d being real number st a <= b & c <= d holds
abs(b-a) + abs(d-c) = (b-a) + (d-c)
proof
let a, b, c, d be real number;
assume a <= b & c <= d;
then a - a <= b - a & c - c <= d - c by REAL_1:92;
then 0 <= b - a & 0 <= d - c by XCMPLX_1:14;
then abs(b-a) = b - a & abs(d-c) = d - c by ABSVALUE:def 1;
hence thesis;
end;
theorem Th20:
for a, r being real number holds r > 0 implies a in ].a-r,a+r.[
proof
let a, r be real number;
assume
A1: r > 0;
abs(a-a) = abs(0) by XCMPLX_1:14;
then abs(a-a) < r by A1,ABSVALUE:def 1;
hence thesis by RCOMP_1:8;
end;
theorem
for a, r being real number holds r >= 0 implies a in [.a-r,a+r.]
proof
let a, r be real number;
assume
A1: r >= 0;
reconsider a, r as Real by XREAL_0:def 1;
A2: [.a-r,a+r.] = {b : a-r <= b & b <= a+r} by RCOMP_1:def 1;
a-r <= a-0 & a+0 <= a+r by A1,REAL_1:55,92; hence thesis by A2;
end;
theorem Th22:
for a, b being real number holds
a < b implies inf ].a,b.[ = a & sup ].a,b.[ = b
proof
let a, b be real number;
assume
A1: a < b;
set X = ].a,b.[;
reconsider a, b as Real by XREAL_0:def 1;
A2: ex p being real number st for r being real number st r in X holds p <= r
proof
take a;
let r be real number; assume r in X;
then r in { l where l is Real : a < l & l < b } by RCOMP_1:def 2;
then consider r1 being Real such that
A3: r1 = r & a < r1 & r1 < b;
thus thesis by A3;
end;
A4: ex p be real number st for r being real number st r in X holds p >= r
proof
take b;
let r be real number; assume r in X;
then r in { l where l is Real : a < l & l < b } by RCOMP_1:def 2;
then consider r1 being Real such that
A5: r1 = r & a < r1 & r1 < b;
thus thesis by A5;
end;
A6:a < (a+b)/2 & (a+b)/2 < b by A1,TOPREAL3:3;
then A7: (a+b)/2 in { l where l is Real : a < l & l < b };
then A8: (a+b)/2 in X by RCOMP_1:def 2;
then A9: (ex r being real number st r in X) & X is bounded_below by A2,SEQ_4:
def 2;
A10: (ex r being real number st r in X) & X is bounded_above
by A4,A8,SEQ_4:def 1;
A11:for r being real number st r in X holds a <= r
proof
let r be real number;
assume r in X;
then r in { l where l is Real : a < l & l < b } by RCOMP_1:def 2;
then consider r1 being Real such that
A12: r1 = r & a < r1 & r1 < b;
thus thesis by A12;
end;
A13:for s being real number st 0 < s ex r being real number
st r in X & r < a+s
proof
let s be real number such that
A14: 0 < s and
A15: for r being real number st r in X holds r >= a+s;
reconsider s as Real by XREAL_0:def 1;
per cases;
suppose a + s >= b;
then (a+b)/2 in X & (a+b)/2 < a+s by A6,A7,AXIOMS:22,RCOMP_1:def 2;
hence thesis by A15;
suppose
A16: a + s < b;
A17: a < a + s by A14,REAL_1:69;
then A18: a < (a+(a+s))/2 by TOPREAL3:3;
A19: (a+(a+s))/2 < a+s by A17,TOPREAL3:3;
then (a+(a+s))/2 < b by A16,AXIOMS:22;
then (a+(a+s))/2 in {r : a < r & r < b } by A18;
then (a+(a+s))/2 in X by RCOMP_1:def 2;
hence thesis by A15,A19;
end;
A20:for r being real number st r in X holds b >= r
proof
let r be real number;
assume r in X;
then r in { l where l is Real : a < l & l < b } by RCOMP_1:def 2;
then consider r1 being Real such that
A21: r1 = r & a < r1 & r1 < b;
thus thesis by A21;
end;
for s being real number st 0 < s ex r being real number st
r in X & b-s < r
proof
let s be real number such that
A22: 0 < s and
A23: for r being real number st r in X holds r <= b-s;
reconsider s as Real by XREAL_0:def 1;
per cases;
suppose b - s <= a;
then (a+b)/2 in X & (a+b)/2 > b-s by A6,A7,AXIOMS:22,RCOMP_1:def 2;
hence thesis by A23;
suppose
A24: b - s > a;
A25: b - s < b - 0 by A22,REAL_1:92;
then b-s < (b+(b-s))/2 by TOPREAL3:3;
then A26: a < (b+(b-s))/2 by A24,AXIOMS:22;
A27: (b+(b-s))/2 > b-s by A25,TOPREAL3:3;
(b+(b-s))/2 < b by A25,TOPREAL3:3;
then (b+(b-s))/2 in {r : a < r & r < b } by A26;
then (b+(b-s))/2 in X by RCOMP_1:def 2;
hence thesis by A23,A27;
end;
hence thesis by A9,A10,A11,A13,A20,SEQ_4:def 4,def 5;
end;
canceled;
theorem Th24:
for A being bounded Subset of REAL holds A c= [.inf A,sup A.]
proof
let A be bounded Subset of REAL;
let a be set;
assume
A1: a in A;
then reconsider r = a as Real;
inf A <= r & r <= sup A by A1,SEQ_4:def 4,def 5;
hence a in [.inf A,sup A.] by TOPREAL5:1;
end;
begin :: Topological preliminaries
definition let T be TopStruct, A be finite Subset of T;
cluster T|A -> finite;
coherence
proof
thus the carrier of T|A is finite by JORDAN1:1;
end;
end;
definition
cluster finite non empty strict TopSpace;
existence
proof
take 1TopSp {0};
thus thesis;
end;
end;
definition let T be TopStruct;
cluster empty -> connected Subset of T;
coherence
proof
let C be Subset of T;
assume C is empty;
then reconsider D = C as empty Subset of T;
let A, B be Subset of T|C such that
A1: [#](T|C) = A \/ B and A,B are_separated;
[#](T|D) = {};
hence A = {}(T|C) or B = {}(T|C) by A1,XBOOLE_1:15;
end;
end;
definition let T be TopSpace;
cluster finite -> compact Subset of T;
coherence
proof
let A be Subset of T;
assume A is finite;
then reconsider B = A as finite Subset of T;
A1: T|B is compact;
B = {} or B <> {};
hence thesis by A1,COMPTS_1:12;
end;
end;
theorem Th25:
for S, T being TopSpace st S, T are_homeomorphic & S is connected holds
T is connected
proof
let S, T be TopSpace;
given f being map of S,T such that
A1: f is_homeomorphism;
assume
A2: S is connected;
A3: f is continuous by A1,TOPS_2:def 5;
dom f = [#]S & rng f = [#]T by A1,TOPS_2:def 5;
then f.:[#]S = [#]T by RELAT_1:146;
hence T is connected by A2,A3,CONNSP_1:15;
end;
theorem
for T being TopSpace, F being finite Subset-Family of T st
for X being Subset of T st X in F holds X is compact holds
union F is compact
proof
let T be TopSpace,
F be finite Subset-Family of T such that
A1: for X being Subset of T st X in F holds X is compact;
defpred P[set] means
ex A being Subset of T st A = union $1 & A is compact;
A2: F is finite;
A3: P[{}]
proof
take {}T;
thus thesis by ZFMISC_1:2;
end;
A4: for x, B being set st x in F & B c= F & P[B] holds P[B \/ {x}]
proof
let x, B be set such that
A5: x in F and
A6: B c= F;
given A being Subset of T such that
A7: A = union B and
A8: A is compact;
reconsider X = x as Subset of T by A5;
B c= bool the carrier of T
proof
let b be set;
assume b in B;
then b in F by A6;
hence thesis;
end;
then B is Subset-Family of T by SETFAM_1:def 7;
then reconsider C = B as Subset-Family of T;
set K = union C \/ X;
take K;
union {x} = x by ZFMISC_1:31;
hence K = union (B \/ {x}) by ZFMISC_1:96;
X is compact by A1,A5;
hence K is compact by A7,A8,COMPTS_1:19;
end;
P[F] from Finite(A2,A3,A4);
hence thesis;
end;
begin
canceled 2;
theorem Th29:
for A, B, C, D, a, b being set st A c= B & C c= D holds
product ((a,b) --> (A,C)) c= product ((a,b) --> (B,D))
proof
let A, B, C, D, a, b be set such that
A1: A c= B & C c= D;
set f = (a,b) --> (A,C),
g = (a,b) --> (B,D);
A2: dom f = {a,b} & dom g = {a,b} by FUNCT_4:65;
for x being set st x in dom f holds f.x c= g.x
proof
let x be set;
assume x in dom f;
then A3: x = a or x = b by A2,TARSKI:def 2;
per cases;
suppose a <> b;
then f.a = A & f.b = C & g.a = B & g.b = D by FUNCT_4:66;
hence thesis by A1,A3;
suppose
A4: a = b;
then f = a .--> C & g = a .--> D by AMI_1:20;
then f.a = C & f.b = C & g.b = D & g.b = D by A4,CQC_LANG:6;
hence thesis by A1,A3,A4;
end;
hence product f c= product g by A2,CARD_3:38;
end;
theorem Th30:
for A, B being Subset of REAL holds
product ((1,2) --> (A,B)) is Subset of TOP-REAL 2
proof
let A, B be Subset of REAL;
set f = (1,2) --> (A,B);
product f c= the carrier of TOP-REAL 2
proof
let a be set;
assume a in product f;
then consider g being Function such that
A1: a = g and
A2: dom g = dom f and
A3: for x being set st x in dom f holds g.x in f.x by CARD_3:def 5;
A4: dom f = {1,2} by FUNCT_4:65;
then A5: 1 in dom f & 2 in dom f by TARSKI:def 2;
f.1 = A & f.2 = B by FUNCT_4:66;
then g.1 in A & g.2 in B by A3,A5;
then reconsider m = g.1, n = g.2 as Real;
A6: dom <*g.1,g.2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
now
let k be set;
assume k in dom g;
then k = 1 or k = 2 by A2,A4,TARSKI:def 2;
hence g.k = <*g.1,g.2*>.k by FINSEQ_1:61;
end;
then a = <*g.1,g.2*> by A1,A2,A4,A6,FUNCT_1:9;
then a = |[m,n]| by EUCLID:def 16;
hence thesis;
end;
hence thesis;
end;
theorem
|.|[0,a]|.| = abs(a) & |.|[a,0]|.| = abs(a)
proof
A1: <*0,a*> = |[0,a]| by EUCLID:def 16;
A2: <*a,0 *> = |[a,0]| by EUCLID:def 16;
A3: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:25;
|.<*0,a*>.|
= sqrt Sum sqr <*0,a*> by EUCLID:def 5
.= sqrt Sum <*0^2,a^2*> by Th16
.= sqrt (0+a^2) by RVSUM_1:107,SQUARE_1:60
.= abs(a) by SQUARE_1:91;
hence |.|[0,a]|.| = abs(a) by A1,A3,JGRAPH_1:def 5;
|.<*a,0 *>.|
= sqrt Sum sqr <*a,0 *> by EUCLID:def 5
.= sqrt Sum <*a^2,0^2 *> by Th16
.= sqrt (a^2+0) by RVSUM_1:107,SQUARE_1:60
.= abs a by SQUARE_1:91;
hence thesis by A2,A3,JGRAPH_1:def 5;
end;
theorem Th32:
for p being Point of Euclid 2, q being Point of TOP-REAL 2 st
p = 0.REAL 2 & p = q holds q = <* 0,0 *> & q`1 = 0 & q`2 = 0
proof
let p be Point of Euclid 2,
q be Point of TOP-REAL 2 such that
A1: p = 0.REAL 2 and
A2: p = q;
A3: p = 0*2 by A1,EUCLID:def 9
.= 2 |-> (0 qua Real) by EUCLID:def 4
.= <*0,0 *> by FINSEQ_2:75;
then p = |[ 0,0 ]| by EUCLID:def 16;
hence thesis by A2,A3,EUCLID:56;
end;
theorem
for p, q being Point of Euclid 2, z being Point of TOP-REAL 2 st
p = 0.REAL 2 & q = z holds dist(p,q) = |.z.|
proof
let p, q be Point of Euclid 2,
z be Point of TOP-REAL 2 such that
A1: p = 0.REAL 2 and
A2: q = z;
reconsider P = p as Point of TOP-REAL 2 by TOPREAL3:13;
A3: P`1 = 0 & P`2 = 0 by A1,Th32;
dist(p,q) = (Pitag_dist 2).(p,q) by Lm2,METRIC_1:def 1
.= sqrt ((P`1 - z`1)^2 + (P`2 - z`2)^2) by A2,TOPREAL3:12
.= sqrt ((- z`1)^2 + (P`2 - z`2)^2) by A3,XCMPLX_1:150
.= sqrt ((- z`1)^2 + (- z`2)^2) by A3,XCMPLX_1:150
.= sqrt ((z`1)^2 + (- z`2)^2) by SQUARE_1:61
.= sqrt ((z`1)^2 + (z`2)^2) by SQUARE_1:61;
hence dist(p,q) = |.z.| by JGRAPH_1:47;
end;
theorem Th34:
r*p = |[r*p`1,r*p`2]|
proof
p = |[p`1,p`2]| by EUCLID:57;
hence thesis by EUCLID:62;
end;
theorem Th35:
s = (1-r)*p + r*q & s <> p & 0 <= r implies 0 < r
proof
assume that
A1: s = (1-r)*p + r*q and
A2: s <> p and
A3: 0 <= r;
assume
A4: r <= 0;
then s = (1-0)*p + r*q by A1,A3,REAL_1:def 5
.= (1-0)*p + 0 * q by A3,A4,REAL_1:def 5
.= 1 * p + 0.REAL 2 by EUCLID:33
.= 1 * p by EUCLID:31
.= p by EUCLID:33;
hence thesis by A2;
end;
theorem Th36:
s = (1-r)*p + r*q & s <> q & r <= 1 implies r < 1
proof
assume that
A1: s = (1-r)*p + r*q and
A2: s <> q and
A3: r <= 1;
assume
A4: r >= 1;
then s = (1-1)*p + r*q by A1,A3,REAL_1:def 5
.= 0 * p + 1 * q by A3,A4,REAL_1:def 5
.= 0.REAL 2 + 1 * q by EUCLID:33
.= 1 * q by EUCLID:31
.= q by EUCLID:33;
hence thesis by A2;
end;
theorem
s in LSeg(p,q) & s <> p & s <> q & p`1 < q`1 implies p`1 < s`1 & s`1 < q`1
proof
assume that
A1: s in LSeg(p,q) and
A2: s <> p & s <> q and
A3: p`1 < q`1;
LSeg(p,q) = { (1-r)*p + r*q : 0 <= r & r <= 1 } by TOPREAL1:def 4;
then consider r such that
A4: s = (1-r)*p + r*q and
A5: 0 <= r & r <= 1 by A1;
(1-r)*p = |[(1-r)*p`1,(1-r)*p`2]| & r*q = |[r*q`1,r*q`2]| by Th34;
then A6: ((1-r)*p)`1 = (1-r)*p`1 & (r*q)`1 = r*q`1 by EUCLID:56;
s = |[((1-r)*p)`1 + (r*q)`1,((1-r)*p)`2 + (r*q)`2]| by A4,EUCLID:59;
then A7: s`1 = (1-r)*p`1 + r*q`1 by A6,EUCLID:56;
then A8: q`1 - s`1 = 1 * q`1 - r*q`1 - (1-r)*p`1 by XCMPLX_1:36
.= (1-r)*q`1 - (1-r)*p`1 by XCMPLX_1:40
.= (1-r)*(q`1-p`1) by XCMPLX_1:40;
A9: p`1 - s`1 = 1 * p`1 - (1-r)*p`1 - r*q`1 by A7,XCMPLX_1:36
.= (1-(1-r))*p`1 - r*q`1 by XCMPLX_1:40
.= (1-1+r)*p`1 - r*q`1 by XCMPLX_1:37
.= r*(p`1-q`1) by XCMPLX_1:40;
A10: q`1-p`1 > 0 & p`1-q`1 < 0 by A3,REAL_2:105,SQUARE_1:11;
r < 1 by A2,A4,A5,Th36;
then 1-r > 0 & r > 0 by A2,A4,A5,Th35,SQUARE_1:11;
then q`1 - s`1 > 0 & p`1 - s`1 < 0 by A8,A9,A10,REAL_2:129,SQUARE_1:24;
hence thesis by REAL_2:106,SQUARE_1:12;
end;
theorem
s in LSeg(p,q) & s <> p & s <> q & p`2 < q`2 implies p`2 < s`2 & s`2 < q`2
proof
assume that
A1: s in LSeg(p,q) and
A2: s <> p & s <> q and
A3: p`2 < q`2;
LSeg(p,q) = { (1-r)*p + r*q : 0 <= r & r <= 1 } by TOPREAL1:def 4;
then consider r such that
A4: s = (1-r)*p + r*q and
A5: 0 <= r & r <= 1 by A1;
(1-r)*p = |[(1-r)*p`1,(1-r)*p`2]| & r*q = |[r*q`1,r*q`2]| by Th34;
then A6: ((1-r)*p)`2 = (1-r)*p`2 & (r*q)`2 = r*q`2 by EUCLID:56;
s = |[((1-r)*p)`1 + (r*q)`1,((1-r)*p)`2 + (r*q)`2]| by A4,EUCLID:59;
then A7: s`2 = (1-r)*p`2 + r*q`2 by A6,EUCLID:56;
then A8: q`2 - s`2 = 1 * q`2 - r*q`2 - (1-r)*p`2 by XCMPLX_1:36
.= (1-r)*q`2 - (1-r)*p`2 by XCMPLX_1:40
.= (1-r)*(q`2-p`2) by XCMPLX_1:40;
A9: p`2 - s`2 = 1 * p`2 - (1-r)*p`2 - r*q`2 by A7,XCMPLX_1:36
.= (1-(1-r))*p`2 - r*q`2 by XCMPLX_1:40
.= (1-1+r)*p`2 - r*q`2 by XCMPLX_1:37
.= r*(p`2-q`2) by XCMPLX_1:40;
A10: q`2-p`2 > 0 & p`2-q`2 < 0 by A3,REAL_2:105,SQUARE_1:11;
r < 1 by A2,A4,A5,Th36;
then 1-r > 0 & r > 0 by A2,A4,A5,Th35,SQUARE_1:11;
then q`2 - s`2 > 0 & p`2 - s`2 < 0 by A8,A9,A10,REAL_2:129,SQUARE_1:24;
hence thesis by REAL_2:106,SQUARE_1:12;
end;
theorem
for p being Point of TOP-REAL 2
ex q being Point of TOP-REAL 2 st q`1 < W-bound D & p <> q
proof
let p be Point of TOP-REAL 2;
take q = |[W-bound D - 1, p`2 - 1]|;
W-bound D - 1 < W-bound D - 0 by REAL_1:92;
hence q`1 < W-bound D by EUCLID:56;
p`2 - 1 < p`2 - 0 by REAL_1:92; hence p <> q by EUCLID:56;
end;
theorem
for p being Point of TOP-REAL 2
ex q being Point of TOP-REAL 2 st q`1 > E-bound D & p <> q
proof
let p be Point of TOP-REAL 2;
take q = |[E-bound D + 1, p`2 - 1]|;
E-bound D + 1 > E-bound D + 0 by REAL_1:53;
hence q`1 > E-bound D by EUCLID:56;
p`2 - 1 < p`2 - 0 by REAL_1:92; hence p <> q by EUCLID:56;
end;
theorem
for p being Point of TOP-REAL 2
ex q being Point of TOP-REAL 2 st q`2 > N-bound D & p <> q
proof
let p be Point of TOP-REAL 2;
take q = |[p`1 - 1,N-bound D + 1]|;
N-bound D + 1 > N-bound D + 0 by REAL_1:53;
hence q`2 > N-bound D by EUCLID:56;
p`1 - 1 < p`1 - 0 by REAL_1:92; hence p <> q by EUCLID:56;
end;
theorem
for p being Point of TOP-REAL 2
ex q being Point of TOP-REAL 2 st q`2 < S-bound D & p <> q
proof
let p be Point of TOP-REAL 2;
take q = |[p`1 - 1,S-bound D - 1]|;
S-bound D - 1 < S-bound D - 0 by REAL_1:92;
hence q`2 < S-bound D by EUCLID:56;
p`1 - 1 < p`1 - 0 by REAL_1:92; hence p <> q by EUCLID:56;
end;
definition
cluster convex non empty -> connected Subset of TOP-REAL 2;
coherence by JORDAN1:9;
cluster non horizontal -> non empty Subset of TOP-REAL 2;
coherence
proof
let P be Subset of TOP-REAL 2;
assume P is non horizontal;
then ex p, q being Point of TOP-REAL 2 st p in P & q in P & p`2 <> q`2
by SPPOL_1:def 2;
hence thesis;
end;
cluster non vertical -> non empty Subset of TOP-REAL 2;
coherence
proof
let P be Subset of TOP-REAL 2;
assume P is non vertical;
then ex p, q being Point of TOP-REAL 2 st p in P & q in P & p`1 <> q`1
by SPPOL_1:def 3;
hence thesis;
end;
cluster being_Region -> open connected Subset of TOP-REAL 2;
coherence by TOPREAL4:def 3;
cluster open connected -> being_Region Subset of TOP-REAL 2;
coherence by TOPREAL4:def 3;
end;
definition
cluster empty -> horizontal Subset of TOP-REAL 2;
coherence
proof
let A be Subset of TOP-REAL 2;
assume
A1: A is empty;
assume A is non horizontal;
then reconsider B = A as non horizontal Subset of TOP-REAL 2;
B is non empty;
hence thesis by A1;
end;
cluster empty -> vertical Subset of TOP-REAL 2;
coherence
proof
let A be Subset of TOP-REAL 2;
assume
A2: A is empty;
assume A is non vertical;
then reconsider B = A as non vertical Subset of TOP-REAL 2;
B is non empty;
hence thesis by A2;
end;
end;
definition
cluster non empty convex Subset of TOP-REAL 2;
existence
proof
consider C being non empty convex Subset of TOP-REAL 2;
take C;
thus thesis;
end;
end;
definition let a, b be Point of TOP-REAL 2;
cluster LSeg(a,b) -> convex connected;
coherence by GOBOARD9:7,8;
end;
definition
cluster R^2-unit_square -> connected;
coherence
proof
A1: R^2-unit_square = LSeg(|[ 0,0 ]|, |[ 0,1 ]|) \/ LSeg(|[ 0,1 ]|, |[ 1,1 ]|)
\/ LSeg(|[ 1,1 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 0,0 ]|)
by TOPREAL1:20,XBOOLE_1:4;
LSeg(|[0,0]|,|[0,1]|) meets LSeg(|[0,1]|,|[1,1]|) &
LSeg(|[0,0]|,|[1,0]|) meets LSeg(|[1,0]|,|[1,1]|) &
LSeg(|[0,1]|,|[1,1]|) meets LSeg(|[1,0]|,|[1,1]|)
by TOPREAL1:21,22,24,XBOOLE_0:def 7;
hence thesis by A1,JORDAN1:8;
end;
end;
definition
cluster being_simple_closed_curve -> connected compact Subset of TOP-REAL 2;
coherence
proof
let P be Subset of TOP-REAL 2;
given f being map of (TOP-REAL 2)|R^2-unit_square, (TOP-REAL 2)|P
such that
A1: f is_homeomorphism;
A2: (TOP-REAL 2)|R^2-unit_square, (TOP-REAL 2)|P are_homeomorphic
proof
take f;
thus f is_homeomorphism by A1;
end;
thus P is connected
proof
(TOP-REAL 2)|R^2-unit_square is connected by CONNSP_1:def 3;
then (TOP-REAL 2)|P is connected by A2,Th25;
hence thesis by CONNSP_1:def 3;
end;
per cases;
suppose
A3: P is empty;
{}TOP-REAL 2 is compact;
hence thesis by A3;
suppose P is non empty;
then reconsider R = P as non empty Subset of TOP-REAL 2;
f is continuous & rng f = [#]((TOP-REAL 2)|P) by A1,TOPS_2:def 5;
then (TOP-REAL 2)|R is compact by COMPTS_1:23;
hence P is compact by COMPTS_1:12;
end;
end;
theorem :: SPRECT_3:26
LSeg(NE-corner P,SE-corner P) c= L~SpStSeq P
proof
A1: LSeg(NE-corner P,SE-corner P) c=
(LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P))
by XBOOLE_1:7;
LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) c=
(LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P)) \/
(LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P))
by XBOOLE_1:7;
then LSeg(NE-corner P,SE-corner P) c=
(LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P)) \/
(LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P))
by A1,XBOOLE_1:1;
hence thesis by SPRECT_1:43;
end;
theorem
LSeg(SW-corner P,SE-corner P) c= L~SpStSeq P
proof
A1: LSeg(SW-corner P,SE-corner P) c=
(LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P)) \/
LSeg(SW-corner P,SE-corner P) by XBOOLE_1:7;
LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) \/
LSeg(SE-corner P,SW-corner P) c=
LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) \/
LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P)
by XBOOLE_1:7;
then LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) \/
LSeg(SE-corner P,SW-corner P) c=
LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) \/
(LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P))
by XBOOLE_1:4;
then LSeg(SW-corner P,SE-corner P) c=
(LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P)) \/
(LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P))
by A1,XBOOLE_1:1;
hence thesis by SPRECT_1:43;
end;
theorem
LSeg(SW-corner P,NW-corner P) c= L~SpStSeq P
proof
LSeg(SW-corner P,NW-corner P) c=
LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) \/
LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P)
by XBOOLE_1:7;
then LSeg(SW-corner P,NW-corner P) c=
LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) \/
(LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P))
by XBOOLE_1:4;
hence thesis by SPRECT_1:43;
end;
theorem
for C being Subset of TOP-REAL 2 holds
{p where p is Point of TOP-REAL 2: p`1 < W-bound C} is
non empty convex connected Subset of TOP-REAL 2
proof
let C be Subset of TOP-REAL 2;
set A = {p where p is Point of TOP-REAL 2: p`1 < W-bound C};
A c= the carrier of TOP-REAL 2
proof
let a be set;
assume a in A;
then consider p being Point of TOP-REAL 2 such that
A1: a = p and p`1 < W-bound C;
thus thesis by A1;
end;
then reconsider A as Subset of TOP-REAL 2;
set p = W-bound C;
set b = |[p-1,0]|;
A2: p - 1 < p - 0 by REAL_1:92;
b`1 = p-1 by EUCLID:56;
then A3: b in A by A2;
A is convex
proof
let w1, w2 be Point of TOP-REAL 2;
assume w1 in A;
then consider p being Point of TOP-REAL 2 such that
A4: w1 = p and
A5: p`1 < W-bound C;
assume w2 in A;
then consider q being Point of TOP-REAL 2 such that
A6: w2 = q and
A7: q`1 < W-bound C;
let k be set; assume
A8: k in LSeg(w1,w2);
then reconsider z = k as Point of TOP-REAL 2;
per cases by REAL_1:def 5;
suppose p`1 < q`1;
then z`1 <= w2`1 by A4,A6,A8,TOPREAL1:9;
then z`1 < W-bound C by A6,A7,AXIOMS:22;
hence k in A;
suppose q`1 < p`1;
then z`1 <= w1`1 by A4,A6,A8,TOPREAL1:9;
then z`1 < W-bound C by A4,A5,AXIOMS:22;
hence k in A;
suppose p`1 = q`1;
then z`1 = p`1 by A4,A6,A8,GOBOARD7:5;
hence k in A by A5;
end;
then reconsider A as non empty convex Subset of TOP-REAL 2 by A3;
A is connected;
hence thesis;
end;
begin :: Balls as subsets of TOP-REAL n
theorem Th47:
e = q & p in Ball(e,r) implies q`1-r < p`1 & p`1 < q`1+r
proof
assume that
A1: e = q and
A2: p in Ball(e,r);
reconsider f = p as Point of Euclid 2 by TOPREAL3:13;
A3: dist(e,f) < r by A2,METRIC_1:12;
A4: dist(e,f) = (Pitag_dist 2).(e,f) by Lm2,METRIC_1:def 1
.= sqrt ((q`1 - p`1)^2 + (q`2 - p`2)^2) by A1,TOPREAL3:12;
A5: r > 0 by A2,TBSP_1:17;
then A6: r^2 > 0 by SQUARE_1:74;
assume
A7: not thesis;
per cases by A7;
suppose q`1-r >= p`1;
then q`1-p`1 >= r by REAL_2:165;
then A8: (q`1-p`1)^2 >= r^2 by A5,SQUARE_1:77;
(q`2-p`2)^2 >= 0 by SQUARE_1:72;
then (q`1-p`1)^2 + (q`2-p`2)^2 >= (q`1-p`1)^2 + 0 by AXIOMS:24;
then (q`1-p`1)^2 + (q`2-p`2)^2 >= r^2 by A8,AXIOMS:22;
then sqrt((q`1-p`1)^2 + (q`2-p`2)^2) >= sqrt(r^2) by A6,SQUARE_1:94;
hence contradiction by A3,A4,A5,SQUARE_1:89;
suppose p`1 >= q`1+r;
then p`1-q`1 >= r by REAL_1:84;
then (p`1-q`1)^2 >= r^2 by A5,SQUARE_1:77;
then (-(q`1-p`1))^2 >= r^2 by XCMPLX_1:143;
then A9: (q`1-p`1)^2 >= r^2 by SQUARE_1:61;
(q`2-p`2)^2 >= 0 by SQUARE_1:72;
then (q`1-p`1)^2 + (q`2-p`2)^2 >= (q`1-p`1)^2 + 0 by AXIOMS:24;
then (q`1-p`1)^2 + (q`2-p`2)^2 >= r^2 by A9,AXIOMS:22;
then sqrt((q`1-p`1)^2 + (q`2-p`2)^2) >= sqrt(r^2) by A6,SQUARE_1:94;
hence contradiction by A3,A4,A5,SQUARE_1:89;
end;
theorem Th48:
e = q & p in Ball(e,r) implies q`2-r < p`2 & p`2 < q`2+r
proof
assume that
A1: e = q and
A2: p in Ball(e,r);
reconsider f = p as Point of Euclid 2 by TOPREAL3:13;
A3: dist(e,f) < r by A2,METRIC_1:12;
A4: dist(e,f) = (Pitag_dist 2).(e,f) by Lm2,METRIC_1:def 1
.= sqrt ((q`1 - p`1)^2 + (q`2 - p`2)^2) by A1,TOPREAL3:12;
A5: r > 0 by A2,TBSP_1:17;
then A6: r^2 > 0 by SQUARE_1:74;
assume
A7: not thesis;
per cases by A7;
suppose q`2-r >= p`2;
then q`2-p`2 >= r by REAL_2:165;
then A8: (q`2-p`2)^2 >= r^2 by A5,SQUARE_1:77;
(q`1-p`1)^2 >= 0 by SQUARE_1:72;
then (q`1-p`1)^2 + (q`2-p`2)^2 >= (q`2-p`2)^2 + 0 by AXIOMS:24;
then (q`1-p`1)^2 + (q`2-p`2)^2 >= r^2 by A8,AXIOMS:22;
then sqrt((q`1-p`1)^2 + (q`2-p`2)^2) >= sqrt(r^2) by A6,SQUARE_1:94;
hence contradiction by A3,A4,A5,SQUARE_1:89;
suppose p`2 >= q`2+r;
then p`2-q`2 >= r by REAL_1:84;
then (p`2-q`2)^2 >= r^2 by A5,SQUARE_1:77;
then (-(q`2-p`2))^2 >= r^2 by XCMPLX_1:143;
then A9: (q`2-p`2)^2 >= r^2 by SQUARE_1:61;
(q`1-p`1)^2 >= 0 by SQUARE_1:72;
then (q`1-p`1)^2 + (q`2-p`2)^2 >= (q`2-p`2)^2 + 0 by AXIOMS:24;
then (q`1-p`1)^2 + (q`2-p`2)^2 >= r^2 by A9,AXIOMS:22;
then sqrt((q`1-p`1)^2 + (q`2-p`2)^2) >= sqrt(r^2) by A6,SQUARE_1:94;
hence contradiction by A3,A4,A5,SQUARE_1:89;
end;
theorem Th49:
p = e implies
product ((1,2) --> (].p`1-r/sqrt 2,p`1+r/sqrt 2.[,
].p`2-r/sqrt 2,p`2+r/sqrt 2.[))
c= Ball(e,r)
proof
set A = ].p`1-r/sqrt 2,p`1+r/sqrt 2.[,
B = ].p`2-r/sqrt 2,p`2+r/sqrt 2.[,
f = (1,2) --> (A,B);
assume
A1: p = e;
let a be set;
assume a in product f;
then consider g being Function such that
A2: a = g and
A3: dom g = dom f and
A4: for x being set st x in dom f holds g.x in f.x by CARD_3:def 5;
A5: A = {m where m is Real :
p`1-r/sqrt 2 < m & m < p`1+r/sqrt 2 } by RCOMP_1:def 2;
A6: B = {n where n is Real : p`2-r/sqrt 2 < n & n < p`2+r/sqrt 2 }
by RCOMP_1:def 2;
A7: dom f = {1,2} by FUNCT_4:65;
then A8: 1 in dom f & 2 in dom f by TARSKI:def 2;
f.1 = A & f.2 = B by FUNCT_4:66;
then A9: g.1 in A & g.2 in B by A4,A8;
then consider m being Real such that
A10: m = g.1 and
p`1-r/sqrt 2 < m & m < p`1+r/sqrt 2 by A5;
consider n being Real such that
A11: n = g.2 and
p`2-r/sqrt 2 < n & n < p`2+r/sqrt 2 by A6,A9;
p`1+r/sqrt 2 > p`1-r/sqrt 2 by A9,RCOMP_1:12;
then p`1-(p`1+r/sqrt 2) < p`1-(p`1-r/sqrt 2) by REAL_1:92;
then p`1-p`1-r/sqrt 2 < p`1-(p`1-r/sqrt 2) by XCMPLX_1:36;
then p`1-p`1-r/sqrt 2 < p`1-p`1+r/sqrt 2 by XCMPLX_1:37;
then 0-r/sqrt 2 < p`1-p`1+r/sqrt 2 by XCMPLX_1:14;
then 0-r/sqrt 2 < 0+r/sqrt 2 by XCMPLX_1:14;
then -r/sqrt 2 < r/sqrt 2 by XCMPLX_1:150;
then -r/sqrt 2+r/sqrt 2 < r/sqrt 2+r/sqrt 2 by REAL_1:53;
then 0 < r/sqrt 2+r/sqrt 2 by XCMPLX_0:def 6;
then A12: 0 < (r+r)/sqrt 2 by XCMPLX_1:63;
A13: now
assume 0 >= r;
then 0+0 >= r+r by REAL_1:55;
hence contradiction by A12,Lm1,REAL_2:126;
end;
A14: dom <*g.1,g.2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
now
let k be set;
assume k in dom g;
then k = 1 or k = 2 by A3,A7,TARSKI:def 2;
hence g.k = <*g.1,g.2*>.k by FINSEQ_1:61;
end;
then a = <*g.1,g.2*> by A2,A3,A7,A14,FUNCT_1:9;
then A15: a = |[m,n]| by A10,A11,EUCLID:def 16;
then reconsider c = a as Point of TOP-REAL 2;
reconsider b = c as Point of Euclid 2 by TOPREAL3:13;
A16: 0 <= abs(m-p`1) & 0 <= abs(n-p`2) by ABSVALUE:5;
0 <= (m-p`1)^2 & 0 <= (n-p`2)^2 by SQUARE_1:72;
then A17: 0+0 <= (m-p`1)^2 + (n-p`2)^2 by REAL_1:55;
abs(m-p`1) < r/sqrt 2 & abs(n-p`2) < r/sqrt 2 by A9,A10,A11,RCOMP_1:8;
then (abs(m-p`1))^2 < (r/sqrt 2)^2 & (abs(n-p`2))^2 < (r/sqrt 2)^2
by A16,SQUARE_1:78;
then (abs(m-p`1))^2 < r^2/(sqrt 2)^2 & (abs(n-p`2))^2 < r^2/(sqrt 2)^2
by SQUARE_1:69;
then (abs(m-p`1))^2 < r^2/2 & (abs(n-p`2))^2 < r^2/2 by SQUARE_1:def 4;
then (m-p`1)^2 < r^2/2 & (n-p`2)^2 < r^2/2 by SQUARE_1:62;
then (m-p`1)^2 + (n-p`2)^2 < r^2/2 + r^2/2 by REAL_1:67;
then (m-p`1)^2 + (n-p`2)^2 < r^2 by XCMPLX_1:66;
then sqrt((m-p`1)^2 + (n-p`2)^2) < sqrt(r^2) by A17,SQUARE_1:95;
then A18: sqrt((m-p`1)^2 + (n-p`2)^2) < r by A13,SQUARE_1:89;
A19: dist(b,e) = (Pitag_dist 2).(b,e) by Lm2,METRIC_1:def 1
.= sqrt ((c`1 - p`1)^2 + (c`2 - p`2)^2) by A1,TOPREAL3:12;
c`1 = m & c`2 = n by A15,EUCLID:56;
hence a in Ball(e,r) by A18,A19,METRIC_1:12;
end;
theorem Th50:
p = e implies Ball(e,r) c= product((1,2)-->(].p`1-r,p`1+r.[,].p`2-r,p`2+r.[))
proof
set A = ].p`1-r,p`1+r.[,
B = ].p`2-r,p`2+r.[,
f = (1,2)-->(A,B);
assume that
A1: p = e;
let a be set;
assume
A2: a in Ball(e,r);
then reconsider b = a as Point of Euclid 2;
reconsider q = b as Point of TOP-REAL 2 by TOPREAL3:13;
reconsider g = q as FinSequence by EUCLID:27;
A3: dom f = {1,2} by FUNCT_4:65;
q is Function of Seg 2, REAL by EUCLID:26;
then A4: dom g = {1,2} by FINSEQ_1:4,FUNCT_2:def 1;
for x being set st x in dom f holds g.x in f.x
proof
let x be set;
assume
A5: x in dom f;
per cases by A3,A5,TARSKI:def 2;
suppose
A6: x = 1;
A7: f.1 = A by FUNCT_4:66;
A8: g.1 = q`1 by EUCLID:def 14;
p`1-r < q`1 & q`1 < p`1+r by A1,A2,Th47;
hence g.x in f.x by A6,A7,A8,JORDAN6:45;
suppose
A9: x = 2;
A10: f.2 = B by FUNCT_4:66;
A11: g.2 = q`2 by EUCLID:def 15;
p`2-r < q`2 & q`2 < p`2+r by A1,A2,Th48;
hence g.x in f.x by A9,A10,A11,JORDAN6:45;
end;
hence a in product f by A3,A4,CARD_3:18;
end;
theorem Th51:
P = Ball(e,r) & p = e implies proj1.:P = ].p`1-r,p`1+r.[
proof
assume that
A1: P = Ball(e,r) and
A2: p = e;
hereby
let a be set;
assume a in proj1.:P;
then consider x being set such that
A3: x in the carrier of TOP-REAL 2 and
A4: x in P and
A5: a = proj1.x by FUNCT_2:115;
reconsider x as Point of TOP-REAL 2 by A3;
reconsider b = a as Real by A5;
a = x`1 by A5,PSCOMP_1:def 28;
then p`1-r < b & b < p`1+r by A1,A2,A4,Th47;
hence a in ].p`1-r,p`1+r.[ by JORDAN6:45;
end;
let a be set;
assume
A6: a in ].p`1-r,p`1+r.[;
then reconsider b = a as Real;
b < p`1+r by A6,JORDAN6:45;
then b - p`1 < p`1+r - p`1 by REAL_1:54
;
then b - p`1 < p`1 - p`1 + r by XCMPLX_1:29;
then A7: b - p`1 < 0 + r by XCMPLX_1:14;
A8: a = |[b,p`2]|`1 by EUCLID:56
.= proj1.(|[b,p`2]|) by PSCOMP_1:def 28;
reconsider f = |[b,p`2]| as Point of Euclid 2 by TOPREAL3:13;
A9: dist(f,e) = (Pitag_dist 2).(f,e) by Lm2,METRIC_1:def 1
.= sqrt ((|[b,p`2]|`1 - p`1)^2 + (|[b,p`2]|`2 - p`2)^2
) by A2,TOPREAL3:12
.= sqrt ((b - p`1)^2 + (|[b,p`2]|`2 - p`2)^2) by EUCLID:56
.= sqrt ((b - p`1)^2 + (p`2 - p`2)^2) by EUCLID:56
.= sqrt ((b - p`1)^2 + 0) by SQUARE_1:60,XCMPLX_1:14;
now per cases;
case 0 <= b - p`1;
hence dist(f,e) < r by A7,A9,SQUARE_1:89;
case 0 > b - p`1;
then A10: -(b - p`1) > 0 by REAL_1:66;
A11: sqrt ((b - p`1)^2) = sqrt ((-(b - p`1))^2) by SQUARE_1:61
.= -(b - p`1) by A10,SQUARE_1:89;
p`1 - r < b by A6,JORDAN6:45;
then p`1 - r + r < b + r by REAL_1:53;
then p`1 - (r - r) < b + r by XCMPLX_1:37;
then p`1 - 0 < b + r by XCMPLX_1:14;
then p`1 - b < r + b - b by REAL_1:54
;
then p`1 - b < r + (b - b) by XCMPLX_1:29;
then p`1 - b < r + 0 by XCMPLX_1:14;
hence dist(f,e) < r by A9,A11,XCMPLX_1:143;
end;
then |[b,p`2]| in P by A1,METRIC_1:12;
hence a in proj1.:P by A8,FUNCT_2:43;
end;
theorem Th52:
P = Ball(e,r) & p = e implies proj2.:P = ].p`2-r,p`2+r.[
proof
assume that
A1: P = Ball(e,r) and
A2: p = e;
hereby
let a be set;
assume a in proj2.:P;
then consider x being set such that
A3: x in the carrier of TOP-REAL 2 and
A4: x in P and
A5: a = proj2.x by FUNCT_2:115;
reconsider x as Point of TOP-REAL 2 by A3;
reconsider b = a as Real by A5;
a = x`2 by A5,PSCOMP_1:def 29;
then p`2-r < b & b < p`2+r by A1,A2,A4,Th48;
hence a in ].p`2-r,p`2+r.[ by JORDAN6:45;
end;
let a be set;
assume
A6: a in ].p`2-r,p`2+r.[;
then reconsider b = a as Real;
b < p`2+r by A6,JORDAN6:45;
then b - p`2 < p`2+r - p`2 by REAL_1:54
;
then b - p`2 < p`2 - p`2 + r by XCMPLX_1:29;
then A7: b - p`2 < 0 + r by XCMPLX_1:14;
A8: a = |[p`1,b]|`2 by EUCLID:56
.= proj2.(|[p`1,b]|) by PSCOMP_1:def 29;
reconsider f = |[p`1,b]| as Point of Euclid 2 by TOPREAL3:13;
A9: dist(f,e) = (Pitag_dist 2).(f,e) by Lm2,METRIC_1:def 1
.= sqrt ((|[p`1,b]|`1 - p`1)^2 + (|[p`1,b]|`2 - p`2)^2
) by A2,TOPREAL3:12
.= sqrt ((p`1 - p`1)^2 + (|[p`1,b]|`2 - p`2)^2) by EUCLID:56
.= sqrt ((p`1 - p`1)^2 + (b - p`2)^2) by EUCLID:56
.= sqrt (0 + (b - p`2)^2) by SQUARE_1:60,XCMPLX_1:14;
now per cases;
case 0 <= b - p`2;
hence dist(f,e) < r by A7,A9,SQUARE_1:89;
case 0 > b - p`2;
then A10: -(b - p`2) > 0 by REAL_1:66;
A11: sqrt ((b - p`2)^2) = sqrt ((-(b - p`2))^2) by SQUARE_1:61
.= -(b - p`2) by A10,SQUARE_1:89;
p`2 - r < b by A6,JORDAN6:45;
then p`2 - r + r < b + r by REAL_1:53;
then p`2 - (r - r) < b + r by XCMPLX_1:37;
then p`2 - 0 < b + r by XCMPLX_1:14;
then p`2 - b < r + b - b by REAL_1:54
;
then p`2 - b < r + (b - b) by XCMPLX_1:29;
then p`2 - b < r + 0 by XCMPLX_1:14;
hence dist(f,e) < r by A9,A11,XCMPLX_1:143;
end;
then |[p`1,b]| in P by A1,METRIC_1:12;
hence a in proj2.:P by A8,FUNCT_2:43;
end;
theorem
D = Ball(e,r) & p = e implies W-bound D = p`1 - r
proof
assume that
A1: D = Ball(e,r) and
A2: p = e;
A3: r > 0 by A1,TBSP_1:17;
then A4: p`1-r < p`1-0 by REAL_1:92;
p`1+0 < p`1+r by A3,REAL_1:53;
then p`1-r < p`1+r by A4,AXIOMS:22;
then A5: inf ].p`1-r,p`1+r.[ = p`1-r by Th22;
proj1.:D = ].p`1-r,p`1+r.[ by A1,A2,Th51;
hence W-bound D = p`1 - r by A5,SPRECT_1:48;
end;
theorem
D = Ball(e,r) & p = e implies E-bound D = p`1 + r
proof
assume that
A1: D = Ball(e,r) and
A2: p = e;
A3: r > 0 by A1,TBSP_1:17;
then A4: p`1-r < p`1-0 by REAL_1:92;
p`1+0 < p`1+r by A3,REAL_1:53;
then p`1-r < p`1+r by A4,AXIOMS:22;
then A5: sup ].p`1-r,p`1+r.[ = p`1+r by Th22;
proj1.:D = ].p`1-r,p`1+r.[ by A1,A2,Th51;
hence E-bound D = p`1 + r by A5,SPRECT_1:51;
end;
theorem
D = Ball(e,r) & p = e implies S-bound D = p`2 - r
proof
assume that
A1: D = Ball(e,r) and
A2: p = e;
A3: r > 0 by A1,TBSP_1:17;
then A4: p`2-r < p`2-0 by REAL_1:92;
p`2+0 < p`2+r by A3,REAL_1:53;
then p`2-r < p`2+r by A4,AXIOMS:22;
then A5: inf ].p`2-r,p`2+r.[ = p`2-r by Th22;
proj2.:D = ].p`2-r,p`2+r.[ by A1,A2,Th52;
hence S-bound D = p`2 - r by A5,SPRECT_1:49;
end;
theorem
D = Ball(e,r) & p = e implies N-bound D = p`2 + r
proof
assume that
A1: D = Ball(e,r) and
A2: p = e;
A3: r > 0 by A1,TBSP_1:17;
then A4: p`2-r < p`2-0 by REAL_1:92;
p`2+0 < p`2+r by A3,REAL_1:53;
then p`2-r < p`2+r by A4,AXIOMS:22;
then A5: sup ].p`2-r,p`2+r.[ = p`2+r by Th22;
proj2.:D = ].p`2-r,p`2+r.[ by A1,A2,Th52;
hence N-bound D = p`2 + r by A5,SPRECT_1:50;
end;
theorem
D = Ball(e,r) implies D is non horizontal
proof
assume
A1: D = Ball(e,r);
reconsider p = e as Point of TOP-REAL 2 by TOPREAL3:13;
take p, q = |[p`1,p`2-r/2]|;
reconsider f = q as Point of Euclid 2 by TOPREAL3:13;
A2: r > 0 by A1,TBSP_1:17;
then A3: r/2 > 0 by REAL_2:127;
thus p in D by A1,A2,TBSP_1:16;
dist(e,f) = (Pitag_dist 2).(e,f) by Lm2,METRIC_1:def 1
.= sqrt ((p`1 - q`1)^2 + (p`2 - q`2)^2) by TOPREAL3:12
.= sqrt ((p`1 - p`1)^2 + (p`2 - q`2)^2) by EUCLID:56
.= sqrt ((p`1 - p`1)^2 + (p`2 - (p`2-r/2))^2) by EUCLID:56
.= sqrt (0 + (p`2 - (p`2-r/2))^2) by SQUARE_1:60,XCMPLX_1:14
.= sqrt ((p`2 - p`2 + r/2)^2) by XCMPLX_1:37
.= sqrt ((0 + r/2)^2) by XCMPLX_1:14
.= r/2 by A3,SQUARE_1:89;
then dist(e,f) < r by A2,SEQ_2:4;
hence q in D by A1,METRIC_1:12;
p`2-r/2 < p`2-0 by A3,REAL_1:92; hence p`2 <> q`2 by EUCLID:56;
end;
theorem
D = Ball(e,r) implies D is non vertical
proof
assume
A1: D = Ball(e,r);
reconsider p = e as Point of TOP-REAL 2 by TOPREAL3:13;
take p, q = |[p`1-r/2,p`2]|;
reconsider f = q as Point of Euclid 2 by TOPREAL3:13;
A2: r > 0 by A1,TBSP_1:17;
then A3: r/2 > 0 by REAL_2:127;
thus p in D by A1,A2,TBSP_1:16;
dist(e,f) = (Pitag_dist 2).(e,f) by Lm2,METRIC_1:def 1
.= sqrt ((p`1 - q`1)^2 + (p`2 - q`2)^2) by TOPREAL3:12
.= sqrt ((p`1 - (p`1-r/2))^2 + (p`2 - q`2)^2) by EUCLID:56
.= sqrt ((p`1 - (p`1-r/2))^2 + (p`2 - p`2)^2) by EUCLID:56
.= sqrt ((p`1 - (p`1-r/2))^2 + 0) by SQUARE_1:60,XCMPLX_1:14
.= sqrt ((p`1 - p`1 + r/2)^2) by XCMPLX_1:37
.= sqrt ((0 + r/2)^2) by XCMPLX_1:14
.= r/2 by A3,SQUARE_1:89;
then dist(e,f) < r by A2,SEQ_2:4;
hence q in D by A1,METRIC_1:12;
p`1-r/2 < p`1-0 by A3,REAL_1:92; hence p`1 <> q`1 by EUCLID:56;
end;
theorem
for f being Point of Euclid 2, x being Point of TOP-REAL 2 st
x in Ball(f,a) holds not |[x`1-2*a,x`2]| in Ball(f,a)
proof
let f be Point of Euclid 2,
x be Point of TOP-REAL 2 such that
A1: x in Ball(f,a);
set p = |[x`1-2*a,x`2]|;
reconsider z = p, X = x as Point of Euclid 2 by TOPREAL3:13;
A2: dist(f,X) < a by A1,METRIC_1:12;
a > 0 by A1,TBSP_1:17;
then A3: 2*a > 2*0 by REAL_1:70;
A4: dist(X,z) = (Pitag_dist 2).(X,z) by Lm2,METRIC_1:def 1
.= sqrt ((x`1 - p`1)^2 + (x`2 - p`2)^2) by TOPREAL3:12
.= sqrt ((x`1 - (x`1-2*a))^2 + (x`2 - p`2)^2) by EUCLID:56
.= sqrt ((x`1 - (x`1-2*a))^2 + (x`2 - x`2)^2) by EUCLID:56
.= sqrt ((x`1 - x`1 + 2*a)^2 + (x`2 - x`2)^2) by XCMPLX_1:37
.= sqrt ((x`1 - x`1)^2 + 2*(x`1 - x`1)*(2*a) + (2*a)^2 + (x`2 - x`2)^2)
by SQUARE_1:63
.= sqrt (0^2 + 2*(x`1 - x`1)*(2*a) + (2*a)^2 + (x`2 - x`2)^2
) by XCMPLX_1:14
.= sqrt (0^2 + 2*0 * (2*a) + (2*a)^2 + (x`2 - x`2)^2) by XCMPLX_1:14
.= sqrt ((2*a)^2) by SQUARE_1:60,XCMPLX_1:14
.= 2*a by A3,SQUARE_1:89;
assume |[x`1-2*a,x`2]| in Ball(f,a);
then dist(f,z) < a by METRIC_1:12;
then dist(f,X) + dist(f,z) < a + a by A2,REAL_1:67;
then dist(f,X) + dist(f,z) < 2*a by XCMPLX_1:11;
hence contradiction by A4,METRIC_1:4;
end;
theorem
for X being non empty compact Subset of TOP-REAL 2,
p being Point of Euclid 2 st p = 0.REAL 2 & a > 0 holds
X c= Ball(p, abs(E-bound X)+abs(N-bound X)+abs(W-bound X)+abs(S-bound X)+a)
proof
let X be non empty compact Subset of TOP-REAL 2,
p be Point of Euclid 2 such that
A1: p = 0.REAL 2 and
A2: a > 0;
let x be set; assume
A3: x in X;
then reconsider b = x as Point of Euclid 2 by TOPREAL3:13;
set A = X,
n = N-bound A, s = S-bound A, e = E-bound A, w = W-bound A,
r = abs(e)+abs(n)+abs(w)+abs(s)+a;
reconsider P = p, B = b as Point of TOP-REAL 2 by TOPREAL3:13;
A4: w <= B`1 & B`1 <= e & s <= B`2 & B`2 <= n by A3,PSCOMP_1:71;
A5: P`1 = 0 & P`2 = 0 by A1,Th32;
A6: dist(p,b) = (Pitag_dist 2).(p,b) by Lm2,METRIC_1:def 1
.= sqrt ((P`1 - B`1)^2 + (P`2 - B`2)^2) by TOPREAL3:12
.= sqrt ((- B`1)^2 + (P`2 - B`2)^2) by A5,XCMPLX_1:150
.= sqrt ((- B`1)^2 + (- B`2)^2) by A5,XCMPLX_1:150
.= sqrt ((B`1)^2 + (- B`2)^2) by SQUARE_1:61
.= sqrt ((B`1)^2 + (B`2)^2) by SQUARE_1:61;
0 <= (B`1)^2 & 0 <= (B`2)^2 by SQUARE_1:72;
then sqrt ((B`1)^2 + (B`2)^2) <= sqrt(B`1)^2 + sqrt(B`2)^2 by Th6;
then sqrt ((B`1)^2 + (B`2)^2) <= abs(B`1) + sqrt(B`2)^2 by SQUARE_1:91;
then A7: sqrt ((B`1)^2 + (B`2)^2) <= abs(B`1) + abs(B`2) by SQUARE_1:91;
A8: 0 <= abs(s) by ABSVALUE:5;
A9: 0 <= abs(w) by ABSVALUE:5;
A10: 0 <= abs(e) by ABSVALUE:5;
A11: 0 <= abs(n) by ABSVALUE:5;
A12: abs(e) + abs(n) + abs(w) + abs(s) + 0 <
abs(e) + abs(n) + abs(w) + abs(s) + a
by A2,REAL_1:67;
now per cases;
case B`1 >= 0 & B`2 >= 0;
then abs(B`1) <= abs(e) & abs(B`2) <= abs(n) by A4,Th7;
then abs(B`1) + abs(B`2) <= abs(e) + abs(n) by REAL_1:55;
then A13: dist(p,b) <= abs(e) + abs(n) by A6,A7,AXIOMS:22;
abs(e) + abs(n) + 0 <= abs(e) + abs(n) + abs(w) by A9,REAL_1:55;
then abs(e) + abs(n) <= abs(e) + abs(n) + abs(w) + abs(s)
by A8,REAL_1:55;
then abs(e) + abs(n) < r by A12,AXIOMS:22;
hence dist(p,b) < r by A13,AXIOMS:22;
case B`1 < 0 & B`2 >= 0;
then abs(B`1) <= abs(w) & abs(B`2) <= abs(n) by A4,Th7,Th8;
then abs(B`1) + abs(B`2) <= abs(w) + abs(n) by REAL_1:55;
then A14: dist(p,b) <= abs(w) + abs(n) by A6,A7,AXIOMS:22;
0 + (abs(n) + abs(w)) <= abs(e) + (abs(n) + abs(w))
by A10,REAL_1:55;
then A15: abs(n) + abs(w) <= abs(e) + abs(n) + abs(w) by XCMPLX_1:1;
abs(e) + abs(n) + abs(w) + 0 <= abs(e) + abs(n) + abs(w) + abs(s)
by A8,REAL_1:55;
then abs(w) + abs(n) <= abs(e) + abs(n) + abs(w) + abs(s)
by A15,AXIOMS:22;
then abs(w) + abs(n) < r by A12,AXIOMS:22;
hence dist(p,b) < r by A14,AXIOMS:22;
case B`1 >= 0 & B`2 < 0;
then abs(B`1) <= abs(e) & abs(B`2) <= abs(s) by A4,Th7,Th8;
then abs(B`1) + abs(B`2) <= abs(e) + abs(s) by REAL_1:55;
then A16: dist(p,b) <= abs(e) + abs(s) by A6,A7,AXIOMS:22;
abs(e) + abs(s) + 0 <= abs(e) + abs(s) + abs(n) by A11,REAL_1:55;
then A17: abs(e) + abs(s) <= abs(e) + abs(n) + abs(s) by XCMPLX_1:1;
abs(e) + abs(n) + abs(s) + 0 <= abs(e) + abs(n) + abs(s) + abs(w)
by A9,REAL_1:55;
then abs(e) + abs(n) + abs(s) <= abs(e) + abs(n) + abs(w) + abs(s)
by XCMPLX_1:1;
then abs(e) + abs(s) <= abs(e) + abs(n) + abs(w) + abs(s)
by A17,AXIOMS:22;
then abs(e) + abs(s) < r by A12,AXIOMS:22;
hence dist(p,b) < r by A16,AXIOMS:22;
case B`1 < 0 & B`2 < 0;
then abs(B`1) <= abs(w) & abs(B`2) <= abs(s) by A4,Th8;
then abs(B`1) + abs(B`2) <= abs(w) + abs(s) by REAL_1:55;
then A18: dist(p,b) <= abs(w) + abs(s) by A6,A7,AXIOMS:22;
0 + 0 <= abs(e) + abs(n) by A10,A11,REAL_1:55;
then 0 + (abs(w) + abs(s)) <= abs(e) + abs(n) + (abs(w) + abs(s))
by REAL_1:55;
then abs(w) + abs(s) <= abs(e) + abs(n) + abs(w) + abs(s) by XCMPLX_1:1;
then abs(w) + abs(s) < r by A12,AXIOMS:22;
hence dist(p,b) < r by A18,AXIOMS:22;
end;
hence x in Ball(p,r) by METRIC_1:12;
end;
theorem Th61:
for M being Reflexive symmetric triangle (non empty MetrStruct),
z being Point of M holds
r < 0 implies Sphere(z,r) = {}
proof
let M be Reflexive symmetric triangle (non empty MetrStruct),
z be Point of M;
assume
A1: r < 0;
thus Sphere(z,r) c= {}
proof
let a be set;
assume
A2: a in Sphere(z,r);
then reconsider b = a as Point of M;
dist(b,z) = r by A2,METRIC_1:14;
hence a in {} by A1,METRIC_1:5;
end;
thus thesis by XBOOLE_1:2;
end;
theorem
for M being Reflexive discerning (non empty MetrStruct),
z being Point of M holds
Sphere(z,0) = {z}
proof
let M be Reflexive discerning (non empty MetrStruct),
z be Point of M;
thus Sphere(z,0) c= {z}
proof
let a be set;
assume
A1: a in Sphere(z,0);
then reconsider b = a as Point of M;
dist(z,b) = 0 by A1,METRIC_1:14;
then b = z by METRIC_1:2;
hence a in {z} by TARSKI:def 1;
end;
let a be set;
assume a in {z};
then A2: a = z by TARSKI:def 1;
dist(z,z) = 0 by METRIC_1:1;
hence thesis by A2,METRIC_1:14;
end;
theorem Th63:
for M being Reflexive symmetric triangle (non empty MetrStruct),
z being Point of M holds
r < 0 implies cl_Ball(z,r) = {}
proof
let M be Reflexive symmetric triangle (non empty MetrStruct),
z be Point of M;
assume r < 0;
then A1: Ball(z,r) = {} & Sphere(z,r) = {} by Th61,TBSP_1:17;
Sphere(z,r) \/ Ball(z,r) = cl_Ball(z,r) by METRIC_1:17;
hence cl_Ball(z,r) = {} by A1;
end;
theorem Th64:
cl_Ball(z,0) = {z}
proof
thus cl_Ball(z,0) c= {z}
proof
let a be set;
assume
A1: a in cl_Ball(z,0);
then reconsider b = a as Point of M;
dist(b,z) <= 0 & dist(b,z) >= 0 by A1,METRIC_1:5,13;
then dist(b,z) = 0;
then b = z by METRIC_1:2;
hence a in {z} by TARSKI:def 1;
end;
let a be set;
assume a in {z};
then A2: a = z by TARSKI:def 1;
dist(z,z) = 0 by METRIC_1:1;
hence thesis by A2,METRIC_1:13;
end;
Lm3:
for A being Subset of TopSpaceMetr M st A = cl_Ball(z,r) holds
A` is open
proof
let A be Subset of TopSpaceMetr M such that
A1: A = cl_Ball(z,r);
for x being set holds x in A` iff
ex Q being Subset of TopSpaceMetr M st Q is open & Q c= A` & x in Q
proof
let x be set;
thus x in A` implies ex Q being Subset of TopSpaceMetr M st
Q is open & Q c= A` & x in Q
proof
assume
A2: x in A`;
then reconsider e = x as Point of M by TOPMETR:16;
the carrier of M = the carrier of TopSpaceMetr M by TOPMETR:16;
then reconsider Q = Ball(e,dist(e,z)-r) as Subset of TopSpaceMetr M
;
take Q;
thus Q is open by TOPMETR:21;
thus Q c= A`
proof
let q be set;
assume
A3: q in Q;
then reconsider f = q as Point of M;
A4: dist(e,f) < dist(e,z)-r by A3,METRIC_1:12;
dist(e,z) <= dist(e,f) + dist(f,z) by METRIC_1:4;
then dist(e,z) - r <= dist(e,f) + dist(f,z) - r by REAL_1:49;
then dist(e,f) < dist(e,f) + dist(f,z) - r by A4,AXIOMS:22;
then dist(e,f) - dist(e,f) < dist(e,f) + dist(f,z) - r - dist(e,f)
by REAL_1:54;
then 0 < dist(e,f) + dist(f,z) - r - dist(e,f) by XCMPLX_1:14;
then 0 < dist(e,f) + dist(f,z) - dist(e,f) - r by XCMPLX_1:21;
then 0 < dist(e,f) - dist(e,f) + dist(f,z) - r by XCMPLX_1:29;
then 0 < 0 + dist(f,z) - r by XCMPLX_1:14;
then dist(f,z) > r by REAL_2:106;
then not q in A by A1,METRIC_1:13;
then q in A` by A3,SUBSET_1:50;
hence thesis;
end;
x in A` by A2;
then not x in A by SUBSET_1:54;
then dist(z,e) > r by A1,METRIC_1:13;
then dist(e,z)-r > r-r by REAL_1:54;
then dist(e,z)-r > 0 by XCMPLX_1:14;
hence x in Q by TBSP_1:16;
end;
thus thesis;
end;
hence A` is open by TOPS_1:57;
end;
theorem Th65:
for A being Subset of TopSpaceMetr M st A = cl_Ball(z,r) holds
A is closed
proof
let A be Subset of TopSpaceMetr M;
assume A = cl_Ball(z,r);
then A` is open by Lm3;
hence A is closed by TOPS_1:29;
end;
theorem Th66:
A = cl_Ball(w,r) implies A is closed
proof
TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
hence thesis by Th65;
end;
theorem Th67:
cl_Ball(z,r) is bounded
proof
per cases;
suppose
A1: r > 0;
take r+1,z;
r+1 > 0+1 by A1,REAL_1:53;
hence 0 < r+1 by AXIOMS:22;
let a be set;
assume
A2: a in cl_Ball(z,r);
then reconsider e = a as Point of M;
A3: dist(e,z) <= r by A2,METRIC_1:13;
r+0 < r+1 by REAL_1:53;
then dist(e,z) < r+1 by A3,AXIOMS:22;
hence a in Ball(z,r+1) by METRIC_1:12;
suppose
A4: r < 0;
{}M is bounded by TBSP_1:14;
hence thesis by A4,Th63;
suppose r = 0;
then cl_Ball(z,r) = {z} by Th64;
hence thesis by TBSP_1:22;
end;
theorem Th68:
for A being Subset of TopSpaceMetr M st A = Sphere(z,r) holds A is closed
proof
let A be Subset of TopSpaceMetr M such that
A1: A = Sphere(z,r);
A2: the carrier of M = the carrier of TopSpaceMetr M by TOPMETR:16;
then reconsider B = cl_Ball(z,r), C = Ball(z,r) as Subset of TopSpaceMetr M
;
A3: (cl_Ball(z,r))` = B` by A2;
A4: A` = B` \/ C
proof
hereby
let a be set;
assume
A5: a in A`;
then reconsider e = a as Point of M by TOPMETR:16;
a in A` by A5;
then not a in A by SUBSET_1:54;
then dist(e,z) <> r by A1,METRIC_1:14;
then dist(e,z) < r or dist(e,z) > r by REAL_1:def 5;
then e in Ball(z,r) or not e in
cl_Ball(z,r) by METRIC_1:12,13;
then e in Ball(z,r) or e in cl_Ball(z,r)` by SUBSET_1:50;
then e in Ball(z,r) or e in (cl_Ball(z,r))`;
hence a in B` \/ C by A3,XBOOLE_0:def 2;
end;
let a be set;
assume
A6: a in B` \/ C;
then reconsider e = a as Point of M by TOPMETR:16;
a in B` or a in C by A6,XBOOLE_0:def 2;
then e in cl_Ball(z,r)` or e in C by A3;
then not e in cl_Ball(z,r) or e in C by SUBSET_1:54;
then dist(e,z) > r or dist(e,z) < r by METRIC_1:12,13;
then not a in A by A1,METRIC_1:14;
then a in A` by A6,SUBSET_1:50;
hence a in A`;
end;
B` is open & C is open by Lm3,TOPMETR:21;
then A` is open by A4,TOPS_1:37;
hence A is closed by TOPS_1:29;
end;
theorem
A = Sphere(w,r) implies A is closed
proof
TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
hence thesis by Th68;
end;
theorem
Sphere(z,r) is bounded
proof
A1: Sphere(z,r) c= cl_Ball(z,r) by METRIC_1:16;
cl_Ball(z,r) is bounded by Th67;
hence thesis by A1,TBSP_1:21;
end;
theorem Th71:
A is Bounded implies Cl A is Bounded
proof
given C being Subset of Euclid n such that
A1: C = A and
A2: C is bounded;
consider r being Real, x being Point of Euclid n such that
0 < r and
A3: C c= Ball(x,r) by A2,METRIC_6:def 10;
A4: Ball(x,r) c= cl_Ball(x,r) by METRIC_1:15;
Cl A is Subset of Euclid n by TOPREAL3:13;
then reconsider D = Cl A as Subset of Euclid n;
take D;
thus D = Cl A;
cl_Ball(x,r) is Subset of TOP-REAL n by TOPREAL3:13;
then reconsider B = cl_Ball(x,r) as Subset of TOP-REAL n;
A5: B is closed by Th66;
A6: cl_Ball(x,r) is bounded by Th67;
A c= B by A1,A3,A4,XBOOLE_1:1;
then Cl A c= Cl B by PRE_TOPC:49;
then Cl A c= B by A5,PRE_TOPC:52;
hence D is bounded by A6,TBSP_1:21;
end;
theorem
for M being non empty MetrStruct holds
M is bounded iff
for X being Subset of M holds X is bounded
proof
let M be non empty MetrStruct;
hereby
assume M is bounded;
then A1: [#]M is bounded by TBSP_1:25;
let X be Subset of M;
X c= [#]M by PRE_TOPC:14;
hence X is bounded by A1,TBSP_1:21;
end;
assume for X being Subset of M holds X is bounded;
then [#]M is bounded;
hence thesis by TBSP_1:25;
end;
theorem Th73:
for M being Reflexive symmetric triangle (non empty MetrStruct),
X, Y being Subset of M st
the carrier of M = X \/ Y & M is non bounded & X is bounded
holds Y is non bounded
proof
let M be Reflexive symmetric triangle (non empty MetrStruct),
X, Y be Subset of M such that
A1: the carrier of M = X \/ Y and
A2: M is non bounded;
A3: [#]M = X \/ Y by A1,PRE_TOPC:12;
assume X is bounded & Y is bounded;
then [#]M is bounded by A3,TBSP_1:20;
hence thesis by A2,TBSP_1:25;
end;
theorem
for X, Y being Subset of TOP-REAL n st
n >= 1 & the carrier of TOP-REAL n = X \/ Y & X is Bounded holds
Y is non Bounded
proof
set M = TOP-REAL n;
let X, Y be Subset of M such that
A1: n >= 1 and
A2: the carrier of M = X \/ Y;
assume X is Bounded;
then consider C being Subset of Euclid n such that
A3: C = X & C is bounded by JORDAN2C:def 2;
reconsider D = Y as Subset of Euclid n by TOPREAL3:13;
A4: the carrier of Euclid n = C \/ D by A2,A3,TOPREAL3:13;
[#]M is Subset of Euclid n by TOPREAL3:13;
then reconsider E = [#]M as Subset of Euclid n;
A5: E = the carrier of M by PRE_TOPC:def 3
.= the carrier of Euclid n by TOPREAL3:13
.= [#]Euclid n by PRE_TOPC:def 3;
[#](TOP-REAL n) is non Bounded by A1,JORDAN2C:41;
then E is non bounded by JORDAN2C:def 2;
then Euclid n is non bounded by A5,TBSP_1:25;
then for D being Subset of Euclid n holds
D <> Y or D is non bounded by A3,A4,Th73;
hence thesis by JORDAN2C:def 2;
end;
canceled;
theorem
A is Bounded & B is Bounded implies A \/ B is Bounded
proof
given C being Subset of Euclid n such that
A1: C = A & C is bounded;
given D being Subset of Euclid n such that
A2: D = B & D is bounded;
reconsider E = C \/ D as Subset of Euclid n;
take E;
thus thesis by A1,A2,TBSP_1:20;
end;
begin :: Topological properties of real numbers subsets
definition let X be non empty Subset of REAL;
cluster Cl X -> non empty;
coherence
proof
X c= Cl X by PSCOMP_1:33;
hence thesis by XBOOLE_1:3;
end;
end;
definition let D be bounded_below Subset of REAL;
cluster Cl D -> bounded_below;
coherence
proof
consider p being real number such that
A1: for r being real number st r in D holds p <= r by SEQ_4:def 2;
take p;
let r be real number;
assume r in Cl D;
then consider s being Real_Sequence such that
A2: rng s c= D and
A3: s is convergent & lim s = r by PSCOMP_1:39;
for n holds s.n >= p
proof
let n;
dom s = NAT by FUNCT_2:def 1;
then s.n in rng s by FUNCT_1:def 5;
hence s.n >= p by A1,A2;
end;
hence p <= r by A3,PREPOWER:2;
end;
end;
definition let D be bounded_above Subset of REAL;
cluster Cl D -> bounded_above;
coherence
proof
consider p being real number such that
A1: for r being real number st r in D holds r <= p by SEQ_4:def 1;
take p;
let r be real number;
assume r in Cl D;
then consider s being Real_Sequence such that
A2: rng s c= D and
A3: s is convergent & lim s = r by PSCOMP_1:39;
for n holds s.n <= p
proof
let n;
dom s = NAT by FUNCT_2:def 1;
then s.n in rng s by FUNCT_1:def 5;
hence s.n <= p by A1,A2;
end;
hence p >= r by A3,PREPOWER:3;
end;
end;
theorem Th77:
for D being non empty bounded_below Subset of REAL holds inf D = inf Cl D
proof
let D be non empty bounded_below Subset of REAL;
D c= Cl D by PSCOMP_1:33;
then A1: inf Cl D <= inf D by PSCOMP_1:12;
A2: for p being real number st p in D holds p >= inf Cl D
proof
let p be real number;
assume p in D;
then inf D <= p by SEQ_4:def 5;
hence thesis by A1,AXIOMS:22;
end;
for q being real number st
for p being real number st p in D holds p >= q
holds inf Cl D >= q
proof
let q be real number such that
A3: for p being real number st p in D holds p >= q;
for p being real number st p in Cl D holds p >= q
proof
let p be real number; assume
p in Cl D;
then consider s being Real_Sequence such that
A4: rng s c= D and
A5: s is convergent & lim s = p by PSCOMP_1:39;
for n holds s.n >= q
proof
let n;
dom s = NAT by FUNCT_2:def 1;
then s.n in rng s by FUNCT_1:def 5;
hence s.n >= q by A3,A4;
end;
hence p >= q by A5,PREPOWER:2;
end;
hence inf Cl D >= q by PSCOMP_1:8;
end;
hence thesis by A2,PSCOMP_1:9;
end;
theorem Th78:
for D being non empty bounded_above Subset of REAL holds sup D = sup Cl D
proof
let D be non empty bounded_above Subset of REAL;
D c= Cl D by PSCOMP_1:33;
then A1: sup Cl D >= sup D by PSCOMP_1:13;
A2: for p being real number st p in D holds p <= sup Cl D
proof
let p be real number;
assume p in D;
then sup D >= p by SEQ_4:def 4;
hence thesis by A1,AXIOMS:22;
end;
for q being real number st
for p being real number st p in D holds p <= q
holds sup Cl D <= q
proof
let q be real number such that
A3: for p being real number st p in D holds p <= q;
for p being real number st p in Cl D holds p <= q
proof
let p be real number; assume
p in Cl D;
then consider s being Real_Sequence such that
A4: rng s c= D and
A5: s is convergent & lim s = p by PSCOMP_1:39;
for n holds s.n <= q
proof
let n;
dom s = NAT by FUNCT_2:def 1;
then s.n in rng s by FUNCT_1:def 5;
hence s.n <= q by A3,A4;
end;
hence p <= q by A5,PREPOWER:3;
end;
hence sup Cl D <= q by PSCOMP_1:10;
end;
hence thesis by A2,PSCOMP_1:11;
end;
definition
cluster R^1 -> being_T2;
coherence by PCOMPS_1:38,TOPMETR:def 7;
end;
Lm4:
R^1 = TopStruct (#the carrier of RealSpace,Family_open_set RealSpace#)
by PCOMPS_1:def 6,TOPMETR:def 7;
theorem Th79:
for A being Subset of REAL, B being Subset of R^1 st A = B holds
A is closed iff B is closed
proof
let A be Subset of REAL,
B be Subset of R^1 such that
A1: A = B;
thus A is closed implies B is closed
proof
assume A is closed;
then A`` is closed;
then A` is open by RCOMP_1:def 5;
then A` in Family_open_set RealSpace by JORDAN5A:6;
then B` in the topology of R^1 by A1,Lm4,TOPMETR:24;
then [#]R^1 \ B in the topology of R^1 by PRE_TOPC:17;
hence [#]R^1 \ B is open by PRE_TOPC:def 5;
end;
assume B is closed;
then B` is open by TOPS_1:29;
then B` in the topology of R^1 by PRE_TOPC:def 5;
then B` in the topology of R^1;
then A` is open by A1,Lm4,JORDAN5A:6,TOPMETR:24;
then A`` is closed by RCOMP_1:def 5;
hence A is closed;
end;
theorem
for A being Subset of REAL, B being Subset of R^1 st A = B holds Cl A = Cl B
proof
let A be Subset of REAL,
B be Subset of R^1 such that
A1: A = B;
thus Cl A c= Cl B
proof
let a be set;
assume
A2: a in Cl A;
for G being Subset of R^1 st G is open & a in G holds B meets G
proof
let G be Subset of R^1 such that
A3: G is open and
A4: a in G;
A5: G in Family_open_set RealSpace by A3,Lm4,PRE_TOPC:def 5;
reconsider H = G as Subset of REAL by TOPMETR:24;
H is open by A5,JORDAN5A:6;
then A /\ H is non empty by A2,A4,PSCOMP_1:38;
hence B meets G by A1,XBOOLE_0:def 7;
end;
hence a in Cl B by A2,PRE_TOPC:def 13,TOPMETR:24;
end;
let a be set;
assume
A6: a in Cl B;
for O being open Subset of REAL st a in O holds O /\ A is non empty
proof
let O be open Subset of REAL such that
A7: a in O;
reconsider P = O as Subset of R^1 by TOPMETR:24;
P in Family_open_set RealSpace by JORDAN5A:6;
then P is open by Lm4,PRE_TOPC:def 5;
then P meets B by A6,A7,PRE_TOPC:def 13;
hence O /\ A is non empty by A1,XBOOLE_0:def 7;
end;
hence thesis by A6,PSCOMP_1:38,TOPMETR:24;
end;
theorem Th81:
for A being Subset of REAL, B being Subset of R^1 st A = B holds
A is compact iff B is compact
proof
let A be Subset of REAL,
B be Subset of R^1 such that
A1: A = B;
thus A is compact implies B is compact
proof
assume
A2: A is compact;
per cases;
suppose A = {};
then reconsider C = B as empty Subset of R^1 by A1;
C is compact;
hence B is compact;
suppose
A3: A <> {};
reconsider X = [.inf A,sup A.] as Subset of R^1
by TOPMETR:24;
A is closed by A2,RCOMP_1:26;
then A4: B is closed by A1,Th79;
A5: A is bounded by A2,RCOMP_1:28;
then A6: A c= [.inf A,sup A.] by Th24;
A7: inf A <= sup A by A3,A5,SEQ_4:24;
then A8: Closed-Interval-TSpace(inf A,sup A) is compact by HEINE:11;
A9: X = {} or X <> {};
Closed-Interval-TSpace(inf A,sup A) = R^1|X by A7,TOPMETR:26;
then X is compact by A8,A9,COMPTS_1:12;
hence B is compact by A1,A4,A6,COMPTS_1:18;
end;
assume B is compact;
then [#]B is compact by WEIERSTR:19;
hence A is compact by A1,WEIERSTR:def 3;
end;
definition
cluster finite -> compact Subset of REAL;
coherence
proof
let A be Subset of REAL;
assume A is finite;
then reconsider B = A as finite Subset of R^1 by TOPMETR:24;
B is compact;
hence A is compact by Th81;
end;
end;
definition let a, b be real number;
cluster [.a,b.] -> compact;
coherence by RCOMP_1:24;
end;
theorem
for a, b being real number holds a <> b iff Cl ].a,b.[ = [.a,b.]
proof
let a, b be real number;
thus a <> b implies Cl ].a,b.[ = [.a,b.]
proof
assume
A1: a <> b;
reconsider a1 = a, b1 = b as Real by XREAL_0:def 1;
per cases by A1,REAL_1:def 5;
suppose
A2: a > b;
hence Cl ].a,b.[ = {} by PSCOMP_1:35,RCOMP_1:12
.= [.a,b.] by A2,RCOMP_1:13;
suppose
A3: a < b;
A4: [.a,b.] is closed by RCOMP_1:26;
].a,b.[ c= [.a,b.] by RCOMP_1:15;
hence Cl ].a,b.[ c= [.a,b.] by A4,PSCOMP_1:32;
A5: [.a,b.] = {w where w is Real : a <= w & w <= b } by RCOMP_1:def 1;
A6: ].a,b.[ = {w where w is Real : a < w & w < b } by RCOMP_1:def 2;
let p be set;
assume p in [.a,b.];
then consider r such that
A7: p = r and
A8: a <= r & r <= b by A5;
a1 < (a1+b1)/2 & (a1+b1)/2 < b1 by A3,TOPREAL3:3;
then A9: (a1+b1)/2 in ].a1,b1.[ by A6;
now per cases by A8,REAL_1:def 5;
case a < r & r < b;
then A10: r in ].a,b.[ by A6;
].a,b.[ c= Cl ].a,b.[ by PSCOMP_1:33;
hence p in Cl ].a,b.[ by A7,A10;
case
A11: a = r;
for O being open Subset of REAL st a in O holds O /\ ].a,b.[ is non empty
proof
let O be open Subset of REAL;
assume a in O;
then consider g being real number such that
A12: 0 < g and
A13: ].a-g,a+g.[ c= O by RCOMP_1:40;
reconsider g as Real by XREAL_0:def 1;
A14: ].a-g,a+g.[ = {w where w is Real : a-g < w & w < a+g } by RCOMP_1:def 2;
A15: a-g < a-0 by A12,REAL_1:92;
per cases;
suppose
A16: a+g < b;
A17: a+0 < a+g by A12,REAL_1:53;
then A18: a1 < (a1+(a1+g))/2 by TOPREAL3:3;
then A19: a-g < (a+(a+g))/2 by A15,AXIOMS:22;
A20: (a1+(a1+g))/2 < a1+g by A17,TOPREAL3:3;
then A21: (a1+(a1+g))/2 in ].a1-g,a1+g.[ by A14,A19;
(a+(a+g))/2 < b by A16,A20,AXIOMS:22;
then (a1+(a1+g))/2 in ].a1,b1.[ by A6,A18;
hence O /\ ].a,b.[ is non empty by A13,A21,XBOOLE_0:def 3;
suppose
A22: a+g >= b;
a1 < (a1+b1)/2 by A3,TOPREAL3:3;
then A23: a-g < (a+b)/2 by A15,AXIOMS:22;
(a1+b1)/2 < b1 by A3,TOPREAL3:3;
then (a+b)/2 < a+g by A22,AXIOMS:22;
then (a1+b1)/2 in ].a1-g,a1+g.[ by A14,A23;
hence O /\ ].a,b.[ is non empty by A9,A13,XBOOLE_0:def 3;
end;
hence p in Cl ].a,b.[ by A7,A11,PSCOMP_1:38;
case
A24: b = r;
for O being open Subset of REAL st b in O holds O /\ ].a,b.[ is non empty
proof
let O be open Subset of REAL;
assume b in O;
then consider g being real number such that
A25: 0 < g and
A26: ].b-g,b+g.[ c= O by RCOMP_1:40;
reconsider g as Real by XREAL_0:def 1;
A27: ].b-g,b+g.[ = {w where w is Real : b-g < w & w < b+g } by RCOMP_1:def 2;
A28: b-g < b-0 by A25,REAL_1:92;
A29: b+0 < b+g by A25,REAL_1:53;
per cases;
suppose
A30: b-g > a;
A31: b1-g < (b1+(b1-g))/2 by A28,TOPREAL3:3;
then A32: a < (b+(b-g))/2 by A30,AXIOMS:22;
(b1+(b1-g))/2 < b1 by A28,TOPREAL3:3;
then (b+(b-g))/2 < b+g by A29,AXIOMS:22;
then A33: (b1+(b1-g))/2 in ].b1-g,b1+g.[ by A27,A31;
(b1+(b1-g))/2 < b1 by A28,TOPREAL3:3;
then (b1+(b1-g))/2 in ].a1,b1.[ by A6,A32;
hence O /\ ].a,b.[ is non empty by A26,A33,XBOOLE_0:def 3;
suppose
A34: b-g <= a;
a1 < (a1+b1)/2 by A3,TOPREAL3:3;
then A35: b-g < (a+b)/2 by A34,AXIOMS:22;
(a1+b1)/2 < b1 by A3,TOPREAL3:3;
then (a+b)/2 < b+g by A29,AXIOMS:22;
then (a1+b1)/2 in ].b1-g,b1+g.[ by A27,A35;
hence O /\ ].a,b.[ is non empty by A9,A26,XBOOLE_0:def 3;
end;
hence p in Cl ].a,b.[ by A7,A24,PSCOMP_1:38;
end;
hence thesis;
end;
assume that
A36: Cl ].a,b.[ = [.a,b.] and
A37: a = b;
[.a,b.] = {a} by A37,RCOMP_1:14;
hence contradiction by A36,A37,PSCOMP_1:35,RCOMP_1:12;
end;
definition
cluster non empty finite bounded Subset of REAL;
existence
proof
reconsider a = {0} as finite Subset of REAL;
take a;
thus thesis by RCOMP_1:28;
end;
end;
theorem Th83:
for T being TopStruct, f being RealMap of T, g being map of T, R^1 st f = g
holds
f is continuous iff g is continuous
proof
let T be TopStruct,
f be RealMap of T,
g be map of T, R^1 such that
A1: f = g;
thus f is continuous implies g is continuous
proof
assume
A2: for Y being Subset of REAL st Y is closed holds f"Y is closed;
let P be Subset of R^1 such that
A3: P is closed;
reconsider R = P as Subset of REAL by TOPMETR:24;
R is closed by A3,Th79;
hence g"P is closed by A1,A2;
end;
assume
A4: for Y being Subset of R^1 st Y is closed holds g"Y is closed;
let P be Subset of REAL such that
A5: P is closed;
reconsider R = P as Subset of R^1 by TOPMETR:24;
R is closed by A5,Th79;
hence f"P is closed by A1,A4;
end;
theorem Th84:
for A, B being Subset of REAL,
f being map of [:R^1,R^1:], TOP-REAL 2 st
for x, y being Real holds f. [x,y] = <*x,y*> holds
f.:[:A,B:] = product ((1,2) --> (A,B))
proof
let A, B be Subset of REAL,
f be map of [:R^1,R^1:], TOP-REAL 2 such that
A1: for x, y being Real holds f. [x,y] = <*x,y*>;
set h = (1,2) --> (A,B);
A2: dom h = {1,2} by FUNCT_4:65;
A3: h.1 = A & h.2 = B by FUNCT_4:66;
thus f.:[:A,B:] c= product h
proof
let x be set;
assume x in f.:[:A,B:];
then consider a being set such that
A4: a in the carrier of [:R^1,R^1:] and
A5: a in [:A,B:] and
A6: f.a = x by FUNCT_2:115;
reconsider a as Point of [:R^1,R^1:] by A4;
consider m, n being set such that
A7: m in A & n in B and
A8: a = [m,n] by A5,ZFMISC_1:def 2;
reconsider m, n as Real by A7;
A9: |[m,n]| = <*m,n*> by EUCLID:def 16;
f.a = x by A6;
then reconsider g = x as Function of Seg 2, REAL by EUCLID:26;
A10: dom g = dom h by A2,FINSEQ_1:4,FUNCT_2:def 1;
for y being set st y in dom h holds g.y in h.y
proof
let y be set;
assume y in dom h;
then A11: y = 1 or y = 2 by A2,TARSKI:def 2;
A12: f. [m,n] = |[m,n]| by A1,A9;
|[m,n]|`1 = m & |[m,n]|`2 = n by EUCLID:56;
hence g.y in h.y by A3,A6,A7,A8,A9,A11,A12,EUCLID:def 14,def 15;
end;
hence thesis by A10,CARD_3:18;
end;
let a be set;
assume a in product h;
then consider g being Function such that
A13: a = g and
A14: dom g = dom h and
A15: for x being set st x in dom h holds g.x in h.x by CARD_3:def 5;
1 in dom h & 2 in dom h by A2,TARSKI:def 2;
then A16: g.1 in A & g.2 in B by A3,A15;
then A17: [g.1,g.2] in [:A,B:] by ZFMISC_1:106;
A18: dom <*g.1,g.2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
now
let k be set;
assume k in dom g;
then k = 1 or k = 2 by A2,A14,TARSKI:def 2;
hence g.k = <*g.1,g.2*>.k by FINSEQ_1:61;
end;
then A19: a = <*g.1,g.2*> by A2,A13,A14,A18,FUNCT_1:9;
the carrier of [:R^1,R^1:] = [:the carrier of R^1,the carrier of R^1:]
by BORSUK_1:def 5;
then A20: [g.1,g.2] in the carrier of [:R^1,R^1:] by A16,TOPMETR:24,ZFMISC_1:
106;
f. [g.1,g.2] = <*g.1,g.2*> by A1,A16;
hence a in f.:[:A,B:] by A17,A19,A20,FUNCT_2:43;
end;
theorem Th85:
for f being map of [:R^1,R^1:], TOP-REAL 2 st
for x, y being Real holds f. [x,y] = <*x,y*> holds
f is_homeomorphism
proof
let f be map of [:R^1,R^1:], TOP-REAL 2 such that
A1: for x, y being Real holds f. [x,y] = <*x,y*>;
A2: the carrier of [:R^1,R^1:] = [:the carrier of R^1,the carrier of R^1:]
by BORSUK_1:def 5;
then A3: dom f = [:the carrier of R^1,the carrier of R^1:] by FUNCT_2:def 1;
hence dom f = [:[#]R^1,the carrier of R^1:] by PRE_TOPC:12
.= [:[#]R^1,[#]R^1:] by PRE_TOPC:12
.= [#][:R^1,R^1:] by BORSUK_3:1;
thus
A4: rng f = [#]TOP-REAL 2
proof
rng f c= the carrier of TOP-REAL 2;
hence rng f c= [#]TOP-REAL 2 by PRE_TOPC:12;
let y be set;
assume y in [#]TOP-REAL 2;
then consider a, b such that
A5: y = <*a,b*> by EUCLID:55;
A6: [a,b] in dom f by A3,TOPMETR:24,ZFMISC_1:106;
f. [a,b] = <*a,b*> by A1;
hence y in rng f by A5,A6,FUNCT_1:def 5;
end;
thus
A7: f is one-to-one
proof
let x, y be set;
assume x in dom f;
then consider x1, x2 being set such that
A8: x1 in REAL & x2 in REAL and
A9: x = [x1,x2] by A3,TOPMETR:24,ZFMISC_1:def 2;
assume y in dom f;
then consider y1, y2 being set such that
A10: y1 in REAL & y2 in REAL and
A11: y = [y1,y2] by A3,TOPMETR:24,ZFMISC_1:def 2;
reconsider x1, x2, y1, y2 as Real by A8,A10;
A12: f. [x1,x2] = <*x1,x2*> & f. [y1,y2] = <*y1,y2*> by A1;
assume f.x = f.y;
then x1 = y1 & x2 = y2 by A9,A11,A12,GROUP_7:2;
hence x = y by A9,A11;
end;
thus f is continuous
proof
let w be Point of [:R^1,R^1:],
G be a_neighborhood of f.w;
consider x, y being set such that
A13: x in the carrier of R^1 & y in the carrier of R^1 and
A14: w = [x,y] by A2,ZFMISC_1:def 2;
reconsider x, y as Real by A13,TOPMETR:24;
reconsider fw = f.w as Point of Euclid 2 by TOPREAL3:13;
fw in Int G by CONNSP_2:def 1;
then consider r being real number such that
A15: r > 0 and
A16: Ball(fw,r) c= G by GOBOARD6:8;
reconsider r as Real by XREAL_0:def 1;
set A = ].(f.w)`1-r/sqrt 2,(f.w)`1+r/sqrt 2.[,
B = ].(f.w)`2-r/sqrt 2,(f.w)`2+r/sqrt 2.[;
reconsider A, B as Subset of R^1 by TOPMETR:24;
take [:A,B:];
thus [:A,B:] is a_neighborhood of w
proof
A17: Base-Appr [:A,B:] = { [:X1,Y1:] where X1, Y1 is Subset of R^1 :
[:X1,Y1:] c= [:A,B:] & X1 is open & Y1 is open} by BORSUK_1:def 6;
A is open & B is open by JORDAN6:46;
then A18: [:A,B:] in Base-Appr [:A,B:] by A17;
A19: r/sqrt 2 > 0 by A15,Lm1,REAL_2:127;
f. [x,y] = <*x,y*> by A1;
then f. [x,y] = |[x,y]| by EUCLID:def 16;
then x = (f.w)`1 & y = (f.w)`2 by A14,EUCLID:56;
then x in A & y in B by A19,Th20;
then w in [:A,B:] by A14,ZFMISC_1:106;
then w in union Base-Appr [:A,B:] by A18,TARSKI:def 4;
hence w in Int [:A,B:] by BORSUK_1:55;
end;
product ((1,2)-->(A,B)) c= Ball(fw,r) by Th49;
then f.:[:A,B:] c= Ball(fw,r) by A1,Th84;
hence f.:[:A,B:] c= G by A16,XBOOLE_1:1;
end;
A20: dom (f") = [#]TOP-REAL 2 by A4,A7,TOPS_2:62
.= the carrier of TOP-REAL 2 by PRE_TOPC:12;
reconsider f1 = proj1, f2 = proj2 as map of TOP-REAL 2, R^1 by TOPMETR:24;
A21: dom <:f1,f2:> = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
now
let x be set;
assume
A22: x in dom (f");
then consider a, b such that
A23: x = <*a,b*> by A20,EUCLID:55;
A24: dom f1 = the carrier of TOP-REAL 2 &
dom f2 = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
A25: [a,b] in dom f by A3,TOPMETR:24,ZFMISC_1:106;
A26: f. [a,b] = <*a,b*> by A1;
reconsider p = x as Point of TOP-REAL 2 by A20,A22;
A27: p = |[a,b]| by A23,EUCLID:def 16;
thus f".x = (f qua Function)".x by A4,A7,TOPS_2:def 4
.= [a,b] by A7,A23,A25,A26,FUNCT_1:54
.= [p`1,b] by A27,EUCLID:56
.= [p`1,p`2] by A27,EUCLID:56
.= [f1.x,p`2] by PSCOMP_1:def 28
.= [f1.x,f2.x] by PSCOMP_1:def 29
.= <:f1,f2:>.x by A20,A22,A24,FUNCT_3:69;
end;
then A28: f" = <:f1,f2:> by A20,A21,FUNCT_1:9;
f1 is continuous & f2 is continuous by Th83;
hence f" is continuous by A28,YELLOW12:41;
end;
theorem
[:R^1,R^1:], TOP-REAL 2 are_homeomorphic
proof
defpred P[Element of REAL,Element of REAL,set] means
ex c being Element of REAL 2 st c = $3 & $3 = <*$1,$2*>;
A1: for x, y being Element of REAL
ex u being Element of REAL 2 st P[x,y,u]
proof
let x, y be Element of REAL;
take <*x,y*>;
<*x,y*> in 2-tuples_on REAL by CATALG_1:10;
hence <*x,y*> is Element of REAL 2 by EUCLID:def 1;
hence P[x,y,<*x,y*>];
end;
consider f being Function of [:REAL,REAL:],REAL 2 such that
A2: for x, y being Element of REAL holds P[x,y,f. [x,y]]
from FuncEx2D(A1);
the carrier of [:R^1,R^1:] = [:the carrier of R^1,the carrier of R^1:] &
the carrier of R^1 = REAL &
the carrier of TOP-REAL 2 = REAL 2
by BORSUK_1:def 5,EUCLID:25,TOPMETR:24;
then reconsider f as map of [:R^1,R^1:], TOP-REAL 2;
take f;
for x, y being Real holds f. [x,y] = <*x,y*>
proof
let x, y be Real;
P[x,y,f. [x,y]] by A2;
hence thesis;
end;
hence thesis by Th85;
end;
begin :: Bounded subsets
theorem Th87:
for A, B being compact Subset of REAL holds
product ((1,2) --> (A,B)) is compact Subset of TOP-REAL 2
proof
let A, B be compact Subset of REAL;
reconsider A1 = A, B1 = B as Subset of R^1 by TOPMETR:24;
A1 is compact & B1 is compact by Th81;
then A1: [:A1,B1:] is compact by BORSUK_3:27;
reconsider X = product ((1,2) --> (A,B)) as Subset of TOP-REAL 2 by Th30;
defpred P[Element of REAL,Element of REAL,set] means
ex c being Element of REAL 2 st c = $3 & $3 = <*$1,$2*>;
A2: for x, y being Element of REAL
ex u being Element of REAL 2 st P[x,y,u]
proof
let x, y be Element of REAL;
take <*x,y*>;
<*x,y*> in 2-tuples_on REAL by CATALG_1:10;
hence <*x,y*> is Element of REAL 2 by EUCLID:def 1;
hence P[x,y,<*x,y*>];
end;
consider h being Function of [:REAL,REAL:],REAL 2 such that
A3: for x, y being Element of REAL holds P[x,y,h. [x,y]]
from FuncEx2D(A2);
the carrier of [:R^1,R^1:] = [:the carrier of R^1,the carrier of R^1:] &
the carrier of R^1 = REAL &
the carrier of TOP-REAL 2 = REAL 2
by BORSUK_1:def 5,EUCLID:25,TOPMETR:24;
then reconsider h as map of [:R^1,R^1:], TOP-REAL 2;
A4: for x, y being Real holds h. [x,y] = <*x,y*>
proof
let x, y be Real;
P[x,y,h. [x,y]] by A3;
hence thesis;
end;
then A5: h.:[:A1,B1:] = X by Th84;
h is_homeomorphism by A4,Th85;
then h is continuous by TOPS_2:def 5;
hence thesis by A1,A5,WEIERSTR:14;
end;
theorem Th88:
P is Bounded closed implies P is compact
proof
assume
A1: P is Bounded closed;
then consider C being Subset of Euclid 2 such that
A2: C = P and
A3: C is bounded by JORDAN2C:def 2;
consider r, e such that
0 < r and
A4: C c= Ball(e,r) by A3,METRIC_6:def 10;
reconsider p = e as Point of TOP-REAL 2 by TOPREAL3:13;
A5: Ball(e,r) c= product ((1,2)-->(].p`1-r,p`1+r.[,].p`2-r,p`2+r.[)) by Th50;
].p`1-r,p`1+r.[ c= [.p`1-r,p`1+r.] & ].p`2-r,p`2+r.[ c= [.p`2-r,p`2+r.]
by RCOMP_1:15;
then product ((1,2)-->(].p`1-r,p`1+r.[,].p`2-r,p`2+r.[)) c=
product ((1,2)-->([.p`1-r,p`1+r.],[.p`2-r,p`2+r.])) by Th29;
then Ball(e,r) c= product ((1,2)-->([.p`1-r,p`1+r.],[.p`2-r,p`2+r.]))
by A5,XBOOLE_1:1;
then A6: P c= product ((1,2)-->([.p`1-r,p`1+r.],[.p`2-r,p`2+r.]))
by A2,A4,XBOOLE_1:1;
product ((1,2)-->([.p`1-r,p`1+r.],[.p`2-r,p`2+r.])) is compact
Subset of TOP-REAL 2 by Th87;
hence P is compact by A1,A6,COMPTS_1:18;
end;
theorem Th89:
P is Bounded implies
for g being continuous RealMap of TOP-REAL 2 holds Cl(g.:P) c= g.:Cl P
proof
assume
A1: P is Bounded;
let g be continuous RealMap of TOP-REAL 2;
reconsider f = g as map of TOP-REAL 2, R^1 by TOPMETR:24;
A2: f is continuous by Th83;
Cl P is Bounded by A1,Th71;
then Cl P is compact by Th88;
then f.:Cl P is compact by A2,WEIERSTR:15;
then f.:Cl P is closed by COMPTS_1:16;
then A3: g.:Cl P is closed by Th79;
P c= Cl P by PRE_TOPC:48;
then g.:P c= g.:Cl P by RELAT_1:156;
hence Cl(g.:P) c= g.:Cl P by A3,PSCOMP_1:32;
end;
theorem Th90:
proj1.:Cl P c= Cl(proj1.:P)
proof
let y be set;
assume y in proj1.:Cl P;
then consider x being set such that
A1: x in the carrier of TOP-REAL 2 and
A2: x in Cl P and
A3: y = proj1.x by FUNCT_2:115;
reconsider x as Point of TOP-REAL 2 by A1;
set r = proj1.x;
for O being open Subset of REAL st y in O holds O /\ proj1.:P is non
empty
proof
let O be open Subset of REAL;
assume y in O;
then consider g being real number such that
A4: 0 < g and
A5: ].r-g,r+g.[ c= O by A3,RCOMP_1:40;
reconsider g as Real by XREAL_0:def 1;
reconsider e = x as Point of Euclid 2 by TOPREAL3:13;
the carrier of TOP-REAL 2 = the carrier of Euclid 2 by TOPREAL3:13;
then reconsider B = Ball(e,g/2) as Subset of TOP-REAL 2;
A6: B is open by GOBOARD6:6;
g/2 > 0 by A4,REAL_2:127;
then e in B by TBSP_1:16;
then P meets B by A2,A6,TOPS_1:39;
then P /\ B <> {} by XBOOLE_0:def 7;
then consider d being Point of TOP-REAL 2 such that
A7: d in P /\ B by SUBSET_1:10;
d in P by A7,XBOOLE_0:def 3;
then proj1.d in proj1.:P by FUNCT_2:43;
then A8: d`1 in proj1.:P by PSCOMP_1:def 28;
A9: ].r-g,r+g.[ = {t where t is Real: r-g < t & t < r+g} by RCOMP_1:def 2;
d in B by A7,XBOOLE_0:def 3;
then x`1-g/2 < d`1 & d`1 < x`1+g/2 by Th47;
then A10: r-g/2 < d`1 & d`1 < r+g/2 by PSCOMP_1:def 28;
g/2 < g/1 by A4,REAL_2:200;
then r-g < r-g/2 & r+g/2 < r+g by REAL_1:53,92;
then r-g < d`1 & d`1 < r+g by A10,AXIOMS:22;
then d`1 in ].r-g,r+g.[ by A9;
hence thesis by A5,A8,XBOOLE_0:def 3;
end;
hence y in Cl(proj1.:P) by A3,PSCOMP_1:38;
end;
theorem Th91:
proj2.:Cl P c= Cl(proj2.:P)
proof
let y be set;
assume y in proj2.:Cl P;
then consider x being set such that
A1: x in the carrier of TOP-REAL 2 and
A2: x in Cl P and
A3: y = proj2.x by FUNCT_2:115;
reconsider x as Point of TOP-REAL 2 by A1;
set r = proj2.x;
for O being open Subset of REAL st y in O holds O /\ proj2.:P is non
empty
proof
let O be open Subset of REAL;
assume y in O;
then consider g being real number such that
A4: 0 < g and
A5: ].r-g,r+g.[ c= O by A3,RCOMP_1:40;
reconsider g as Real by XREAL_0:def 1;
reconsider e = x as Point of Euclid 2 by TOPREAL3:13;
the carrier of TOP-REAL 2 = the carrier of Euclid 2 by TOPREAL3:13;
then reconsider B = Ball(e,g/2) as Subset of TOP-REAL 2;
A6: B is open by GOBOARD6:6;
g/2 > 0 by A4,REAL_2:127;
then e in B by TBSP_1:16;
then P meets B by A2,A6,TOPS_1:39;
then P /\ B <> {} by XBOOLE_0:def 7;
then consider d being Point of TOP-REAL 2 such that
A7: d in P /\ B by SUBSET_1:10;
d in P by A7,XBOOLE_0:def 3;
then proj2.d in proj2.:P by FUNCT_2:43;
then A8: d`2 in proj2.:P by PSCOMP_1:def 29;
A9: ].r-g,r+g.[ = {t where t is Real: r-g < t & t < r+g} by RCOMP_1:def 2;
d in B by A7,XBOOLE_0:def 3;
then x`2-g/2 < d`2 & d`2 < x`2+g/2 by Th48;
then A10: r-g/2 < d`2 & d`2 < r+g/2 by PSCOMP_1:def 29;
g/2 < g/1 by A4,REAL_2:200;
then r-g < r-g/2 & r+g/2 < r+g by REAL_1:53,92;
then r-g < d`2 & d`2 < r+g by A10,AXIOMS:22;
then d`2 in ].r-g,r+g.[ by A9;
hence thesis by A5,A8,XBOOLE_0:def 3;
end;
hence y in Cl(proj2.:P) by A3,PSCOMP_1:38;
end;
theorem Th92:
P is Bounded implies Cl(proj1.:P) = proj1.:Cl P
proof
assume P is Bounded;
hence Cl(proj1.:P) c= proj1.:Cl P by Th89;
thus thesis by Th90;
end;
theorem Th93:
P is Bounded implies Cl(proj2.:P) = proj2.:Cl P
proof
assume P is Bounded;
hence Cl(proj2.:P) c= proj2.:Cl P by Th89;
thus thesis by Th91;
end;
theorem
D is Bounded implies W-bound D = W-bound Cl D
proof
assume
A1: D is Bounded;
then Cl D is Bounded by Th71;
then A2: Cl D is compact by Th88;
A3: W-bound D = inf (proj1.:D) & W-bound Cl D = inf (proj1.:
Cl D) by SPRECT_1:48;
A4: proj1.:Cl D is bounded_below by A2,SPRECT_1:46;
D c= Cl D by PRE_TOPC:48;
then proj1.:D c= proj1.:Cl D by RELAT_1:156;
then proj1.:D is bounded_below by A4,RCOMP_1:3;
then inf (proj1.:D) = inf Cl(proj1.:D) by Th77
.= inf (proj1.:Cl D) by A1,Th92;
hence thesis by A3;
end;
theorem
D is Bounded implies E-bound D = E-bound Cl D
proof
assume
A1: D is Bounded;
then Cl D is Bounded by Th71;
then A2: Cl D is compact by Th88;
A3: E-bound D = sup (proj1.:D) & E-bound Cl D = sup (proj1.:
Cl D) by SPRECT_1:51;
A4: proj1.:Cl D is bounded_above by A2,SPRECT_1:47;
D c= Cl D by PRE_TOPC:48;
then proj1.:D c= proj1.:Cl D by RELAT_1:156;
then proj1.:D is bounded_above by A4,RCOMP_1:4;
then sup (proj1.:D) = sup Cl(proj1.:D) by Th78
.= sup (proj1.:Cl D) by A1,Th92;
hence thesis by A3;
end;
theorem
D is Bounded implies N-bound D = N-bound Cl D
proof
assume
A1: D is Bounded;
then Cl D is Bounded by Th71;
then A2: Cl D is compact by Th88;
A3: N-bound D = sup (proj2.:D) & N-bound Cl D = sup (proj2.:
Cl D) by SPRECT_1:50;
A4: proj2.:Cl D is bounded_above by A2,SPRECT_1:47;
D c= Cl D by PRE_TOPC:48;
then proj2.:D c= proj2.:Cl D by RELAT_1:156;
then proj2.:D is bounded_above by A4,RCOMP_1:4;
then sup (proj2.:D) = sup Cl(proj2.:D) by Th78
.= sup (proj2.:Cl D) by A1,Th93;
hence thesis by A3;
end;
theorem
D is Bounded implies S-bound D = S-bound Cl D
proof
assume
A1: D is Bounded;
then Cl D is Bounded by Th71;
then A2: Cl D is compact by Th88;
A3: S-bound D = inf (proj2.:D) & S-bound Cl D = inf (proj2.:
Cl D) by SPRECT_1:49;
A4: proj2.:Cl D is bounded_below by A2,SPRECT_1:46;
D c= Cl D by PRE_TOPC:48;
then proj2.:D c= proj2.:Cl D by RELAT_1:156;
then proj2.:D is bounded_below by A4,RCOMP_1:3;
then inf (proj2.:D) = inf Cl(proj2.:D) by Th77
.= inf (proj2.:Cl D) by A1,Th93;
hence thesis by A3;
end;