### The Mizar article:

### Compactness of the Bounded Closed Subsets of $\cal E^2_\rm T$

**by****Artur Kornilowicz**

- Received February 19, 1999
Copyright (c) 1999 Association of Mizar Users

- MML identifier: TOPREAL6
- [ MML identifier index ]

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;

Back to top