:: TOPREAL6 semantic presentation begin theorem Th1: :: TOPREAL6:1 for a, b being real number st 0 <= a & 0 <= b holds sqrt (a + b) <= (sqrt a) + (sqrt b) by SQUARE_1:59; theorem Th2: :: TOPREAL6:2 for a, b being real number st 0 <= a & a <= b holds abs a <= abs b proof let a, b be real number ; ::_thesis: ( 0 <= a & a <= b implies abs a <= abs b ) assume that A1: 0 <= a and A2: a <= b ; ::_thesis: abs a <= abs b abs a = a by A1, ABSVALUE:def_1; hence abs a <= abs b by A1, A2, ABSVALUE:def_1; ::_thesis: verum end; theorem Th3: :: TOPREAL6:3 for b, a being real number st b <= a & a <= 0 holds abs a <= abs b proof let b, a be real number ; ::_thesis: ( b <= a & a <= 0 implies abs a <= abs b ) assume that A1: b <= a and A2: a <= 0 ; ::_thesis: abs a <= abs b percases ( a = 0 or a < 0 ) by A2; suppose a = 0 ; ::_thesis: abs a <= abs b then abs a = 0 by ABSVALUE:2; hence abs a <= abs b by COMPLEX1:46; ::_thesis: verum end; supposeA3: a < 0 ; ::_thesis: abs a <= abs b then A4: abs a = - a by ABSVALUE:def_1; abs b = - b by A1, A3, ABSVALUE:def_1; hence abs a <= abs b by A1, A4, XREAL_1:24; ::_thesis: verum end; end; end; theorem :: TOPREAL6:4 for r being Real holds Product (0 |-> r) = 1 by RVSUM_1:94; theorem Th5: :: TOPREAL6:5 for r being Real holds Product (1 |-> r) = r proof let r be Real; ::_thesis: Product (1 |-> r) = r thus Product (1 |-> r) = Product <*r*> by FINSEQ_2:59 .= r by RVSUM_1:95 ; ::_thesis: verum end; theorem :: TOPREAL6:6 for r being Real holds Product (2 |-> r) = r * r proof let r be Real; ::_thesis: Product (2 |-> r) = r * r thus Product (2 |-> r) = Product <*r,r*> by FINSEQ_2:61 .= r * r by RVSUM_1:99 ; ::_thesis: verum end; theorem Th7: :: TOPREAL6:7 for r being Real for n being Element of NAT holds Product ((n + 1) |-> r) = (Product (n |-> r)) * r proof let r be Real; ::_thesis: for n being Element of NAT holds Product ((n + 1) |-> r) = (Product (n |-> r)) * r let n be Element of NAT ; ::_thesis: Product ((n + 1) |-> r) = (Product (n |-> r)) * r thus Product ((n + 1) |-> r) = (Product (n |-> r)) * (Product (1 |-> r)) by RVSUM_1:104 .= (Product (n |-> r)) * r by Th5 ; ::_thesis: verum end; theorem Th8: :: TOPREAL6:8 for r being Real for j being Element of NAT holds ( ( j <> 0 & r = 0 ) iff Product (j |-> r) = 0 ) proof let r be Real; ::_thesis: for j being Element of NAT holds ( ( j <> 0 & r = 0 ) iff Product (j |-> r) = 0 ) let j be Element of NAT ; ::_thesis: ( ( j <> 0 & r = 0 ) iff Product (j |-> r) = 0 ) set f = j |-> r; A1: dom (j |-> r) = Seg j by FUNCOP_1:13; hereby ::_thesis: ( Product (j |-> r) = 0 implies ( j <> 0 & r = 0 ) ) assume that A2: j <> 0 and A3: r = 0 ; ::_thesis: Product (j |-> r) = 0 ex n being Nat st j = n + 1 by A2, NAT_1:6; then 1 <= j by NAT_1:11; then A4: 1 in Seg j by FINSEQ_1:1; then (j |-> r) . 1 = 0 by A3, FUNCOP_1:7; hence Product (j |-> r) = 0 by A1, A4, RVSUM_1:103; ::_thesis: verum end; assume Product (j |-> r) = 0 ; ::_thesis: ( j <> 0 & r = 0 ) then ex n being Nat st ( n in dom (j |-> r) & (j |-> r) . n = 0 ) by RVSUM_1:103; hence ( j <> 0 & r = 0 ) by A1, FUNCOP_1:7; ::_thesis: verum end; theorem Th9: :: TOPREAL6:9 for r being Real for j, i being Element of NAT st r <> 0 & j <= i holds Product ((i -' j) |-> r) = (Product (i |-> r)) / (Product (j |-> r)) proof let r be Real; ::_thesis: for j, i being Element of NAT st r <> 0 & j <= i holds Product ((i -' j) |-> r) = (Product (i |-> r)) / (Product (j |-> r)) let j, i be Element of NAT ; ::_thesis: ( r <> 0 & j <= i implies Product ((i -' j) |-> r) = (Product (i |-> r)) / (Product (j |-> r)) ) assume that A1: r <> 0 and A2: j <= i ; ::_thesis: Product ((i -' j) |-> r) = (Product (i |-> r)) / (Product (j |-> r)) defpred S1[ Element of NAT ] means ( j <= \$1 implies Product ((\$1 -' j) |-> r) = (Product (\$1 |-> r)) / (Product (j |-> r)) ); A3: Product (j |-> r) <> 0 by A1, Th8; A4: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume that A5: S1[n] and A6: j <= n + 1 ; ::_thesis: Product (((n + 1) -' j) |-> r) = (Product ((n + 1) |-> r)) / (Product (j |-> r)) percases ( j <= n or j = n + 1 ) by A6, NAT_1:8; supposeA7: j <= n ; ::_thesis: Product (((n + 1) -' j) |-> r) = (Product ((n + 1) |-> r)) / (Product (j |-> r)) Product (((n -' j) + 1) |-> r) = (Product ((n -' j) |-> r)) * (Product (1 |-> r)) by RVSUM_1:104 .= ((Product (n |-> r)) / (Product (j |-> r))) * r by A5, A7, Th5 .= ((Product (n |-> r)) * r) / (Product (j |-> r)) by XCMPLX_1:74 .= (Product ((n + 1) |-> r)) / (Product (j |-> r)) by Th7 ; hence Product (((n + 1) -' j) |-> r) = (Product ((n + 1) |-> r)) / (Product (j |-> r)) by A7, NAT_D:38; ::_thesis: verum end; supposeA8: j = n + 1 ; ::_thesis: Product (((n + 1) -' j) |-> r) = (Product ((n + 1) |-> r)) / (Product (j |-> r)) hence Product (((n + 1) -' j) |-> r) = Product (0 |-> r) by XREAL_1:232 .= 1 by RVSUM_1:94 .= (Product ((n + 1) |-> r)) / (Product (j |-> r)) by A3, A8, XCMPLX_1:60 ; ::_thesis: verum end; end; end; A9: S1[ 0 ] proof assume A10: j <= 0 ; ::_thesis: Product ((0 -' j) |-> r) = (Product (0 |-> r)) / (Product (j |-> r)) then j = 0 by NAT_1:3; hence Product ((0 -' j) |-> r) = (Product (0 |-> r)) / (Product (<*> REAL)) by NAT_D:40, RVSUM_1:94 .= (Product (0 |-> r)) / (Product (j |-> r)) by A10, NAT_1:3 ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A4); hence Product ((i -' j) |-> r) = (Product (i |-> r)) / (Product (j |-> r)) by A2; ::_thesis: verum end; theorem :: TOPREAL6:10 for r being Real for j, i being Element of NAT st r <> 0 & j <= i holds r |^ (i -' j) = (r |^ i) / (r |^ j) proof let r be Real; ::_thesis: for j, i being Element of NAT st r <> 0 & j <= i holds r |^ (i -' j) = (r |^ i) / (r |^ j) let j, i be Element of NAT ; ::_thesis: ( r <> 0 & j <= i implies r |^ (i -' j) = (r |^ i) / (r |^ j) ) assume that A1: r <> 0 and A2: j <= i ; ::_thesis: r |^ (i -' j) = (r |^ i) / (r |^ j) 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, A2, Th9 .= r |^ (i -' j) by NEWTON:def_1 ; ::_thesis: verum end; theorem Th11: :: TOPREAL6:11 for a, b being Real holds sqr <*a,b*> = <*(a ^2),(b ^2)*> proof let a, b be Real; ::_thesis: sqr <*a,b*> = <*(a ^2),(b ^2)*> dom sqrreal = REAL by FUNCT_2:def_1; then A1: rng <*a,b*> c= dom sqrreal ; A2: dom <*(a ^2),(b ^2)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; A3: 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 ; ::_thesis: ( i in dom <*(a ^2),(b ^2)*> implies (sqr <*a,b*>) . i = <*(a ^2),(b ^2)*> . i ) A4: <*a,b*> . 1 = a by FINSEQ_1:44; A5: <*a,b*> . 2 = b by FINSEQ_1:44; assume A6: i in dom <*(a ^2),(b ^2)*> ; ::_thesis: (sqr <*a,b*>) . i = <*(a ^2),(b ^2)*> . i percases ( i = 1 or i = 2 ) by A2, A6, TARSKI:def_2; supposeA7: i = 1 ; ::_thesis: (sqr <*a,b*>) . i = <*(a ^2),(b ^2)*> . i hence (sqr <*a,b*>) . i = a ^2 by A4, VALUED_1:11 .= <*(a ^2),(b ^2)*> . i by A7, FINSEQ_1:44 ; ::_thesis: verum end; supposeA8: i = 2 ; ::_thesis: (sqr <*a,b*>) . i = <*(a ^2),(b ^2)*> . i hence (sqr <*a,b*>) . i = b ^2 by A5, VALUED_1:11 .= <*(a ^2),(b ^2)*> . i by A8, FINSEQ_1:44 ; ::_thesis: verum end; end; end; dom (sqr <*a,b*>) = dom (sqrreal * <*a,b*>) by RVSUM_1:def_8 .= dom <*a,b*> by A1, RELAT_1:27 .= {1,2} by FINSEQ_1:2, FINSEQ_1:89 ; hence sqr <*a,b*> = <*(a ^2),(b ^2)*> by A3, FINSEQ_1:2, FINSEQ_1:89, FUNCT_1:2; ::_thesis: verum end; theorem Th12: :: TOPREAL6:12 for a being Real for i being Nat for F being FinSequence of REAL st i in dom (abs F) & a = F . i holds (abs F) . i = abs a proof let a be Real; ::_thesis: for i being Nat for F being FinSequence of REAL st i in dom (abs F) & a = F . i holds (abs F) . i = abs a let i be Nat; ::_thesis: for F being FinSequence of REAL st i in dom (abs F) & a = F . i holds (abs F) . i = abs a let F be FinSequence of REAL ; ::_thesis: ( i in dom (abs F) & a = F . i implies (abs F) . i = abs a ) assume that A1: i in dom (abs F) and A2: a = F . i ; ::_thesis: (abs F) . i = abs a (abs F) . i = absreal . a by A1, A2, FUNCT_1:12; hence (abs F) . i = abs a by EUCLID:def_2; ::_thesis: verum end; theorem :: TOPREAL6:13 for a, b being Real holds abs <*a,b*> = <*(abs a),(abs b)*> proof let a, b be Real; ::_thesis: abs <*a,b*> = <*(abs a),(abs b)*> dom absreal = REAL by FUNCT_2:def_1; then rng <*a,b*> c= dom absreal ; then A1: dom (abs <*a,b*>) = dom <*a,b*> by RELAT_1:27 .= {1,2} by FINSEQ_1:2, FINSEQ_1:89 ; A2: dom <*(abs a),(abs b)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; 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 ; ::_thesis: ( i in dom <*(abs a),(abs b)*> implies (abs <*a,b*>) . i = <*(abs a),(abs b)*> . i ) A3: <*a,b*> . 1 = a by FINSEQ_1:44; A4: <*a,b*> . 2 = b by FINSEQ_1:44; A5: 2 in {1,2} by TARSKI:def_2; A6: 1 in {1,2} by TARSKI:def_2; assume A7: i in dom <*(abs a),(abs b)*> ; ::_thesis: (abs <*a,b*>) . i = <*(abs a),(abs b)*> . i percases ( i = 1 or i = 2 ) by A2, A7, TARSKI:def_2; supposeA8: i = 1 ; ::_thesis: (abs <*a,b*>) . i = <*(abs a),(abs b)*> . i hence (abs <*a,b*>) . i = abs a by A1, A3, A6, Th12 .= <*(abs a),(abs b)*> . i by A8, FINSEQ_1:44 ; ::_thesis: verum end; supposeA9: i = 2 ; ::_thesis: (abs <*a,b*>) . i = <*(abs a),(abs b)*> . i hence (abs <*a,b*>) . i = abs b by A1, A4, A5, Th12 .= <*(abs a),(abs b)*> . i by A9, FINSEQ_1:44 ; ::_thesis: verum end; end; end; hence abs <*a,b*> = <*(abs a),(abs b)*> by A1, FINSEQ_1:2, FINSEQ_1:89, FUNCT_1:2; ::_thesis: verum end; theorem :: TOPREAL6:14 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 ; ::_thesis: ( a <= b & c <= d implies (abs (b - a)) + (abs (d - c)) = (b - a) + (d - c) ) assume that A1: a <= b and A2: c <= d ; ::_thesis: (abs (b - a)) + (abs (d - c)) = (b - a) + (d - c) a - a <= b - a by A1, XREAL_1:13; then A3: abs (b - a) = b - a by ABSVALUE:def_1; c - c <= d - c by A2, XREAL_1:13; hence (abs (b - a)) + (abs (d - c)) = (b - a) + (d - c) by A3, ABSVALUE:def_1; ::_thesis: verum end; theorem Th15: :: TOPREAL6:15 for a, r being real number st r > 0 holds a in ].(a - r),(a + r).[ proof let a, r be real number ; ::_thesis: ( r > 0 implies a in ].(a - r),(a + r).[ ) assume r > 0 ; ::_thesis: a in ].(a - r),(a + r).[ then abs (a - a) < r by ABSVALUE:def_1; hence a in ].(a - r),(a + r).[ by RCOMP_1:1; ::_thesis: verum end; theorem :: TOPREAL6:16 for a, r being real number st r >= 0 holds a in [.(a - r),(a + r).] proof let a, r be real number ; ::_thesis: ( r >= 0 implies a in [.(a - r),(a + r).] ) assume A1: r >= 0 ; ::_thesis: a in [.(a - r),(a + r).] reconsider a = a, r = r as Real by XREAL_0:def_1; A2: a + 0 <= a + r by A1, XREAL_1:7; A3: [.(a - r),(a + r).] = { b where b is Real : ( a - r <= b & b <= a + r ) } by RCOMP_1:def_1; a - r <= a - 0 by A1, XREAL_1:13; hence a in [.(a - r),(a + r).] by A3, A2; ::_thesis: verum end; theorem Th17: :: TOPREAL6:17 for a, b being real number st a < b holds ( lower_bound ].a,b.[ = a & upper_bound ].a,b.[ = b ) proof let a, b be real number ; ::_thesis: ( a < b implies ( lower_bound ].a,b.[ = a & upper_bound ].a,b.[ = b ) ) assume A1: a < b ; ::_thesis: ( lower_bound ].a,b.[ = a & upper_bound ].a,b.[ = b ) set X = ].a,b.[; reconsider a = a, b = b as Real by XREAL_0:def_1; A2: (a + b) / 2 < b by A1, XREAL_1:226; A3: a < (a + b) / 2 by A1, XREAL_1:226; then A4: (a + b) / 2 in { l where l is Real : ( a < l & l < b ) } by A2; A5: for s being real number st 0 < s holds ex r being real number st ( r in ].a,b.[ & r < a + s ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in ].a,b.[ & r < a + s ) ) assume that A6: 0 < s and A7: for r being real number st r in ].a,b.[ holds r >= a + s ; ::_thesis: contradiction reconsider s = s as Real by XREAL_0:def_1; percases ( a + s >= b or a + s < b ) ; supposeA8: a + s >= b ; ::_thesis: contradiction A9: (a + b) / 2 in ].a,b.[ by A4, RCOMP_1:def_2; (a + b) / 2 < a + s by A2, A8, XXREAL_0:2; hence contradiction by A7, A9; ::_thesis: verum end; supposeA10: a + s < b ; ::_thesis: contradiction A11: a < a + s by A6, XREAL_1:29; then (a + (a + s)) / 2 < a + s by XREAL_1:226; then A12: (a + (a + s)) / 2 < b by A10, XXREAL_0:2; a < (a + (a + s)) / 2 by A11, XREAL_1:226; then (a + (a + s)) / 2 in { r where r is Real : ( a < r & r < b ) } by A12; then (a + (a + s)) / 2 in ].a,b.[ by RCOMP_1:def_2; hence contradiction by A7, A11, XREAL_1:226; ::_thesis: verum end; end; end; A13: for s being real number st 0 < s holds ex r being real number st ( r in ].a,b.[ & b - s < r ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in ].a,b.[ & b - s < r ) ) assume that A14: 0 < s and A15: for r being real number st r in ].a,b.[ holds r <= b - s ; ::_thesis: contradiction reconsider s = s as Real by XREAL_0:def_1; percases ( b - s <= a or b - s > a ) ; supposeA16: b - s <= a ; ::_thesis: contradiction A17: (a + b) / 2 in ].a,b.[ by A4, RCOMP_1:def_2; (a + b) / 2 > b - s by A3, A16, XXREAL_0:2; hence contradiction by A15, A17; ::_thesis: verum end; supposeA18: b - s > a ; ::_thesis: contradiction A19: b - s < b - 0 by A14, XREAL_1:15; then b - s < (b + (b - s)) / 2 by XREAL_1:226; then A20: a < (b + (b - s)) / 2 by A18, XXREAL_0:2; (b + (b - s)) / 2 < b by A19, XREAL_1:226; then (b + (b - s)) / 2 in { r where r is Real : ( a < r & r < b ) } by A20; then (b + (b - s)) / 2 in ].a,b.[ by RCOMP_1:def_2; hence contradiction by A15, A19, XREAL_1:226; ::_thesis: verum end; end; end; a is LowerBound of ].a,b.[ proof let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in ].a,b.[ or a <= r ) assume r in ].a,b.[ ; ::_thesis: a <= r then r in { l where l is Real : ( a < l & l < b ) } by RCOMP_1:def_2; then ex r1 being Real st ( r1 = r & a < r1 & r1 < b ) ; hence a <= r ; ::_thesis: verum end; then A21: ].a,b.[ is bounded_below by XXREAL_2:def_9; A22: for r being real number st r in ].a,b.[ holds a <= r proof let r be real number ; ::_thesis: ( r in ].a,b.[ implies a <= r ) assume r in ].a,b.[ ; ::_thesis: a <= r then r in { l where l is Real : ( a < l & l < b ) } by RCOMP_1:def_2; then ex r1 being Real st ( r1 = r & a < r1 & r1 < b ) ; hence a <= r ; ::_thesis: verum end; b is UpperBound of ].a,b.[ proof let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in ].a,b.[ or r <= b ) assume r in ].a,b.[ ; ::_thesis: r <= b then r in { l where l is Real : ( a < l & l < b ) } by RCOMP_1:def_2; then ex r1 being Real st ( r1 = r & a < r1 & r1 < b ) ; hence r <= b ; ::_thesis: verum end; then A23: ].a,b.[ is bounded_above by XXREAL_2:def_10; A24: for r being real number st r in ].a,b.[ holds b >= r proof let r be real number ; ::_thesis: ( r in ].a,b.[ implies b >= r ) assume r in ].a,b.[ ; ::_thesis: b >= r then r in { l where l is Real : ( a < l & l < b ) } by RCOMP_1:def_2; then ex r1 being Real st ( r1 = r & a < r1 & r1 < b ) ; hence b >= r ; ::_thesis: verum end; (a + b) / 2 in ].a,b.[ by A4, RCOMP_1:def_2; hence ( lower_bound ].a,b.[ = a & upper_bound ].a,b.[ = b ) by A21, A23, A22, A5, A24, A13, SEQ_4:def_1, SEQ_4:def_2; ::_thesis: verum end; begin registration let T be TopStruct ; let A be finite Subset of T; clusterT | A -> finite ; coherence T | A is finite by PRE_TOPC:8; end; registration let T be TopStruct ; cluster empty -> connected for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is empty holds b1 is connected proof let C be Subset of T; ::_thesis: ( C is empty implies C is connected ) assume C is empty ; ::_thesis: C is connected then reconsider D = C as empty Subset of T ; let A, B be Subset of (T | C); :: according to CONNSP_1:def_2,CONNSP_1:def_3 ::_thesis: ( not [#] (T | C) = A \/ B or not A,B are_separated or A = {} (T | C) or B = {} (T | C) ) assume that [#] (T | C) = A \/ B and A,B are_separated ; ::_thesis: ( A = {} (T | C) or B = {} (T | C) ) [#] (T | D) = {} ; hence ( A = {} (T | C) or B = {} (T | C) ) ; ::_thesis: verum end; end; theorem :: TOPREAL6:18 canceled; theorem Th19: :: TOPREAL6:19 for S, T being TopSpace st S,T are_homeomorphic & S is connected holds T is connected proof let S, T be TopSpace; ::_thesis: ( S,T are_homeomorphic & S is connected implies T is connected ) given f being Function of S,T such that A1: f is being_homeomorphism ; :: according to T_0TOPSP:def_1 ::_thesis: ( not S is connected or T is connected ) A2: rng f = [#] T by A1, TOPS_2:def_5; assume A3: S is connected ; ::_thesis: T is connected dom f = [#] S by A1, TOPS_2:def_5; then f .: ([#] S) = [#] T by A2, RELAT_1:113; hence T is connected by A1, A3, CONNSP_1:14; ::_thesis: verum end; theorem :: TOPREAL6:20 for T being TopSpace for 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; ::_thesis: for 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 let F be finite Subset-Family of T; ::_thesis: ( ( for X being Subset of T st X in F holds X is compact ) implies union F is compact ) assume A1: for X being Subset of T st X in F holds X is compact ; ::_thesis: union F is compact defpred S1[ set ] means ex A being Subset of T st ( A = union \$1 & A is compact ); A2: for x, B being set st x in F & B c= F & S1[B] holds S1[B \/ {x}] proof let x, B be set ; ::_thesis: ( x in F & B c= F & S1[B] implies S1[B \/ {x}] ) assume that A3: x in F and A4: B c= F ; ::_thesis: ( not S1[B] or S1[B \/ {x}] ) B c= bool the carrier of T proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in B or b in bool the carrier of T ) assume b in B ; ::_thesis: b in bool the carrier of T then b in F by A4; hence b in bool the carrier of T ; ::_thesis: verum end; then reconsider C = B as Subset-Family of T ; reconsider X = x as Subset of T by A3; given A being Subset of T such that A5: A = union B and A6: A is compact ; ::_thesis: S1[B \/ {x}] set K = (union C) \/ X; take (union C) \/ X ; ::_thesis: ( (union C) \/ X = union (B \/ {x}) & (union C) \/ X is compact ) union {x} = x by ZFMISC_1:25; hence (union C) \/ X = union (B \/ {x}) by ZFMISC_1:78; ::_thesis: (union C) \/ X is compact X is compact by A1, A3; hence (union C) \/ X is compact by A5, A6, COMPTS_1:10; ::_thesis: verum end; A7: S1[ {} ] proof take {} T ; ::_thesis: ( {} T = union {} & {} T is compact ) thus ( {} T = union {} & {} T is compact ) by ZFMISC_1:2; ::_thesis: verum end; A8: F is finite ; S1[F] from FINSET_1:sch_2(A8, A7, A2); hence union F is compact ; ::_thesis: verum end; begin theorem Th21: :: TOPREAL6:21 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 ; ::_thesis: ( A c= B & C c= D implies product ((a,b) --> (A,C)) c= product ((a,b) --> (B,D)) ) assume that A1: A c= B and A2: C c= D ; ::_thesis: product ((a,b) --> (A,C)) c= product ((a,b) --> (B,D)) set f = (a,b) --> (A,C); set g = (a,b) --> (B,D); A3: dom ((a,b) --> (A,C)) = {a,b} by FUNCT_4:62; A4: for x being set st x in dom ((a,b) --> (A,C)) holds ((a,b) --> (A,C)) . x c= ((a,b) --> (B,D)) . x proof let x be set ; ::_thesis: ( x in dom ((a,b) --> (A,C)) implies ((a,b) --> (A,C)) . x c= ((a,b) --> (B,D)) . x ) assume x in dom ((a,b) --> (A,C)) ; ::_thesis: ((a,b) --> (A,C)) . x c= ((a,b) --> (B,D)) . x then A5: ( x = a or x = b ) by A3, TARSKI:def_2; percases ( a <> b or a = b ) ; supposeA6: a <> b ; ::_thesis: ((a,b) --> (A,C)) . x c= ((a,b) --> (B,D)) . x A7: ((a,b) --> (A,C)) . b = C by FUNCT_4:63; ((a,b) --> (A,C)) . a = A by A6, FUNCT_4:63; hence ((a,b) --> (A,C)) . x c= ((a,b) --> (B,D)) . x by A1, A2, A5, A6, A7, FUNCT_4:63; ::_thesis: verum end; supposeA8: a = b ; ::_thesis: ((a,b) --> (A,C)) . x c= ((a,b) --> (B,D)) . x then (a,b) --> (A,C) = a .--> C by FUNCT_4:81; then A9: ((a,b) --> (A,C)) . a = C by FUNCOP_1:72; (a,b) --> (B,D) = a .--> D by A8, FUNCT_4:81; hence ((a,b) --> (A,C)) . x c= ((a,b) --> (B,D)) . x by A2, A5, A8, A9, FUNCOP_1:72; ::_thesis: verum end; end; end; dom ((a,b) --> (B,D)) = {a,b} by FUNCT_4:62; hence product ((a,b) --> (A,C)) c= product ((a,b) --> (B,D)) by A4, CARD_3:27, FUNCT_4:62; ::_thesis: verum end; theorem Th22: :: TOPREAL6:22 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; ::_thesis: product ((1,2) --> (A,B)) is Subset of (TOP-REAL 2) set f = (1,2) --> (A,B); product ((1,2) --> (A,B)) c= the carrier of (TOP-REAL 2) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in product ((1,2) --> (A,B)) or a in the carrier of (TOP-REAL 2) ) A1: ((1,2) --> (A,B)) . 1 = A by FUNCT_4:63; A2: ((1,2) --> (A,B)) . 2 = B by FUNCT_4:63; assume a in product ((1,2) --> (A,B)) ; ::_thesis: a in the carrier of (TOP-REAL 2) then consider g being Function such that A3: a = g and A4: dom g = dom ((1,2) --> (A,B)) and A5: for x being set st x in dom ((1,2) --> (A,B)) holds g . x in ((1,2) --> (A,B)) . x by CARD_3:def_5; A6: dom ((1,2) --> (A,B)) = {1,2} by FUNCT_4:62; then 2 in dom ((1,2) --> (A,B)) by TARSKI:def_2; then A7: g . 2 in B by A5, A2; 1 in dom ((1,2) --> (A,B)) by A6, TARSKI:def_2; then g . 1 in A by A5, A1; then reconsider m = g . 1, n = g . 2 as Real by A7; A8: now__::_thesis:_for_k_being_set_st_k_in_dom_g_holds_ g_._k_=_<*(g_._1),(g_._2)*>_._k let k be set ; ::_thesis: ( k in dom g implies g . k = <*(g . 1),(g . 2)*> . k ) assume k in dom g ; ::_thesis: g . k = <*(g . 1),(g . 2)*> . k then ( k = 1 or k = 2 ) by A4, TARSKI:def_2; hence g . k = <*(g . 1),(g . 2)*> . k by FINSEQ_1:44; ::_thesis: verum end; dom <*(g . 1),(g . 2)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; then a = |[m,n]| by A3, A4, A8, FUNCT_1:2, FUNCT_4:62; hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; hence product ((1,2) --> (A,B)) is Subset of (TOP-REAL 2) ; ::_thesis: verum end; theorem :: TOPREAL6:23 for a being Real holds ( |.|[0,a]|.| = abs a & |.|[a,0]|.| = abs a ) proof let a be Real; ::_thesis: ( |.|[0,a]|.| = abs a & |.|[a,0]|.| = abs a ) |.<*0,a*>.| = sqrt (Sum <*(0 ^2),(a ^2)*>) by Th11 .= sqrt (0 + (a ^2)) by RVSUM_1:77 .= abs a by COMPLEX1:72 ; hence |.|[0,a]|.| = abs a ; ::_thesis: |.|[a,0]|.| = abs a |.<*a,0*>.| = sqrt (Sum <*(a ^2),(0 ^2)*>) by Th11 .= sqrt ((a ^2) + 0) by RVSUM_1:77 .= abs a by COMPLEX1:72 ; hence |.|[a,0]|.| = abs a ; ::_thesis: verum end; theorem Th24: :: TOPREAL6:24 for p being Point of (Euclid 2) for q being Point of (TOP-REAL 2) st p = 0. (TOP-REAL 2) & p = q holds ( q = <*0,0*> & q `1 = 0 & q `2 = 0 ) proof let p be Point of (Euclid 2); ::_thesis: for q being Point of (TOP-REAL 2) st p = 0. (TOP-REAL 2) & p = q holds ( q = <*0,0*> & q `1 = 0 & q `2 = 0 ) let q be Point of (TOP-REAL 2); ::_thesis: ( p = 0. (TOP-REAL 2) & p = q implies ( q = <*0,0*> & q `1 = 0 & q `2 = 0 ) ) assume that A1: p = 0. (TOP-REAL 2) and A2: p = q ; ::_thesis: ( q = <*0,0*> & q `1 = 0 & q `2 = 0 ) 0.REAL 2 = 0. (TOP-REAL 2) by EUCLID:66; then p = <*0,0*> by A1, FINSEQ_2:61; hence ( q = <*0,0*> & q `1 = 0 & q `2 = 0 ) by A2, EUCLID:52; ::_thesis: verum end; theorem :: TOPREAL6:25 for p, q being Point of (Euclid 2) for 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); ::_thesis: for z being Point of (TOP-REAL 2) st p = 0.REAL 2 & q = z holds dist (p,q) = |.z.| let z be Point of (TOP-REAL 2); ::_thesis: ( p = 0.REAL 2 & q = z implies dist (p,q) = |.z.| ) assume that A1: p = 0.REAL 2 and A2: q = z ; ::_thesis: dist (p,q) = |.z.| reconsider P = p as Point of (TOP-REAL 2) by TOPREAL3:8; A3: 0.REAL 2 = 0. (TOP-REAL 2) by EUCLID:66; then A4: P `1 = 0 by A1, Th24; A5: P `2 = 0 by A1, A3, Th24; dist (p,q) = (Pitag_dist 2) . (p,q) by METRIC_1:def_1 .= sqrt ((((P `1) - (z `1)) ^2) + (((P `2) - (z `2)) ^2)) by A2, TOPREAL3:7 .= sqrt (((z `1) ^2) + ((z `2) ^2)) by A4, A5 ; hence dist (p,q) = |.z.| by JGRAPH_1:30; ::_thesis: verum end; theorem Th26: :: TOPREAL6:26 for r being Real for p being Point of (TOP-REAL 2) holds r * p = |[(r * (p `1)),(r * (p `2))]| proof let r be Real; ::_thesis: for p being Point of (TOP-REAL 2) holds r * p = |[(r * (p `1)),(r * (p `2))]| let p be Point of (TOP-REAL 2); ::_thesis: r * p = |[(r * (p `1)),(r * (p `2))]| p = |[(p `1),(p `2)]| by EUCLID:53; hence r * p = |[(r * (p `1)),(r * (p `2))]| by EUCLID:58; ::_thesis: verum end; theorem Th27: :: TOPREAL6:27 for r being Real for s, p, q being Point of (TOP-REAL 2) st s = ((1 - r) * p) + (r * q) & s <> p & 0 <= r holds 0 < r proof let r be Real; ::_thesis: for s, p, q being Point of (TOP-REAL 2) st s = ((1 - r) * p) + (r * q) & s <> p & 0 <= r holds 0 < r let s, p, q be Point of (TOP-REAL 2); ::_thesis: ( s = ((1 - r) * p) + (r * q) & s <> p & 0 <= r implies 0 < r ) assume that A1: s = ((1 - r) * p) + (r * q) and A2: s <> p and A3: 0 <= r ; ::_thesis: 0 < r assume A4: r <= 0 ; ::_thesis: contradiction then s = ((1 - 0) * p) + (r * q) by A1, A3 .= ((1 - 0) * p) + (0 * q) by A3, A4 .= (1 * p) + (0. (TOP-REAL 2)) by EUCLID:29 .= 1 * p by EUCLID:27 .= p by EUCLID:29 ; hence contradiction by A2; ::_thesis: verum end; theorem Th28: :: TOPREAL6:28 for r being Real for s, p, q being Point of (TOP-REAL 2) st s = ((1 - r) * p) + (r * q) & s <> q & r <= 1 holds r < 1 proof let r be Real; ::_thesis: for s, p, q being Point of (TOP-REAL 2) st s = ((1 - r) * p) + (r * q) & s <> q & r <= 1 holds r < 1 let s, p, q be Point of (TOP-REAL 2); ::_thesis: ( s = ((1 - r) * p) + (r * q) & s <> q & r <= 1 implies r < 1 ) assume that A1: s = ((1 - r) * p) + (r * q) and A2: s <> q and A3: r <= 1 ; ::_thesis: r < 1 assume A4: r >= 1 ; ::_thesis: contradiction then s = ((1 - 1) * p) + (r * q) by A1, A3, XXREAL_0:1 .= (0 * p) + (1 * q) by A3, A4, XXREAL_0:1 .= (0. (TOP-REAL 2)) + (1 * q) by EUCLID:29 .= 1 * q by EUCLID:27 .= q by EUCLID:29 ; hence contradiction by A2; ::_thesis: verum end; theorem :: TOPREAL6:29 for s, p, q being Point of (TOP-REAL 2) st s in LSeg (p,q) & s <> p & s <> q & p `1 < q `1 holds ( p `1 < s `1 & s `1 < q `1 ) proof let s, p, q be Point of (TOP-REAL 2); ::_thesis: ( s in LSeg (p,q) & s <> p & s <> q & p `1 < q `1 implies ( p `1 < s `1 & s `1 < q `1 ) ) assume that A1: s in LSeg (p,q) and A2: s <> p and A3: s <> q and A4: p `1 < q `1 ; ::_thesis: ( p `1 < s `1 & s `1 < q `1 ) A5: (p `1) - (q `1) < 0 by A4, XREAL_1:49; consider r being Real such that A6: s = ((1 - r) * p) + (r * q) and A7: 0 <= r and A8: r <= 1 by A1; (1 - r) * p = |[((1 - r) * (p `1)),((1 - r) * (p `2))]| by Th26; then A9: ((1 - r) * p) `1 = (1 - r) * (p `1) by EUCLID:52; r * q = |[(r * (q `1)),(r * (q `2))]| by Th26; then A10: (r * q) `1 = r * (q `1) by EUCLID:52; s = |[((((1 - r) * p) `1) + ((r * q) `1)),((((1 - r) * p) `2) + ((r * q) `2))]| by A6, EUCLID:55; then A11: s `1 = ((1 - r) * (p `1)) + (r * (q `1)) by A9, A10, EUCLID:52; then A12: (p `1) - (s `1) = r * ((p `1) - (q `1)) ; r < 1 by A3, A6, A8, Th28; then A13: 1 - r > 0 by XREAL_1:50; A14: (q `1) - (p `1) > 0 by A4, XREAL_1:50; r > 0 by A2, A6, A7, Th27; then A15: (p `1) - (s `1) < 0 by A12, A5, XREAL_1:132; (q `1) - (s `1) = (1 - r) * ((q `1) - (p `1)) by A11; then (q `1) - (s `1) > 0 by A14, A13, XREAL_1:129; hence ( p `1 < s `1 & s `1 < q `1 ) by A15, XREAL_1:47, XREAL_1:48; ::_thesis: verum end; theorem :: TOPREAL6:30 for s, p, q being Point of (TOP-REAL 2) st s in LSeg (p,q) & s <> p & s <> q & p `2 < q `2 holds ( p `2 < s `2 & s `2 < q `2 ) proof let s, p, q be Point of (TOP-REAL 2); ::_thesis: ( s in LSeg (p,q) & s <> p & s <> q & p `2 < q `2 implies ( p `2 < s `2 & s `2 < q `2 ) ) assume that A1: s in LSeg (p,q) and A2: s <> p and A3: s <> q and A4: p `2 < q `2 ; ::_thesis: ( p `2 < s `2 & s `2 < q `2 ) A5: (p `2) - (q `2) < 0 by A4, XREAL_1:49; consider r being Real such that A6: s = ((1 - r) * p) + (r * q) and A7: 0 <= r and A8: r <= 1 by A1; (1 - r) * p = |[((1 - r) * (p `1)),((1 - r) * (p `2))]| by Th26; then A9: ((1 - r) * p) `2 = (1 - r) * (p `2) by EUCLID:52; r * q = |[(r * (q `1)),(r * (q `2))]| by Th26; then A10: (r * q) `2 = r * (q `2) by EUCLID:52; s = |[((((1 - r) * p) `1) + ((r * q) `1)),((((1 - r) * p) `2) + ((r * q) `2))]| by A6, EUCLID:55; then A11: s `2 = ((1 - r) * (p `2)) + (r * (q `2)) by A9, A10, EUCLID:52; then A12: (p `2) - (s `2) = r * ((p `2) - (q `2)) ; r < 1 by A3, A6, A8, Th28; then A13: 1 - r > 0 by XREAL_1:50; A14: (q `2) - (p `2) > 0 by A4, XREAL_1:50; r > 0 by A2, A6, A7, Th27; then A15: (p `2) - (s `2) < 0 by A12, A5, XREAL_1:132; (q `2) - (s `2) = (1 - r) * ((q `2) - (p `2)) by A11; then (q `2) - (s `2) > 0 by A14, A13, XREAL_1:129; hence ( p `2 < s `2 & s `2 < q `2 ) by A15, XREAL_1:47, XREAL_1:48; ::_thesis: verum end; theorem :: TOPREAL6:31 for D being non empty Subset of (TOP-REAL 2) 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 D be non empty Subset of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st ( q `1 < W-bound D & p <> q ) let p be Point of (TOP-REAL 2); ::_thesis: ex q being Point of (TOP-REAL 2) st ( q `1 < W-bound D & p <> q ) take q = |[((W-bound D) - 1),((p `2) - 1)]|; ::_thesis: ( q `1 < W-bound D & p <> q ) (W-bound D) - 1 < (W-bound D) - 0 by XREAL_1:15; hence q `1 < W-bound D by EUCLID:52; ::_thesis: p <> q (p `2) - 1 < (p `2) - 0 by XREAL_1:15; hence p <> q by EUCLID:52; ::_thesis: verum end; theorem :: TOPREAL6:32 for D being non empty Subset of (TOP-REAL 2) 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 D be non empty Subset of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st ( q `1 > E-bound D & p <> q ) let p be Point of (TOP-REAL 2); ::_thesis: ex q being Point of (TOP-REAL 2) st ( q `1 > E-bound D & p <> q ) take q = |[((E-bound D) + 1),((p `2) - 1)]|; ::_thesis: ( q `1 > E-bound D & p <> q ) (E-bound D) + 1 > (E-bound D) + 0 by XREAL_1:6; hence q `1 > E-bound D by EUCLID:52; ::_thesis: p <> q (p `2) - 1 < (p `2) - 0 by XREAL_1:15; hence p <> q by EUCLID:52; ::_thesis: verum end; theorem :: TOPREAL6:33 for D being non empty Subset of (TOP-REAL 2) 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 D be non empty Subset of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st ( q `2 > N-bound D & p <> q ) let p be Point of (TOP-REAL 2); ::_thesis: ex q being Point of (TOP-REAL 2) st ( q `2 > N-bound D & p <> q ) take q = |[((p `1) - 1),((N-bound D) + 1)]|; ::_thesis: ( q `2 > N-bound D & p <> q ) (N-bound D) + 1 > (N-bound D) + 0 by XREAL_1:6; hence q `2 > N-bound D by EUCLID:52; ::_thesis: p <> q (p `1) - 1 < (p `1) - 0 by XREAL_1:15; hence p <> q by EUCLID:52; ::_thesis: verum end; theorem :: TOPREAL6:34 for D being non empty Subset of (TOP-REAL 2) 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 D be non empty Subset of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st ( q `2 < S-bound D & p <> q ) let p be Point of (TOP-REAL 2); ::_thesis: ex q being Point of (TOP-REAL 2) st ( q `2 < S-bound D & p <> q ) take q = |[((p `1) - 1),((S-bound D) - 1)]|; ::_thesis: ( q `2 < S-bound D & p <> q ) (S-bound D) - 1 < (S-bound D) - 0 by XREAL_1:15; hence q `2 < S-bound D by EUCLID:52; ::_thesis: p <> q (p `1) - 1 < (p `1) - 0 by XREAL_1:15; hence p <> q by EUCLID:52; ::_thesis: verum end; registration cluster non horizontal -> non empty for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Subset of (TOP-REAL 2) st not b1 is horizontal holds not b1 is empty proof let P be Subset of (TOP-REAL 2); ::_thesis: ( not P is horizontal implies not P is empty ) assume not P is horizontal ; ::_thesis: not P is empty 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 not P is empty ; ::_thesis: verum end; cluster non vertical -> non empty for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Subset of (TOP-REAL 2) st not b1 is vertical holds not b1 is empty proof let P be Subset of (TOP-REAL 2); ::_thesis: ( not P is vertical implies not P is empty ) assume not P is vertical ; ::_thesis: not P is empty 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 not P is empty ; ::_thesis: verum end; cluster being_Region -> open connected for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Subset of (TOP-REAL 2) st b1 is being_Region holds ( b1 is open & b1 is connected ) by TOPREAL4:def_3; cluster open connected -> being_Region for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Subset of (TOP-REAL 2) st b1 is open & b1 is connected holds b1 is being_Region by TOPREAL4:def_3; end; registration cluster empty -> horizontal for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Subset of (TOP-REAL 2) st b1 is empty holds b1 is horizontal ; cluster empty -> vertical for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Subset of (TOP-REAL 2) st b1 is empty holds b1 is vertical ; end; registration cluster non empty convex for Element of bool the carrier of (TOP-REAL 2); existence ex b1 being Subset of (TOP-REAL 2) st ( not b1 is empty & b1 is convex ) proof set C = the non empty convex Subset of (TOP-REAL 2); take the non empty convex Subset of (TOP-REAL 2) ; ::_thesis: ( not the non empty convex Subset of (TOP-REAL 2) is empty & the non empty convex Subset of (TOP-REAL 2) is convex ) thus ( not the non empty convex Subset of (TOP-REAL 2) is empty & the non empty convex Subset of (TOP-REAL 2) is convex ) ; ::_thesis: verum end; end; registration let a, b be Point of (TOP-REAL 2); cluster LSeg (a,b) -> connected ; coherence LSeg (a,b) is connected ; end; registration cluster R^2-unit_square -> connected ; coherence R^2-unit_square is connected proof A1: LSeg (|[0,1]|,|[1,1]|) meets LSeg (|[1,0]|,|[1,1]|) by TOPREAL1:18, XBOOLE_0:def_7; A2: LSeg (|[0,0]|,|[1,0]|) meets LSeg (|[1,0]|,|[1,1]|) by TOPREAL1:16, XBOOLE_0:def_7; A3: LSeg (|[0,0]|,|[0,1]|) meets LSeg (|[0,1]|,|[1,1]|) by TOPREAL1:15, XBOOLE_0:def_7; 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:def_2, XBOOLE_1:4; hence R^2-unit_square is connected by A3, A2, A1, JORDAN1:5; ::_thesis: verum end; end; registration cluster being_simple_closed_curve -> connected for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Subset of (TOP-REAL 2) st b1 is being_simple_closed_curve holds b1 is connected proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve implies P is connected ) given f being Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | P) such that A1: f is being_homeomorphism ; :: according to TOPREAL2:def_1 ::_thesis: P is connected A2: (TOP-REAL 2) | R^2-unit_square,(TOP-REAL 2) | P are_homeomorphic proof take f ; :: according to T_0TOPSP:def_1 ::_thesis: f is being_homeomorphism thus f is being_homeomorphism by A1; ::_thesis: verum end; (TOP-REAL 2) | R^2-unit_square is connected by CONNSP_1:def_3; then (TOP-REAL 2) | P is connected by A2, Th19; hence P is connected by CONNSP_1:def_3; ::_thesis: verum end; end; theorem :: TOPREAL6:35 for P being Subset of (TOP-REAL 2) holds LSeg ((NE-corner P),(SE-corner P)) c= L~ (SpStSeq P) proof let P be Subset of (TOP-REAL 2); ::_thesis: LSeg ((NE-corner P),(SE-corner P)) c= L~ (SpStSeq P) A1: (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; 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; 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 LSeg ((NE-corner P),(SE-corner P)) c= L~ (SpStSeq P) by SPRECT_1:41; ::_thesis: verum end; theorem :: TOPREAL6:36 for P being Subset of (TOP-REAL 2) holds LSeg ((SW-corner P),(SE-corner P)) c= L~ (SpStSeq P) proof let P be Subset of (TOP-REAL 2); ::_thesis: LSeg ((SW-corner P),(SE-corner P)) c= L~ (SpStSeq P) ((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 A1: ((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; 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; 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 LSeg ((SW-corner P),(SE-corner P)) c= L~ (SpStSeq P) by SPRECT_1:41; ::_thesis: verum end; theorem :: TOPREAL6:37 for P being Subset of (TOP-REAL 2) holds LSeg ((SW-corner P),(NW-corner P)) c= L~ (SpStSeq P) proof let P be Subset of (TOP-REAL 2); ::_thesis: LSeg ((SW-corner P),(NW-corner P)) c= L~ (SpStSeq P) 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 LSeg ((SW-corner P),(NW-corner P)) c= L~ (SpStSeq P) by SPRECT_1:41; ::_thesis: verum end; theorem :: TOPREAL6:38 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 connected convex Subset of (TOP-REAL 2) proof let C be Subset of (TOP-REAL 2); ::_thesis: { p where p is Point of (TOP-REAL 2) : p `1 < W-bound C } is non empty connected convex Subset of (TOP-REAL 2) set A = { p where p is Point of (TOP-REAL 2) : p `1 < W-bound C } ; { p where p is Point of (TOP-REAL 2) : p `1 < W-bound C } c= the carrier of (TOP-REAL 2) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { p where p is Point of (TOP-REAL 2) : p `1 < W-bound C } or a in the carrier of (TOP-REAL 2) ) assume a in { p where p is Point of (TOP-REAL 2) : p `1 < W-bound C } ; ::_thesis: a in the carrier of (TOP-REAL 2) then ex p being Point of (TOP-REAL 2) st ( a = p & p `1 < W-bound C ) ; hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; then reconsider A = { p where p is Point of (TOP-REAL 2) : p `1 < W-bound C } as Subset of (TOP-REAL 2) ; set p = W-bound C; set b = |[((W-bound C) - 1),0]|; A1: |[((W-bound C) - 1),0]| `1 = (W-bound C) - 1 by EUCLID:52; (W-bound C) - 1 < (W-bound C) - 0 by XREAL_1:15; then A2: |[((W-bound C) - 1),0]| in A by A1; A is convex proof let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def_1 ::_thesis: ( not w1 in A or not w2 in A or LSeg (w1,w2) c= A ) assume w1 in A ; ::_thesis: ( not w2 in A or LSeg (w1,w2) c= A ) then consider p being Point of (TOP-REAL 2) such that A3: w1 = p and A4: p `1 < W-bound C ; assume w2 in A ; ::_thesis: LSeg (w1,w2) c= A then consider q being Point of (TOP-REAL 2) such that A5: w2 = q and A6: q `1 < W-bound C ; let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in LSeg (w1,w2) or k in A ) assume A7: k in LSeg (w1,w2) ; ::_thesis: k in A then reconsider z = k as Point of (TOP-REAL 2) ; percases ( p `1 < q `1 or q `1 < p `1 or p `1 = q `1 ) by XXREAL_0:1; suppose p `1 < q `1 ; ::_thesis: k in A then z `1 <= w2 `1 by A3, A5, A7, TOPREAL1:3; then z `1 < W-bound C by A5, A6, XXREAL_0:2; hence k in A ; ::_thesis: verum end; suppose q `1 < p `1 ; ::_thesis: k in A then z `1 <= w1 `1 by A3, A5, A7, TOPREAL1:3; then z `1 < W-bound C by A3, A4, XXREAL_0:2; hence k in A ; ::_thesis: verum end; suppose p `1 = q `1 ; ::_thesis: k in A then z `1 = p `1 by A3, A5, A7, GOBOARD7:5; hence k in A by A4; ::_thesis: verum end; end; end; then reconsider A = A as non empty convex Subset of (TOP-REAL 2) by A2; A is connected ; hence { p where p is Point of (TOP-REAL 2) : p `1 < W-bound C } is non empty connected convex Subset of (TOP-REAL 2) ; ::_thesis: verum end; begin theorem Th39: :: TOPREAL6:39 for q, p being Point of (TOP-REAL 2) for e being Point of (Euclid 2) for r being real number st e = q & p in Ball (e,r) holds ( (q `1) - r < p `1 & p `1 < (q `1) + r ) proof let q, p be Point of (TOP-REAL 2); ::_thesis: for e being Point of (Euclid 2) for r being real number st e = q & p in Ball (e,r) holds ( (q `1) - r < p `1 & p `1 < (q `1) + r ) let e be Point of (Euclid 2); ::_thesis: for r being real number st e = q & p in Ball (e,r) holds ( (q `1) - r < p `1 & p `1 < (q `1) + r ) let r be real number ; ::_thesis: ( e = q & p in Ball (e,r) implies ( (q `1) - r < p `1 & p `1 < (q `1) + r ) ) assume that A1: e = q and A2: p in Ball (e,r) ; ::_thesis: ( (q `1) - r < p `1 & p `1 < (q `1) + r ) reconsider f = p as Point of (Euclid 2) by TOPREAL3:8; A3: dist (e,f) < r by A2, METRIC_1:11; A4: dist (e,f) = (Pitag_dist 2) . (e,f) by METRIC_1:def_1 .= sqrt ((((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2)) by A1, TOPREAL3:7 ; A5: r > 0 by A2, TBSP_1:12; assume A6: ( not (q `1) - r < p `1 or not p `1 < (q `1) + r ) ; ::_thesis: contradiction percases ( (q `1) - r >= p `1 or p `1 >= (q `1) + r ) by A6; supposeA7: (q `1) - r >= p `1 ; ::_thesis: contradiction ((q `2) - (p `2)) ^2 >= 0 by XREAL_1:63; then A8: (((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2) >= (((q `1) - (p `1)) ^2) + 0 by XREAL_1:6; (q `1) - (p `1) >= r by A7, XREAL_1:11; then ((q `1) - (p `1)) ^2 >= r ^2 by A5, SQUARE_1:15; then (((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2) >= r ^2 by A8, XXREAL_0:2; then sqrt ((((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2)) >= sqrt (r ^2) by A5, SQUARE_1:26; hence contradiction by A3, A4, A5, SQUARE_1:22; ::_thesis: verum end; supposeA9: p `1 >= (q `1) + r ; ::_thesis: contradiction ((q `2) - (p `2)) ^2 >= 0 by XREAL_1:63; then A10: (((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2) >= (((q `1) - (p `1)) ^2) + 0 by XREAL_1:6; (p `1) - (q `1) >= r by A9, XREAL_1:19; then (- ((q `1) - (p `1))) ^2 >= r ^2 by A5, SQUARE_1:15; then (((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2) >= r ^2 by A10, XXREAL_0:2; then sqrt ((((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2)) >= sqrt (r ^2) by A5, SQUARE_1:26; hence contradiction by A3, A4, A5, SQUARE_1:22; ::_thesis: verum end; end; end; theorem Th40: :: TOPREAL6:40 for q, p being Point of (TOP-REAL 2) for e being Point of (Euclid 2) for r being real number st e = q & p in Ball (e,r) holds ( (q `2) - r < p `2 & p `2 < (q `2) + r ) proof let q, p be Point of (TOP-REAL 2); ::_thesis: for e being Point of (Euclid 2) for r being real number st e = q & p in Ball (e,r) holds ( (q `2) - r < p `2 & p `2 < (q `2) + r ) let e be Point of (Euclid 2); ::_thesis: for r being real number st e = q & p in Ball (e,r) holds ( (q `2) - r < p `2 & p `2 < (q `2) + r ) let r be real number ; ::_thesis: ( e = q & p in Ball (e,r) implies ( (q `2) - r < p `2 & p `2 < (q `2) + r ) ) assume that A1: e = q and A2: p in Ball (e,r) ; ::_thesis: ( (q `2) - r < p `2 & p `2 < (q `2) + r ) reconsider f = p as Point of (Euclid 2) by TOPREAL3:8; A3: dist (e,f) < r by A2, METRIC_1:11; A4: dist (e,f) = (Pitag_dist 2) . (e,f) by METRIC_1:def_1 .= sqrt ((((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2)) by A1, TOPREAL3:7 ; A5: r > 0 by A2, TBSP_1:12; assume A6: ( not (q `2) - r < p `2 or not p `2 < (q `2) + r ) ; ::_thesis: contradiction percases ( (q `2) - r >= p `2 or p `2 >= (q `2) + r ) by A6; supposeA7: (q `2) - r >= p `2 ; ::_thesis: contradiction ((q `1) - (p `1)) ^2 >= 0 by XREAL_1:63; then A8: (((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2) >= (((q `2) - (p `2)) ^2) + 0 by XREAL_1:6; (q `2) - (p `2) >= r by A7, XREAL_1:11; then ((q `2) - (p `2)) ^2 >= r ^2 by A5, SQUARE_1:15; then (((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2) >= r ^2 by A8, XXREAL_0:2; then sqrt ((((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2)) >= sqrt (r ^2) by A5, SQUARE_1:26; hence contradiction by A3, A4, A5, SQUARE_1:22; ::_thesis: verum end; supposeA9: p `2 >= (q `2) + r ; ::_thesis: contradiction ((q `1) - (p `1)) ^2 >= 0 by XREAL_1:63; then A10: (((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2) >= (((q `2) - (p `2)) ^2) + 0 by XREAL_1:6; (p `2) - (q `2) >= r by A9, XREAL_1:19; then (- ((q `2) - (p `2))) ^2 >= r ^2 by A5, SQUARE_1:15; then (((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2) >= r ^2 by A10, XXREAL_0:2; then sqrt ((((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2)) >= sqrt (r ^2) by A5, SQUARE_1:26; hence contradiction by A3, A4, A5, SQUARE_1:22; ::_thesis: verum end; end; end; theorem Th41: :: TOPREAL6:41 for p being Point of (TOP-REAL 2) for e being Point of (Euclid 2) for r being real number st p = e holds 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 let p be Point of (TOP-REAL 2); ::_thesis: for e being Point of (Euclid 2) for r being real number st p = e holds 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) let e be Point of (Euclid 2); ::_thesis: for r being real number st p = e holds 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) let r be real number ; ::_thesis: ( 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) ) set A = ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[; set B = ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[; set f = (1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[); assume A1: p = e ; ::_thesis: 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) let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in product ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) or a in Ball (e,r) ) A2: ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ = { m where m is Real : ( (p `1) - (r / (sqrt 2)) < m & m < (p `1) + (r / (sqrt 2)) ) } by RCOMP_1:def_2; A3: ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) . 2 = ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ by FUNCT_4:63; A4: ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ = { n where n is Real : ( (p `2) - (r / (sqrt 2)) < n & n < (p `2) + (r / (sqrt 2)) ) } by RCOMP_1:def_2; A5: ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) . 1 = ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ by FUNCT_4:63; assume a in product ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) ; ::_thesis: a in Ball (e,r) then consider g being Function such that A6: a = g and A7: dom g = dom ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) and A8: for x being set st x in dom ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) holds g . x in ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) . x by CARD_3:def_5; A9: dom ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) = {1,2} by FUNCT_4:62; then 1 in dom ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) by TARSKI:def_2; then A10: g . 1 in ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ by A8, A5; then consider m being Real such that A11: m = g . 1 and (p `1) - (r / (sqrt 2)) < m and m < (p `1) + (r / (sqrt 2)) by A2; A12: 0 <= (m - (p `1)) ^2 by XREAL_1:63; 2 in dom ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) by A9, TARSKI:def_2; then A13: g . 2 in ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ by A8, A3; then consider n being Real such that A14: n = g . 2 and (p `2) - (r / (sqrt 2)) < n and n < (p `2) + (r / (sqrt 2)) by A4; abs (n - (p `2)) < r / (sqrt 2) by A13, A14, RCOMP_1:1; then (abs (n - (p `2))) ^2 < (r / (sqrt 2)) ^2 by COMPLEX1:46, SQUARE_1:16; then (abs (n - (p `2))) ^2 < (r ^2) / ((sqrt 2) ^2) by XCMPLX_1:76; then (abs (n - (p `2))) ^2 < (r ^2) / 2 by SQUARE_1:def_2; then A15: (n - (p `2)) ^2 < (r ^2) / 2 by COMPLEX1:75; (p `1) - ((p `1) + (r / (sqrt 2))) < (p `1) - ((p `1) - (r / (sqrt 2))) by A10, XREAL_1:15, XXREAL_1:28; then (- (r / (sqrt 2))) + (r / (sqrt 2)) < (r / (sqrt 2)) + (r / (sqrt 2)) by XREAL_1:6; then A16: 0 < r by SQUARE_1:19; A17: now__::_thesis:_for_k_being_set_st_k_in_dom_g_holds_ g_._k_=_<*(g_._1),(g_._2)*>_._k let k be set ; ::_thesis: ( k in dom g implies g . k = <*(g . 1),(g . 2)*> . k ) assume k in dom g ; ::_thesis: g . k = <*(g . 1),(g . 2)*> . k then ( k = 1 or k = 2 ) by A7, TARSKI:def_2; hence g . k = <*(g . 1),(g . 2)*> . k by FINSEQ_1:44; ::_thesis: verum end; A18: 0 <= (n - (p `2)) ^2 by XREAL_1:63; abs (m - (p `1)) < r / (sqrt 2) by A10, A11, RCOMP_1:1; then (abs (m - (p `1))) ^2 < (r / (sqrt 2)) ^2 by COMPLEX1:46, SQUARE_1:16; then (abs (m - (p `1))) ^2 < (r ^2) / ((sqrt 2) ^2) by XCMPLX_1:76; then (abs (m - (p `1))) ^2 < (r ^2) / 2 by SQUARE_1:def_2; then (m - (p `1)) ^2 < (r ^2) / 2 by COMPLEX1:75; then ((m - (p `1)) ^2) + ((n - (p `2)) ^2) < ((r ^2) / 2) + ((r ^2) / 2) by A15, XREAL_1:8; then sqrt (((m - (p `1)) ^2) + ((n - (p `2)) ^2)) < sqrt (r ^2) by A12, A18, SQUARE_1:27; then A19: sqrt (((m - (p `1)) ^2) + ((n - (p `2)) ^2)) < r by A16, SQUARE_1:22; dom <*(g . 1),(g . 2)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; then a = |[m,n]| by A6, A7, A11, A14, A17, FUNCT_1:2, FUNCT_4:62; then reconsider c = a as Point of (TOP-REAL 2) ; reconsider b = c as Point of (Euclid 2) by TOPREAL3:8; dist (b,e) = (Pitag_dist 2) . (b,e) by METRIC_1:def_1 .= sqrt ((((c `1) - (p `1)) ^2) + (((c `2) - (p `2)) ^2)) by A1, TOPREAL3:7 ; hence a in Ball (e,r) by A6, A11, A14, A19, METRIC_1:11; ::_thesis: verum end; theorem Th42: :: TOPREAL6:42 for p being Point of (TOP-REAL 2) for e being Point of (Euclid 2) for r being real number st p = e holds Ball (e,r) c= product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) proof let p be Point of (TOP-REAL 2); ::_thesis: for e being Point of (Euclid 2) for r being real number st p = e holds Ball (e,r) c= product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) let e be Point of (Euclid 2); ::_thesis: for r being real number st p = e holds Ball (e,r) c= product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) let r be real number ; ::_thesis: ( p = e implies Ball (e,r) c= product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) ) set A = ].((p `1) - r),((p `1) + r).[; set B = ].((p `2) - r),((p `2) + r).[; set f = (1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[); assume A1: p = e ; ::_thesis: Ball (e,r) c= product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Ball (e,r) or a in product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) ) assume A2: a in Ball (e,r) ; ::_thesis: a in product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) then reconsider b = a as Point of (Euclid 2) ; reconsider q = b as Point of (TOP-REAL 2) by TOPREAL3:8; reconsider g = q as FinSequence ; A3: for x being set st x in dom ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) holds g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x proof let x be set ; ::_thesis: ( x in dom ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) implies g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x ) assume A4: x in dom ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) ; ::_thesis: g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x percases ( x = 1 or x = 2 ) by A4, TARSKI:def_2; supposeA5: x = 1 ; ::_thesis: g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x A6: ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . 1 = ].((p `1) - r),((p `1) + r).[ by FUNCT_4:63; A7: q `1 < (p `1) + r by A1, A2, Th39; (p `1) - r < q `1 by A1, A2, Th39; hence g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x by A5, A6, A7, XXREAL_1:4; ::_thesis: verum end; supposeA8: x = 2 ; ::_thesis: g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x A9: ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . 2 = ].((p `2) - r),((p `2) + r).[ by FUNCT_4:63; A10: q `2 < (p `2) + r by A1, A2, Th40; (p `2) - r < q `2 by A1, A2, Th40; hence g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x by A8, A9, A10, XXREAL_1:4; ::_thesis: verum end; end; end; q is Function of (Seg 2),REAL by EUCLID:23; then A11: dom g = {1,2} by FINSEQ_1:2, FUNCT_2:def_1; dom ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) = {1,2} by FUNCT_4:62; hence a in product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) by A11, A3, CARD_3:9; ::_thesis: verum end; theorem Th43: :: TOPREAL6:43 for p being Point of (TOP-REAL 2) for e being Point of (Euclid 2) for P being Subset of (TOP-REAL 2) for r being real number st P = Ball (e,r) & p = e holds proj1 .: P = ].((p `1) - r),((p `1) + r).[ proof let p be Point of (TOP-REAL 2); ::_thesis: for e being Point of (Euclid 2) for P being Subset of (TOP-REAL 2) for r being real number st P = Ball (e,r) & p = e holds proj1 .: P = ].((p `1) - r),((p `1) + r).[ let e be Point of (Euclid 2); ::_thesis: for P being Subset of (TOP-REAL 2) for r being real number st P = Ball (e,r) & p = e holds proj1 .: P = ].((p `1) - r),((p `1) + r).[ let P be Subset of (TOP-REAL 2); ::_thesis: for r being real number st P = Ball (e,r) & p = e holds proj1 .: P = ].((p `1) - r),((p `1) + r).[ let r be real number ; ::_thesis: ( P = Ball (e,r) & p = e implies proj1 .: P = ].((p `1) - r),((p `1) + r).[ ) assume that A1: P = Ball (e,r) and A2: p = e ; ::_thesis: proj1 .: P = ].((p `1) - r),((p `1) + r).[ hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: ].((p `1) - r),((p `1) + r).[ c= proj1 .: P let a be set ; ::_thesis: ( a in proj1 .: P implies a in ].((p `1) - r),((p `1) + r).[ ) assume a in proj1 .: P ; ::_thesis: a in ].((p `1) - r),((p `1) + r).[ 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:64; reconsider b = a as Real by A5; reconsider x = x as Point of (TOP-REAL 2) by A3; A6: a = x `1 by A5, PSCOMP_1:def_5; then A7: b < (p `1) + r by A1, A2, A4, Th39; (p `1) - r < b by A1, A2, A4, A6, Th39; hence a in ].((p `1) - r),((p `1) + r).[ by A7, XXREAL_1:4; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ].((p `1) - r),((p `1) + r).[ or a in proj1 .: P ) assume A8: a in ].((p `1) - r),((p `1) + r).[ ; ::_thesis: a in proj1 .: P then reconsider b = a as Real ; reconsider f = |[b,(p `2)]| as Point of (Euclid 2) by TOPREAL3:8; A9: dist (f,e) = (Pitag_dist 2) . (f,e) by METRIC_1:def_1 .= sqrt ((((|[b,(p `2)]| `1) - (p `1)) ^2) + (((|[b,(p `2)]| `2) - (p `2)) ^2)) by A2, TOPREAL3:7 .= sqrt (((b - (p `1)) ^2) + (((|[b,(p `2)]| `2) - (p `2)) ^2)) by EUCLID:52 .= sqrt (((b - (p `1)) ^2) + (((p `2) - (p `2)) ^2)) by EUCLID:52 .= sqrt (((b - (p `1)) ^2) + 0) ; b < (p `1) + r by A8, XXREAL_1:4; then A10: b - (p `1) < ((p `1) + r) - (p `1) by XREAL_1:9; now__::_thesis:_(_(_0_<=_b_-_(p_`1)_&_dist_(f,e)_<_r_)_or_(_0_>_b_-_(p_`1)_&_dist_(f,e)_<_r_)_) percases ( 0 <= b - (p `1) or 0 > b - (p `1) ) ; case 0 <= b - (p `1) ; ::_thesis: dist (f,e) < r hence dist (f,e) < r by A10, A9, SQUARE_1:22; ::_thesis: verum end; caseA11: 0 > b - (p `1) ; ::_thesis: dist (f,e) < r (p `1) - r < b by A8, XXREAL_1:4; then ((p `1) - r) + r < b + r by XREAL_1:6; then A12: (p `1) - b < (r + b) - b by XREAL_1:9; sqrt ((b - (p `1)) ^2) = sqrt ((- (b - (p `1))) ^2) .= - (b - (p `1)) by A11, SQUARE_1:22 ; hence dist (f,e) < r by A9, A12; ::_thesis: verum end; end; end; then A13: |[b,(p `2)]| in P by A1, METRIC_1:11; a = |[b,(p `2)]| `1 by EUCLID:52 .= proj1 . |[b,(p `2)]| by PSCOMP_1:def_5 ; hence a in proj1 .: P by A13, FUNCT_2:35; ::_thesis: verum end; theorem Th44: :: TOPREAL6:44 for p being Point of (TOP-REAL 2) for e being Point of (Euclid 2) for P being Subset of (TOP-REAL 2) for r being real number st P = Ball (e,r) & p = e holds proj2 .: P = ].((p `2) - r),((p `2) + r).[ proof let p be Point of (TOP-REAL 2); ::_thesis: for e being Point of (Euclid 2) for P being Subset of (TOP-REAL 2) for r being real number st P = Ball (e,r) & p = e holds proj2 .: P = ].((p `2) - r),((p `2) + r).[ let e be Point of (Euclid 2); ::_thesis: for P being Subset of (TOP-REAL 2) for r being real number st P = Ball (e,r) & p = e holds proj2 .: P = ].((p `2) - r),((p `2) + r).[ let P be Subset of (TOP-REAL 2); ::_thesis: for r being real number st P = Ball (e,r) & p = e holds proj2 .: P = ].((p `2) - r),((p `2) + r).[ let r be real number ; ::_thesis: ( P = Ball (e,r) & p = e implies proj2 .: P = ].((p `2) - r),((p `2) + r).[ ) assume that A1: P = Ball (e,r) and A2: p = e ; ::_thesis: proj2 .: P = ].((p `2) - r),((p `2) + r).[ hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: ].((p `2) - r),((p `2) + r).[ c= proj2 .: P let a be set ; ::_thesis: ( a in proj2 .: P implies a in ].((p `2) - r),((p `2) + r).[ ) assume a in proj2 .: P ; ::_thesis: a in ].((p `2) - r),((p `2) + r).[ 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:64; reconsider b = a as Real by A5; reconsider x = x as Point of (TOP-REAL 2) by A3; A6: a = x `2 by A5, PSCOMP_1:def_6; then A7: b < (p `2) + r by A1, A2, A4, Th40; (p `2) - r < b by A1, A2, A4, A6, Th40; hence a in ].((p `2) - r),((p `2) + r).[ by A7, XXREAL_1:4; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ].((p `2) - r),((p `2) + r).[ or a in proj2 .: P ) assume A8: a in ].((p `2) - r),((p `2) + r).[ ; ::_thesis: a in proj2 .: P then reconsider b = a as Real ; reconsider f = |[(p `1),b]| as Point of (Euclid 2) by TOPREAL3:8; A9: dist (f,e) = (Pitag_dist 2) . (f,e) by METRIC_1:def_1 .= sqrt ((((|[(p `1),b]| `1) - (p `1)) ^2) + (((|[(p `1),b]| `2) - (p `2)) ^2)) by A2, TOPREAL3:7 .= sqrt ((((p `1) - (p `1)) ^2) + (((|[(p `1),b]| `2) - (p `2)) ^2)) by EUCLID:52 .= sqrt (0 + ((b - (p `2)) ^2)) by EUCLID:52 ; b < (p `2) + r by A8, XXREAL_1:4; then A10: b - (p `2) < ((p `2) + r) - (p `2) by XREAL_1:9; now__::_thesis:_(_(_0_<=_b_-_(p_`2)_&_dist_(f,e)_<_r_)_or_(_0_>_b_-_(p_`2)_&_dist_(f,e)_<_r_)_) percases ( 0 <= b - (p `2) or 0 > b - (p `2) ) ; case 0 <= b - (p `2) ; ::_thesis: dist (f,e) < r hence dist (f,e) < r by A10, A9, SQUARE_1:22; ::_thesis: verum end; caseA11: 0 > b - (p `2) ; ::_thesis: dist (f,e) < r (p `2) - r < b by A8, XXREAL_1:4; then ((p `2) - r) + r < b + r by XREAL_1:6; then A12: (p `2) - b < (r + b) - b by XREAL_1:9; sqrt ((b - (p `2)) ^2) = sqrt ((- (b - (p `2))) ^2) .= - (b - (p `2)) by A11, SQUARE_1:22 ; hence dist (f,e) < r by A9, A12; ::_thesis: verum end; end; end; then A13: |[(p `1),b]| in P by A1, METRIC_1:11; a = |[(p `1),b]| `2 by EUCLID:52 .= proj2 . |[(p `1),b]| by PSCOMP_1:def_6 ; hence a in proj2 .: P by A13, FUNCT_2:35; ::_thesis: verum end; theorem :: TOPREAL6:45 for p being Point of (TOP-REAL 2) for e being Point of (Euclid 2) for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) & p = e holds W-bound D = (p `1) - r proof let p be Point of (TOP-REAL 2); ::_thesis: for e being Point of (Euclid 2) for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) & p = e holds W-bound D = (p `1) - r let e be Point of (Euclid 2); ::_thesis: for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) & p = e holds W-bound D = (p `1) - r let D be non empty Subset of (TOP-REAL 2); ::_thesis: for r being real number st D = Ball (e,r) & p = e holds W-bound D = (p `1) - r let r be real number ; ::_thesis: ( D = Ball (e,r) & p = e implies W-bound D = (p `1) - r ) assume that A1: D = Ball (e,r) and A2: p = e ; ::_thesis: W-bound D = (p `1) - r r > 0 by A1, TBSP_1:12; then A3: (p `1) + 0 < (p `1) + r by XREAL_1:6; (p `1) - r < (p `1) - 0 by A1, TBSP_1:12, XREAL_1:15; then (p `1) - r < (p `1) + r by A3, XXREAL_0:2; then A4: lower_bound ].((p `1) - r),((p `1) + r).[ = (p `1) - r by Th17; proj1 .: D = ].((p `1) - r),((p `1) + r).[ by A1, A2, Th43; hence W-bound D = (p `1) - r by A4, SPRECT_1:43; ::_thesis: verum end; theorem :: TOPREAL6:46 for p being Point of (TOP-REAL 2) for e being Point of (Euclid 2) for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) & p = e holds E-bound D = (p `1) + r proof let p be Point of (TOP-REAL 2); ::_thesis: for e being Point of (Euclid 2) for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) & p = e holds E-bound D = (p `1) + r let e be Point of (Euclid 2); ::_thesis: for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) & p = e holds E-bound D = (p `1) + r let D be non empty Subset of (TOP-REAL 2); ::_thesis: for r being real number st D = Ball (e,r) & p = e holds E-bound D = (p `1) + r let r be real number ; ::_thesis: ( D = Ball (e,r) & p = e implies E-bound D = (p `1) + r ) assume that A1: D = Ball (e,r) and A2: p = e ; ::_thesis: E-bound D = (p `1) + r r > 0 by A1, TBSP_1:12; then A3: (p `1) + 0 < (p `1) + r by XREAL_1:6; (p `1) - r < (p `1) - 0 by A1, TBSP_1:12, XREAL_1:15; then (p `1) - r < (p `1) + r by A3, XXREAL_0:2; then A4: upper_bound ].((p `1) - r),((p `1) + r).[ = (p `1) + r by Th17; proj1 .: D = ].((p `1) - r),((p `1) + r).[ by A1, A2, Th43; hence E-bound D = (p `1) + r by A4, SPRECT_1:46; ::_thesis: verum end; theorem :: TOPREAL6:47 for p being Point of (TOP-REAL 2) for e being Point of (Euclid 2) for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) & p = e holds S-bound D = (p `2) - r proof let p be Point of (TOP-REAL 2); ::_thesis: for e being Point of (Euclid 2) for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) & p = e holds S-bound D = (p `2) - r let e be Point of (Euclid 2); ::_thesis: for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) & p = e holds S-bound D = (p `2) - r let D be non empty Subset of (TOP-REAL 2); ::_thesis: for r being real number st D = Ball (e,r) & p = e holds S-bound D = (p `2) - r let r be real number ; ::_thesis: ( D = Ball (e,r) & p = e implies S-bound D = (p `2) - r ) assume that A1: D = Ball (e,r) and A2: p = e ; ::_thesis: S-bound D = (p `2) - r r > 0 by A1, TBSP_1:12; then A3: (p `2) + 0 < (p `2) + r by XREAL_1:6; (p `2) - r < (p `2) - 0 by A1, TBSP_1:12, XREAL_1:15; then (p `2) - r < (p `2) + r by A3, XXREAL_0:2; then A4: lower_bound ].((p `2) - r),((p `2) + r).[ = (p `2) - r by Th17; proj2 .: D = ].((p `2) - r),((p `2) + r).[ by A1, A2, Th44; hence S-bound D = (p `2) - r by A4, SPRECT_1:44; ::_thesis: verum end; theorem :: TOPREAL6:48 for p being Point of (TOP-REAL 2) for e being Point of (Euclid 2) for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) & p = e holds N-bound D = (p `2) + r proof let p be Point of (TOP-REAL 2); ::_thesis: for e being Point of (Euclid 2) for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) & p = e holds N-bound D = (p `2) + r let e be Point of (Euclid 2); ::_thesis: for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) & p = e holds N-bound D = (p `2) + r let D be non empty Subset of (TOP-REAL 2); ::_thesis: for r being real number st D = Ball (e,r) & p = e holds N-bound D = (p `2) + r let r be real number ; ::_thesis: ( D = Ball (e,r) & p = e implies N-bound D = (p `2) + r ) assume that A1: D = Ball (e,r) and A2: p = e ; ::_thesis: N-bound D = (p `2) + r r > 0 by A1, TBSP_1:12; then A3: (p `2) + 0 < (p `2) + r by XREAL_1:6; (p `2) - r < (p `2) - 0 by A1, TBSP_1:12, XREAL_1:15; then (p `2) - r < (p `2) + r by A3, XXREAL_0:2; then A4: upper_bound ].((p `2) - r),((p `2) + r).[ = (p `2) + r by Th17; proj2 .: D = ].((p `2) - r),((p `2) + r).[ by A1, A2, Th44; hence N-bound D = (p `2) + r by A4, SPRECT_1:45; ::_thesis: verum end; theorem :: TOPREAL6:49 for e being Point of (Euclid 2) for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) holds not D is horizontal proof let e be Point of (Euclid 2); ::_thesis: for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) holds not D is horizontal let D be non empty Subset of (TOP-REAL 2); ::_thesis: for r being real number st D = Ball (e,r) holds not D is horizontal let r be real number ; ::_thesis: ( D = Ball (e,r) implies not D is horizontal ) reconsider p = e as Point of (TOP-REAL 2) by TOPREAL3:8; assume A1: D = Ball (e,r) ; ::_thesis: not D is horizontal then A2: r > 0 by TBSP_1:12; take p ; :: according to SPPOL_1:def_2 ::_thesis: ex b1 being Element of the carrier of (TOP-REAL 2) st ( p in D & b1 in D & not p `2 = b1 `2 ) take q = |[(p `1),((p `2) - (r / 2))]|; ::_thesis: ( p in D & q in D & not p `2 = q `2 ) thus p in D by A1, TBSP_1:11, TBSP_1:12; ::_thesis: ( q in D & not p `2 = q `2 ) reconsider f = q as Point of (Euclid 2) by TOPREAL3:8; dist (e,f) = (Pitag_dist 2) . (e,f) by METRIC_1:def_1 .= sqrt ((((p `1) - (q `1)) ^2) + (((p `2) - (q `2)) ^2)) by TOPREAL3:7 .= sqrt ((((p `1) - (p `1)) ^2) + (((p `2) - (q `2)) ^2)) by EUCLID:52 .= sqrt (0 + (((p `2) - ((p `2) - (r / 2))) ^2)) by EUCLID:52 .= r / 2 by A2, SQUARE_1:22 ; then dist (e,f) < r by A1, TBSP_1:12, XREAL_1:216; hence q in D by A1, METRIC_1:11; ::_thesis: not p `2 = q `2 r / 2 > 0 by A2, XREAL_1:139; then (p `2) - (r / 2) < (p `2) - 0 by XREAL_1:15; hence not p `2 = q `2 by EUCLID:52; ::_thesis: verum end; theorem :: TOPREAL6:50 for e being Point of (Euclid 2) for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) holds not D is vertical proof let e be Point of (Euclid 2); ::_thesis: for D being non empty Subset of (TOP-REAL 2) for r being real number st D = Ball (e,r) holds not D is vertical let D be non empty Subset of (TOP-REAL 2); ::_thesis: for r being real number st D = Ball (e,r) holds not D is vertical let r be real number ; ::_thesis: ( D = Ball (e,r) implies not D is vertical ) reconsider p = e as Point of (TOP-REAL 2) by TOPREAL3:8; assume A1: D = Ball (e,r) ; ::_thesis: not D is vertical then A2: r > 0 by TBSP_1:12; take p ; :: according to SPPOL_1:def_3 ::_thesis: ex b1 being Element of the carrier of (TOP-REAL 2) st ( p in D & b1 in D & not p `1 = b1 `1 ) take q = |[((p `1) - (r / 2)),(p `2)]|; ::_thesis: ( p in D & q in D & not p `1 = q `1 ) thus p in D by A1, TBSP_1:11, TBSP_1:12; ::_thesis: ( q in D & not p `1 = q `1 ) reconsider f = q as Point of (Euclid 2) by TOPREAL3:8; dist (e,f) = (Pitag_dist 2) . (e,f) by METRIC_1:def_1 .= sqrt ((((p `1) - (q `1)) ^2) + (((p `2) - (q `2)) ^2)) by TOPREAL3:7 .= sqrt ((((p `1) - ((p `1) - (r / 2))) ^2) + (((p `2) - (q `2)) ^2)) by EUCLID:52 .= sqrt ((((p `1) - ((p `1) - (r / 2))) ^2) + (((p `2) - (p `2)) ^2)) by EUCLID:52 .= r / 2 by A2, SQUARE_1:22 ; then dist (e,f) < r by A1, TBSP_1:12, XREAL_1:216; hence q in D by A1, METRIC_1:11; ::_thesis: not p `1 = q `1 r / 2 > 0 by A2, XREAL_1:139; then (p `1) - (r / 2) < (p `1) - 0 by XREAL_1:15; hence not p `1 = q `1 by EUCLID:52; ::_thesis: verum end; theorem :: TOPREAL6:51 for a being Real for f being Point of (Euclid 2) for 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 a be Real; ::_thesis: for f being Point of (Euclid 2) for 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) let f be Point of (Euclid 2); ::_thesis: for 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) let x be Point of (TOP-REAL 2); ::_thesis: ( x in Ball (f,a) implies not |[((x `1) - (2 * a)),(x `2)]| in Ball (f,a) ) assume A1: x in Ball (f,a) ; ::_thesis: not |[((x `1) - (2 * a)),(x `2)]| in Ball (f,a) A2: a > 0 by A1, TBSP_1:12; set p = |[((x `1) - (2 * a)),(x `2)]|; reconsider z = |[((x `1) - (2 * a)),(x `2)]|, X = x as Point of (Euclid 2) by TOPREAL3:8; A3: dist (X,z) = (Pitag_dist 2) . (X,z) by METRIC_1:def_1 .= sqrt ((((x `1) - (|[((x `1) - (2 * a)),(x `2)]| `1)) ^2) + (((x `2) - (|[((x `1) - (2 * a)),(x `2)]| `2)) ^2)) by TOPREAL3:7 .= sqrt ((((x `1) - ((x `1) - (2 * a))) ^2) + (((x `2) - (|[((x `1) - (2 * a)),(x `2)]| `2)) ^2)) by EUCLID:52 .= sqrt ((((0 ^2) + ((2 * ((x `1) - (x `1))) * (2 * a))) + ((2 * a) ^2)) + (((x `2) - (x `2)) ^2)) by EUCLID:52 .= 2 * a by A2, SQUARE_1:22 ; assume |[((x `1) - (2 * a)),(x `2)]| in Ball (f,a) ; ::_thesis: contradiction then A4: dist (f,z) < a by METRIC_1:11; dist (f,X) < a by A1, METRIC_1:11; then (dist (f,X)) + (dist (f,z)) < a + a by A4, XREAL_1:8; hence contradiction by A3, METRIC_1:4; ::_thesis: verum end; theorem :: TOPREAL6:52 for a being Real for X being non empty compact Subset of (TOP-REAL 2) for p being Point of (Euclid 2) st p = 0. (TOP-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 a be Real; ::_thesis: for X being non empty compact Subset of (TOP-REAL 2) for p being Point of (Euclid 2) st p = 0. (TOP-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)) let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: for p being Point of (Euclid 2) st p = 0. (TOP-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)) let p be Point of (Euclid 2); ::_thesis: ( p = 0. (TOP-REAL 2) & a > 0 implies X c= Ball (p,(((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a)) ) assume that A1: p = 0. (TOP-REAL 2) and A2: a > 0 ; ::_thesis: X c= Ball (p,(((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a)) set A = X; set n = N-bound X; set s = S-bound X; set e = E-bound X; set w = W-bound X; set r = ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a; A3: ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + 0 < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A2, XREAL_1:8; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Ball (p,(((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a)) ) assume A4: x in X ; ::_thesis: x in Ball (p,(((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a)) then reconsider b = x as Point of (Euclid 2) by TOPREAL3:8; reconsider P = p, B = b as Point of (TOP-REAL 2) by TOPREAL3:8; A5: P `1 = 0 by A1, Th24; A6: B `1 <= E-bound X by A4, PSCOMP_1:24; A7: B `2 <= N-bound X by A4, PSCOMP_1:24; A8: S-bound X <= B `2 by A4, PSCOMP_1:24; A9: P `2 = 0 by A1, Th24; A10: dist (p,b) = (Pitag_dist 2) . (p,b) by METRIC_1:def_1 .= sqrt ((((P `1) - (B `1)) ^2) + (((P `2) - (B `2)) ^2)) by TOPREAL3:7 .= sqrt (((B `1) ^2) + ((B `2) ^2)) by A5, A9 ; A11: 0 <= (B `2) ^2 by XREAL_1:63; 0 <= (B `1) ^2 by XREAL_1:63; then sqrt (((B `1) ^2) + ((B `2) ^2)) <= (sqrt ((B `1) ^2)) + (sqrt ((B `2) ^2)) by A11, Th1; then sqrt (((B `1) ^2) + ((B `2) ^2)) <= (abs (B `1)) + (sqrt ((B `2) ^2)) by COMPLEX1:72; then A12: sqrt (((B `1) ^2) + ((B `2) ^2)) <= (abs (B `1)) + (abs (B `2)) by COMPLEX1:72; A13: 0 <= abs (N-bound X) by COMPLEX1:46; A14: 0 <= abs (E-bound X) by COMPLEX1:46; A15: 0 <= abs (W-bound X) by COMPLEX1:46; A16: 0 <= abs (S-bound X) by COMPLEX1:46; A17: W-bound X <= B `1 by A4, PSCOMP_1:24; now__::_thesis:_(_(_B_`1_>=_0_&_B_`2_>=_0_&_dist_(p,b)_<_((((abs_(E-bound_X))_+_(abs_(N-bound_X)))_+_(abs_(W-bound_X)))_+_(abs_(S-bound_X)))_+_a_)_or_(_B_`1_<_0_&_B_`2_>=_0_&_dist_(p,b)_<_((((abs_(E-bound_X))_+_(abs_(N-bound_X)))_+_(abs_(W-bound_X)))_+_(abs_(S-bound_X)))_+_a_)_or_(_B_`1_>=_0_&_B_`2_<_0_&_dist_(p,b)_<_((((abs_(E-bound_X))_+_(abs_(N-bound_X)))_+_(abs_(W-bound_X)))_+_(abs_(S-bound_X)))_+_a_)_or_(_B_`1_<_0_&_B_`2_<_0_&_dist_(p,b)_<_((((abs_(E-bound_X))_+_(abs_(N-bound_X)))_+_(abs_(W-bound_X)))_+_(abs_(S-bound_X)))_+_a_)_) percases ( ( B `1 >= 0 & B `2 >= 0 ) or ( B `1 < 0 & B `2 >= 0 ) or ( B `1 >= 0 & B `2 < 0 ) or ( B `1 < 0 & B `2 < 0 ) ) ; caseA18: ( B `1 >= 0 & B `2 >= 0 ) ; ::_thesis: dist (p,b) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a ((abs (E-bound X)) + (abs (N-bound X))) + 0 <= ((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X)) by A15, XREAL_1:7; then (abs (E-bound X)) + (abs (N-bound X)) <= (((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X)) by A16, XREAL_1:7; then A19: (abs (E-bound X)) + (abs (N-bound X)) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A3, XXREAL_0:2; A20: abs (B `2) <= abs (N-bound X) by A7, A18, Th2; abs (B `1) <= abs (E-bound X) by A6, A18, Th2; then (abs (B `1)) + (abs (B `2)) <= (abs (E-bound X)) + (abs (N-bound X)) by A20, XREAL_1:7; then dist (p,b) <= (abs (E-bound X)) + (abs (N-bound X)) by A10, A12, XXREAL_0:2; hence dist (p,b) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A19, XXREAL_0:2; ::_thesis: verum end; caseA21: ( B `1 < 0 & B `2 >= 0 ) ; ::_thesis: dist (p,b) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a 0 + ((abs (N-bound X)) + (abs (W-bound X))) <= (abs (E-bound X)) + ((abs (N-bound X)) + (abs (W-bound X))) by A14, XREAL_1:7; then (abs (W-bound X)) + (abs (N-bound X)) <= (((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X)) by A16, XREAL_1:7; then A22: (abs (W-bound X)) + (abs (N-bound X)) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A3, XXREAL_0:2; A23: abs (B `2) <= abs (N-bound X) by A7, A21, Th2; abs (B `1) <= abs (W-bound X) by A17, A21, Th3; then (abs (B `1)) + (abs (B `2)) <= (abs (W-bound X)) + (abs (N-bound X)) by A23, XREAL_1:7; then dist (p,b) <= (abs (W-bound X)) + (abs (N-bound X)) by A10, A12, XXREAL_0:2; hence dist (p,b) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A22, XXREAL_0:2; ::_thesis: verum end; caseA24: ( B `1 >= 0 & B `2 < 0 ) ; ::_thesis: dist (p,b) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a A25: (((abs (E-bound X)) + (abs (N-bound X))) + (abs (S-bound X))) + 0 <= (((abs (E-bound X)) + (abs (N-bound X))) + (abs (S-bound X))) + (abs (W-bound X)) by A15, XREAL_1:7; ((abs (E-bound X)) + (abs (S-bound X))) + 0 <= ((abs (E-bound X)) + (abs (S-bound X))) + (abs (N-bound X)) by A13, XREAL_1:7; then (abs (E-bound X)) + (abs (S-bound X)) <= (((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X)) by A25, XXREAL_0:2; then A26: (abs (E-bound X)) + (abs (S-bound X)) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A3, XXREAL_0:2; A27: abs (B `2) <= abs (S-bound X) by A8, A24, Th3; abs (B `1) <= abs (E-bound X) by A6, A24, Th2; then (abs (B `1)) + (abs (B `2)) <= (abs (E-bound X)) + (abs (S-bound X)) by A27, XREAL_1:7; then dist (p,b) <= (abs (E-bound X)) + (abs (S-bound X)) by A10, A12, XXREAL_0:2; hence dist (p,b) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A26, XXREAL_0:2; ::_thesis: verum end; caseA28: ( B `1 < 0 & B `2 < 0 ) ; ::_thesis: dist (p,b) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a then A29: abs (B `2) <= abs (S-bound X) by A8, Th3; abs (B `1) <= abs (W-bound X) by A17, A28, Th3; then (abs (B `1)) + (abs (B `2)) <= (abs (W-bound X)) + (abs (S-bound X)) by A29, XREAL_1:7; then A30: dist (p,b) <= (abs (W-bound X)) + (abs (S-bound X)) by A10, A12, XXREAL_0:2; 0 + ((abs (W-bound X)) + (abs (S-bound X))) <= ((abs (E-bound X)) + (abs (N-bound X))) + ((abs (W-bound X)) + (abs (S-bound X))) by A14, A13, XREAL_1:7; then (abs (W-bound X)) + (abs (S-bound X)) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A2, XREAL_1:8; hence dist (p,b) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A30, XXREAL_0:2; ::_thesis: verum end; end; end; hence x in Ball (p,(((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a)) by METRIC_1:11; ::_thesis: verum end; theorem Th53: :: TOPREAL6:53 for r being real number for M being non empty Reflexive symmetric triangle MetrStruct for z being Point of M st r < 0 holds Sphere (z,r) = {} proof let r be real number ; ::_thesis: for M being non empty Reflexive symmetric triangle MetrStruct for z being Point of M st r < 0 holds Sphere (z,r) = {} let M be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for z being Point of M st r < 0 holds Sphere (z,r) = {} let z be Point of M; ::_thesis: ( r < 0 implies Sphere (z,r) = {} ) assume A1: r < 0 ; ::_thesis: Sphere (z,r) = {} thus Sphere (z,r) c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= Sphere (z,r) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Sphere (z,r) or a in {} ) assume A2: a in Sphere (z,r) ; ::_thesis: a in {} then reconsider b = a as Point of M ; dist (b,z) = r by A2, METRIC_1:13; hence a in {} by A1, METRIC_1:5; ::_thesis: verum end; thus {} c= Sphere (z,r) by XBOOLE_1:2; ::_thesis: verum end; theorem :: TOPREAL6:54 for M being non empty Reflexive discerning MetrStruct for z being Point of M holds Sphere (z,0) = {z} proof let M be non empty Reflexive discerning MetrStruct ; ::_thesis: for z being Point of M holds Sphere (z,0) = {z} let z be Point of M; ::_thesis: Sphere (z,0) = {z} thus Sphere (z,0) c= {z} :: according to XBOOLE_0:def_10 ::_thesis: {z} c= Sphere (z,0) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Sphere (z,0) or a in {z} ) assume A1: a in Sphere (z,0) ; ::_thesis: a in {z} then reconsider b = a as Point of M ; dist (z,b) = 0 by A1, METRIC_1:13; then b = z by METRIC_1:2; hence a in {z} by TARSKI:def_1; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {z} or a in Sphere (z,0) ) assume a in {z} ; ::_thesis: a in Sphere (z,0) then A2: a = z by TARSKI:def_1; dist (z,z) = 0 by METRIC_1:1; hence a in Sphere (z,0) by A2, METRIC_1:13; ::_thesis: verum end; theorem :: TOPREAL6:55 for r being real number for M being non empty Reflexive symmetric triangle MetrStruct for z being Point of M st r < 0 holds cl_Ball (z,r) = {} proof let r be real number ; ::_thesis: for M being non empty Reflexive symmetric triangle MetrStruct for z being Point of M st r < 0 holds cl_Ball (z,r) = {} let M be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for z being Point of M st r < 0 holds cl_Ball (z,r) = {} let z be Point of M; ::_thesis: ( r < 0 implies cl_Ball (z,r) = {} ) A1: (Sphere (z,r)) \/ (Ball (z,r)) = cl_Ball (z,r) by METRIC_1:16; assume A2: r < 0 ; ::_thesis: cl_Ball (z,r) = {} then Ball (z,r) = {} by TBSP_1:12; hence cl_Ball (z,r) = {} by A2, A1, Th53; ::_thesis: verum end; theorem :: TOPREAL6:56 for M being non empty MetrSpace for z being Point of M holds cl_Ball (z,0) = {z} proof let M be non empty MetrSpace; ::_thesis: for z being Point of M holds cl_Ball (z,0) = {z} let z be Point of M; ::_thesis: cl_Ball (z,0) = {z} thus cl_Ball (z,0) c= {z} :: according to XBOOLE_0:def_10 ::_thesis: {z} c= cl_Ball (z,0) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in cl_Ball (z,0) or a in {z} ) assume A1: a in cl_Ball (z,0) ; ::_thesis: a in {z} then reconsider b = a as Point of M ; dist (b,z) <= 0 by A1, METRIC_1:12; then dist (b,z) = 0 by METRIC_1:5; then b = z by METRIC_1:2; hence a in {z} by TARSKI:def_1; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {z} or a in cl_Ball (z,0) ) assume a in {z} ; ::_thesis: a in cl_Ball (z,0) then A2: a = z by TARSKI:def_1; dist (z,z) = 0 by METRIC_1:1; hence a in cl_Ball (z,0) by A2, METRIC_1:12; ::_thesis: verum end; Lm1: for M being non empty MetrSpace for z being Point of M for r being real number for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds A ` is open proof let M be non empty MetrSpace; ::_thesis: for z being Point of M for r being real number for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds A ` is open let z be Point of M; ::_thesis: for r being real number for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds A ` is open let r be real number ; ::_thesis: for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds A ` is open let A be Subset of (TopSpaceMetr M); ::_thesis: ( A = cl_Ball (z,r) implies A ` is open ) assume A1: A = cl_Ball (z,r) ; ::_thesis: A ` is open 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 ; ::_thesis: ( x in A ` iff ex Q being Subset of (TopSpaceMetr M) st ( Q is open & Q c= A ` & x in Q ) ) thus ( x in A ` implies ex Q being Subset of (TopSpaceMetr M) st ( Q is open & Q c= A ` & x in Q ) ) ::_thesis: ( ex Q being Subset of (TopSpaceMetr M) st ( Q is open & Q c= A ` & x in Q ) implies x in A ` ) proof assume A2: x in A ` ; ::_thesis: ex Q being Subset of (TopSpaceMetr M) st ( Q is open & Q c= A ` & x in Q ) then reconsider e = x as Point of M by TOPMETR:12; reconsider Q = Ball (e,((dist (e,z)) - r)) as Subset of (TopSpaceMetr M) by TOPMETR:12; take Q ; ::_thesis: ( Q is open & Q c= A ` & x in Q ) thus Q is open by TOPMETR:14; ::_thesis: ( Q c= A ` & x in Q ) thus Q c= A ` ::_thesis: x in Q proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Q or q in A ` ) assume A3: q in Q ; ::_thesis: q in A ` then reconsider f = q as Point of M ; dist (e,z) <= (dist (e,f)) + (dist (f,z)) by METRIC_1:4; then A4: (dist (e,z)) - r <= ((dist (e,f)) + (dist (f,z))) - r by XREAL_1:9; dist (e,f) < (dist (e,z)) - r by A3, METRIC_1:11; then dist (e,f) < ((dist (e,f)) + (dist (f,z))) - r by A4, XXREAL_0:2; then (dist (e,f)) - (dist (e,f)) < (((dist (e,f)) + (dist (f,z))) - r) - (dist (e,f)) by XREAL_1:9; then 0 < (((dist (e,f)) - (dist (e,f))) + (dist (f,z))) - r ; then dist (f,z) > r by XREAL_1:47; then not q in A by A1, METRIC_1:12; hence q in A ` by A3, SUBSET_1:29; ::_thesis: verum end; not x in A by A2, XBOOLE_0:def_5; then dist (z,e) > r by A1, METRIC_1:12; then (dist (e,z)) - r > r - r by XREAL_1:9; hence x in Q by TBSP_1:11; ::_thesis: verum end; thus ( ex Q being Subset of (TopSpaceMetr M) st ( Q is open & Q c= A ` & x in Q ) implies x in A ` ) ; ::_thesis: verum end; hence A ` is open by TOPS_1:25; ::_thesis: verum end; theorem Th57: :: TOPREAL6:57 for M being non empty MetrSpace for z being Point of M for r being real number for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds A is closed proof let M be non empty MetrSpace; ::_thesis: for z being Point of M for r being real number for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds A is closed let z be Point of M; ::_thesis: for r being real number for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds A is closed let r be real number ; ::_thesis: for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds A is closed let A be Subset of (TopSpaceMetr M); ::_thesis: ( A = cl_Ball (z,r) implies A is closed ) assume A = cl_Ball (z,r) ; ::_thesis: A is closed then A ` is open by Lm1; hence A is closed by TOPS_1:3; ::_thesis: verum end; theorem :: TOPREAL6:58 for n being Element of NAT for w being Point of (Euclid n) for A being Subset of (TOP-REAL n) for r being real number st A = cl_Ball (w,r) holds A is closed proof let n be Element of NAT ; ::_thesis: for w being Point of (Euclid n) for A being Subset of (TOP-REAL n) for r being real number st A = cl_Ball (w,r) holds A is closed let w be Point of (Euclid n); ::_thesis: for A being Subset of (TOP-REAL n) for r being real number st A = cl_Ball (w,r) holds A is closed let A be Subset of (TOP-REAL n); ::_thesis: for r being real number st A = cl_Ball (w,r) holds A is closed let r be real number ; ::_thesis: ( A = cl_Ball (w,r) implies A is closed ) A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; then reconsider E = A as Subset of (TopSpaceMetr (Euclid n)) ; assume A = cl_Ball (w,r) ; ::_thesis: A is closed then E is closed by Th57; hence A is closed by A1, PRE_TOPC:31; ::_thesis: verum end; theorem Th59: :: TOPREAL6:59 for r being real number for M being non empty Reflexive symmetric triangle MetrStruct for x being Element of M holds cl_Ball (x,r) is bounded proof let r be real number ; ::_thesis: for M being non empty Reflexive symmetric triangle MetrStruct for x being Element of M holds cl_Ball (x,r) is bounded let M be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for x being Element of M holds cl_Ball (x,r) is bounded let x be Element of M; ::_thesis: cl_Ball (x,r) is bounded cl_Ball (x,r) c= Ball (x,(r + 1)) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in cl_Ball (x,r) or y in Ball (x,(r + 1)) ) assume A1: y in cl_Ball (x,r) ; ::_thesis: y in Ball (x,(r + 1)) reconsider Y = y as Point of M by A1; A2: r + 0 < r + 1 by XREAL_1:8; dist (x,Y) <= r by A1, METRIC_1:12; then dist (x,Y) < r + 1 by A2, XXREAL_0:2; hence y in Ball (x,(r + 1)) by METRIC_1:11; ::_thesis: verum end; hence cl_Ball (x,r) is bounded by TBSP_1:14; ::_thesis: verum end; theorem Th60: :: TOPREAL6:60 for M being non empty MetrSpace for z being Point of M for r being real number for A being Subset of (TopSpaceMetr M) st A = Sphere (z,r) holds A is closed proof let M be non empty MetrSpace; ::_thesis: for z being Point of M for r being real number for A being Subset of (TopSpaceMetr M) st A = Sphere (z,r) holds A is closed let z be Point of M; ::_thesis: for r being real number for A being Subset of (TopSpaceMetr M) st A = Sphere (z,r) holds A is closed let r be real number ; ::_thesis: for A being Subset of (TopSpaceMetr M) st A = Sphere (z,r) holds A is closed let A be Subset of (TopSpaceMetr M); ::_thesis: ( A = Sphere (z,r) implies A is closed ) assume A1: A = Sphere (z,r) ; ::_thesis: A is closed reconsider B = cl_Ball (z,r), C = Ball (z,r) as Subset of (TopSpaceMetr M) by TOPMETR:12; A2: (cl_Ball (z,r)) ` = B ` by TOPMETR:12; A3: A ` = (B `) \/ C proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (B `) \/ C c= A ` let a be set ; ::_thesis: ( a in A ` implies a in (B `) \/ C ) assume A4: a in A ` ; ::_thesis: a in (B `) \/ C then reconsider e = a as Point of M by TOPMETR:12; not a in A by A4, XBOOLE_0:def_5; then dist (e,z) <> r by A1, METRIC_1:13; then ( dist (e,z) < r or dist (e,z) > r ) by XXREAL_0:1; then ( e in Ball (z,r) or not e in cl_Ball (z,r) ) by METRIC_1:11, METRIC_1:12; then ( e in Ball (z,r) or e in (cl_Ball (z,r)) ` ) by SUBSET_1:29; hence a in (B `) \/ C by A2, XBOOLE_0:def_3; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (B `) \/ C or a in A ` ) assume A5: a in (B `) \/ C ; ::_thesis: a in A ` then reconsider e = a as Point of M by TOPMETR:12; ( a in B ` or a in C ) by A5, XBOOLE_0:def_3; then ( not e in cl_Ball (z,r) or e in C ) by XBOOLE_0:def_5; then ( dist (e,z) > r or dist (e,z) < r ) by METRIC_1:11, METRIC_1:12; then not a in A by A1, METRIC_1:13; hence a in A ` by A5, SUBSET_1:29; ::_thesis: verum end; A6: C is open by TOPMETR:14; B ` is open by Lm1; hence A is closed by A3, A6, TOPS_1:3; ::_thesis: verum end; theorem :: TOPREAL6:61 for n being Element of NAT for w being Point of (Euclid n) for A being Subset of (TOP-REAL n) for r being real number st A = Sphere (w,r) holds A is closed proof let n be Element of NAT ; ::_thesis: for w being Point of (Euclid n) for A being Subset of (TOP-REAL n) for r being real number st A = Sphere (w,r) holds A is closed let w be Point of (Euclid n); ::_thesis: for A being Subset of (TOP-REAL n) for r being real number st A = Sphere (w,r) holds A is closed let A be Subset of (TOP-REAL n); ::_thesis: for r being real number st A = Sphere (w,r) holds A is closed let r be real number ; ::_thesis: ( A = Sphere (w,r) implies A is closed ) A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; then reconsider E = A as Subset of (TopSpaceMetr (Euclid n)) ; assume A = Sphere (w,r) ; ::_thesis: A is closed then E is closed by Th60; hence A is closed by A1, PRE_TOPC:31; ::_thesis: verum end; theorem :: TOPREAL6:62 for M being non empty MetrSpace for z being Point of M for r being real number holds Sphere (z,r) is bounded proof let M be non empty MetrSpace; ::_thesis: for z being Point of M for r being real number holds Sphere (z,r) is bounded let z be Point of M; ::_thesis: for r being real number holds Sphere (z,r) is bounded let r be real number ; ::_thesis: Sphere (z,r) is bounded Sphere (z,r) c= cl_Ball (z,r) by METRIC_1:15; hence Sphere (z,r) is bounded by Th59, TBSP_1:14; ::_thesis: verum end; theorem :: TOPREAL6:63 for n being Element of NAT for A being Subset of (TOP-REAL n) st A is bounded holds Cl A is bounded ; theorem :: TOPREAL6:64 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 ; ::_thesis: ( M is bounded iff for X being Subset of M holds X is bounded ) hereby ::_thesis: ( ( for X being Subset of M holds X is bounded ) implies M is bounded ) assume A1: M is bounded ; ::_thesis: for X being Subset of M holds X is bounded let X be Subset of M; ::_thesis: X is bounded [#] M is bounded by A1; hence X is bounded by TBSP_1:14; ::_thesis: verum end; assume for X being Subset of M holds X is bounded ; ::_thesis: M is bounded then [#] M is bounded ; hence M is bounded by TBSP_1:18; ::_thesis: verum end; theorem Th65: :: TOPREAL6:65 for M being non empty Reflexive symmetric triangle MetrStruct for X, Y being Subset of M st the carrier of M = X \/ Y & not M is bounded & X is bounded holds not Y is bounded proof let M be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for X, Y being Subset of M st the carrier of M = X \/ Y & not M is bounded & X is bounded holds not Y is bounded let X, Y be Subset of M; ::_thesis: ( the carrier of M = X \/ Y & not M is bounded & X is bounded implies not Y is bounded ) assume that A1: the carrier of M = X \/ Y and A2: not M is bounded ; ::_thesis: ( not X is bounded or not Y is bounded ) assume that A3: X is bounded and A4: Y is bounded ; ::_thesis: contradiction [#] M is bounded by A1, A3, A4, TBSP_1:13; hence contradiction by A2, TBSP_1:18; ::_thesis: verum end; theorem :: TOPREAL6:66 for n being Element of NAT for X, Y being Subset of (TOP-REAL n) st n >= 1 & the carrier of (TOP-REAL n) = X \/ Y & X is bounded holds not Y is bounded proof let n be Element of NAT ; ::_thesis: for X, Y being Subset of (TOP-REAL n) st n >= 1 & the carrier of (TOP-REAL n) = X \/ Y & X is bounded holds not Y is bounded set M = TOP-REAL n; let X, Y be Subset of (TOP-REAL n); ::_thesis: ( n >= 1 & the carrier of (TOP-REAL n) = X \/ Y & X is bounded implies not Y is bounded ) assume that A1: n >= 1 and A2: the carrier of (TOP-REAL n) = X \/ Y ; ::_thesis: ( not X is bounded or not Y is bounded ) reconsider E = [#] (TOP-REAL n) as Subset of (Euclid n) by TOPREAL3:8; not [#] (TOP-REAL n) is bounded by A1, JORDAN2C:35; then A3: not E is bounded by JORDAN2C:11; reconsider D = Y as Subset of (Euclid n) by TOPREAL3:8; assume X is bounded ; ::_thesis: not Y is bounded then reconsider C = X as bounded Subset of (Euclid n) by JORDAN2C:11; A4: the carrier of (Euclid n) = C \/ D by A2, TOPREAL3:8; E = [#] (Euclid n) by TOPREAL3:8; then not Euclid n is bounded by A3; then not D is bounded by A4, Th65; hence not Y is bounded by JORDAN2C:11; ::_thesis: verum end; theorem Th67: :: TOPREAL6:67 for n being Element of NAT for A, B being Subset of (TOP-REAL n) st A is bounded & B is bounded holds A \/ B is bounded proof let n be Element of NAT ; ::_thesis: for A, B being Subset of (TOP-REAL n) st A is bounded & B is bounded holds A \/ B is bounded let A, B be Subset of (TOP-REAL n); ::_thesis: ( A is bounded & B is bounded implies A \/ B is bounded ) assume A is bounded ; ::_thesis: ( not B is bounded or A \/ B is bounded ) then A1: A is bounded Subset of (Euclid n) by JORDAN2C:11; then reconsider A = A as Subset of (Euclid n) ; assume B is bounded ; ::_thesis: A \/ B is bounded then A2: B is bounded Subset of (Euclid n) by JORDAN2C:11; then reconsider B = B as Subset of (Euclid n) ; reconsider E = A \/ B as Subset of (Euclid n) ; E is bounded Subset of (Euclid n) by A1, A2, TBSP_1:13; hence A \/ B is bounded by JORDAN2C:11; ::_thesis: verum end; begin registration let X be non empty Subset of REAL; cluster Cl X -> non empty ; coherence not Cl X is empty by MEASURE6:58, XBOOLE_1:3; end; registration let D be bounded_below Subset of REAL; cluster Cl D -> bounded_below ; coherence Cl D is bounded_below proof consider p being real number such that A1: p is LowerBound of D by XXREAL_2:def_9; A2: for r being real number st r in D holds p <= r by A1, XXREAL_2:def_2; take p ; :: according to XXREAL_2:def_9 ::_thesis: p is LowerBound of Cl D let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in Cl D or p <= r ) assume r in Cl D ; ::_thesis: p <= r then consider s being Real_Sequence such that A3: rng s c= D and A4: s is convergent and A5: lim s = r by MEASURE6:64; for n being Element of NAT holds s . n >= p proof let n be Element of NAT ; ::_thesis: s . n >= p dom s = NAT by FUNCT_2:def_1; then s . n in rng s by FUNCT_1:def_3; hence s . n >= p by A2, A3; ::_thesis: verum end; hence p <= r by A4, A5, PREPOWER:1; ::_thesis: verum end; end; registration let D be bounded_above Subset of REAL; cluster Cl D -> bounded_above ; coherence Cl D is bounded_above proof consider p being real number such that A1: p is UpperBound of D by XXREAL_2:def_10; A2: for r being real number st r in D holds r <= p by A1, XXREAL_2:def_1; take p ; :: according to XXREAL_2:def_10 ::_thesis: p is UpperBound of Cl D let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in Cl D or r <= p ) assume r in Cl D ; ::_thesis: r <= p then consider s being Real_Sequence such that A3: rng s c= D and A4: s is convergent and A5: lim s = r by MEASURE6:64; for n being Element of NAT holds s . n <= p proof let n be Element of NAT ; ::_thesis: s . n <= p dom s = NAT by FUNCT_2:def_1; then s . n in rng s by FUNCT_1:def_3; hence s . n <= p by A2, A3; ::_thesis: verum end; hence r <= p by A4, A5, PREPOWER:2; ::_thesis: verum end; end; theorem Th68: :: TOPREAL6:68 for D being non empty bounded_below Subset of REAL holds lower_bound D = lower_bound (Cl D) proof let D be non empty bounded_below Subset of REAL; ::_thesis: lower_bound D = lower_bound (Cl D) A1: for q being real number st ( for p being real number st p in D holds p >= q ) holds lower_bound (Cl D) >= q proof let q be real number ; ::_thesis: ( ( for p being real number st p in D holds p >= q ) implies lower_bound (Cl D) >= q ) assume A2: for p being real number st p in D holds p >= q ; ::_thesis: lower_bound (Cl D) >= q for p being real number st p in Cl D holds p >= q proof let p be real number ; ::_thesis: ( p in Cl D implies p >= q ) assume p in Cl D ; ::_thesis: p >= q then consider s being Real_Sequence such that A3: rng s c= D and A4: s is convergent and A5: lim s = p by MEASURE6:64; for n being Element of NAT holds s . n >= q proof let n be Element of NAT ; ::_thesis: s . n >= q dom s = NAT by FUNCT_2:def_1; then s . n in rng s by FUNCT_1:def_3; hence s . n >= q by A2, A3; ::_thesis: verum end; hence p >= q by A4, A5, PREPOWER:1; ::_thesis: verum end; hence lower_bound (Cl D) >= q by SEQ_4:43; ::_thesis: verum end; A6: lower_bound (Cl D) <= lower_bound D by MEASURE6:58, SEQ_4:47; for p being real number st p in D holds p >= lower_bound (Cl D) proof let p be real number ; ::_thesis: ( p in D implies p >= lower_bound (Cl D) ) assume p in D ; ::_thesis: p >= lower_bound (Cl D) then lower_bound D <= p by SEQ_4:def_2; hence p >= lower_bound (Cl D) by A6, XXREAL_0:2; ::_thesis: verum end; hence lower_bound D = lower_bound (Cl D) by A1, SEQ_4:44; ::_thesis: verum end; theorem Th69: :: TOPREAL6:69 for D being non empty bounded_above Subset of REAL holds upper_bound D = upper_bound (Cl D) proof let D be non empty bounded_above Subset of REAL; ::_thesis: upper_bound D = upper_bound (Cl D) A1: for q being real number st ( for p being real number st p in D holds p <= q ) holds upper_bound (Cl D) <= q proof let q be real number ; ::_thesis: ( ( for p being real number st p in D holds p <= q ) implies upper_bound (Cl D) <= q ) assume A2: for p being real number st p in D holds p <= q ; ::_thesis: upper_bound (Cl D) <= q for p being real number st p in Cl D holds p <= q proof let p be real number ; ::_thesis: ( p in Cl D implies p <= q ) assume p in Cl D ; ::_thesis: p <= q then consider s being Real_Sequence such that A3: rng s c= D and A4: s is convergent and A5: lim s = p by MEASURE6:64; for n being Element of NAT holds s . n <= q proof let n be Element of NAT ; ::_thesis: s . n <= q dom s = NAT by FUNCT_2:def_1; then s . n in rng s by FUNCT_1:def_3; hence s . n <= q by A2, A3; ::_thesis: verum end; hence p <= q by A4, A5, PREPOWER:2; ::_thesis: verum end; hence upper_bound (Cl D) <= q by SEQ_4:45; ::_thesis: verum end; A6: upper_bound (Cl D) >= upper_bound D by MEASURE6:58, SEQ_4:48; for p being real number st p in D holds p <= upper_bound (Cl D) proof let p be real number ; ::_thesis: ( p in D implies p <= upper_bound (Cl D) ) assume p in D ; ::_thesis: p <= upper_bound (Cl D) then upper_bound D >= p by SEQ_4:def_1; hence p <= upper_bound (Cl D) by A6, XXREAL_0:2; ::_thesis: verum end; hence upper_bound D = upper_bound (Cl D) by A1, SEQ_4:46; ::_thesis: verum end; registration cluster R^1 -> T_2 ; coherence R^1 is T_2 by PCOMPS_1:34, TOPMETR:def_6; end; theorem :: TOPREAL6:70 canceled; theorem :: TOPREAL6:71 canceled; theorem :: TOPREAL6:72 canceled; theorem :: TOPREAL6:73 canceled; theorem :: TOPREAL6:74 canceled; theorem Th75: :: TOPREAL6:75 for A, B being Subset of REAL for f being Function 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; ::_thesis: for f being Function 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)) let f be Function of [:R^1,R^1:],(TOP-REAL 2); ::_thesis: ( ( for x, y being Real holds f . [x,y] = <*x,y*> ) implies f .: [:A,B:] = product ((1,2) --> (A,B)) ) assume A1: for x, y being Real holds f . [x,y] = <*x,y*> ; ::_thesis: f .: [:A,B:] = product ((1,2) --> (A,B)) set h = (1,2) --> (A,B); A2: dom ((1,2) --> (A,B)) = {1,2} by FUNCT_4:62; thus f .: [:A,B:] c= product ((1,2) --> (A,B)) :: according to XBOOLE_0:def_10 ::_thesis: product ((1,2) --> (A,B)) c= f .: [:A,B:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: [:A,B:] or x in product ((1,2) --> (A,B)) ) assume x in f .: [:A,B:] ; ::_thesis: x in product ((1,2) --> (A,B)) then consider a being set such that A3: a in the carrier of [:R^1,R^1:] and A4: a in [:A,B:] and A5: f . a = x by FUNCT_2:64; reconsider a = a as Point of [:R^1,R^1:] by A3; consider m, n being set such that A6: m in A and A7: n in B and A8: a = [m,n] by A4, ZFMISC_1:def_2; f . a = x by A5; then reconsider g = x as Function of (Seg 2),REAL by EUCLID:23; reconsider m = m, n = n as Real by A6, A7; A9: for y being set st y in dom ((1,2) --> (A,B)) holds g . y in ((1,2) --> (A,B)) . y proof let y be set ; ::_thesis: ( y in dom ((1,2) --> (A,B)) implies g . y in ((1,2) --> (A,B)) . y ) A10: |[m,n]| `1 = m by EUCLID:52; assume y in dom ((1,2) --> (A,B)) ; ::_thesis: g . y in ((1,2) --> (A,B)) . y then A11: ( y = 1 or y = 2 ) by TARSKI:def_2; A12: |[m,n]| `2 = n by EUCLID:52; f . [m,n] = |[m,n]| by A1; hence g . y in ((1,2) --> (A,B)) . y by A5, A6, A7, A8, A11, A10, A12, FUNCT_4:63; ::_thesis: verum end; dom g = dom ((1,2) --> (A,B)) by A2, FINSEQ_1:2, FUNCT_2:def_1; hence x in product ((1,2) --> (A,B)) by A9, CARD_3:9; ::_thesis: verum end; A13: ((1,2) --> (A,B)) . 2 = B by FUNCT_4:63; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in product ((1,2) --> (A,B)) or a in f .: [:A,B:] ) assume a in product ((1,2) --> (A,B)) ; ::_thesis: a in f .: [:A,B:] then consider g being Function such that A14: a = g and A15: dom g = dom ((1,2) --> (A,B)) and A16: for x being set st x in dom ((1,2) --> (A,B)) holds g . x in ((1,2) --> (A,B)) . x by CARD_3:def_5; 2 in dom ((1,2) --> (A,B)) by A2, TARSKI:def_2; then A17: g . 2 in B by A13, A16; A18: ((1,2) --> (A,B)) . 1 = A by FUNCT_4:63; 1 in dom ((1,2) --> (A,B)) by A2, TARSKI:def_2; then A19: g . 1 in A by A18, A16; then A20: f . [(g . 1),(g . 2)] = <*(g . 1),(g . 2)*> by A1, A17; A21: now__::_thesis:_for_k_being_set_st_k_in_dom_g_holds_ g_._k_=_<*(g_._1),(g_._2)*>_._k let k be set ; ::_thesis: ( k in dom g implies g . k = <*(g . 1),(g . 2)*> . k ) assume k in dom g ; ::_thesis: g . k = <*(g . 1),(g . 2)*> . k then ( k = 1 or k = 2 ) by A15, TARSKI:def_2; hence g . k = <*(g . 1),(g . 2)*> . k by FINSEQ_1:44; ::_thesis: verum end; A22: dom <*(g . 1),(g . 2)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; A23: [(g . 1),(g . 2)] in [:A,B:] by A19, A17, ZFMISC_1:87; the carrier of [:R^1,R^1:] = [: the carrier of R^1, the carrier of R^1:] by BORSUK_1:def_2; then [(g . 1),(g . 2)] in the carrier of [:R^1,R^1:] by A19, A17, TOPMETR:17, ZFMISC_1:87; hence a in f .: [:A,B:] by A2, A14, A15, A23, A22, A21, A20, FUNCT_1:2, FUNCT_2:35; ::_thesis: verum end; theorem Th76: :: TOPREAL6:76 for f being Function of [:R^1,R^1:],(TOP-REAL 2) st ( for x, y being Real holds f . [x,y] = <*x,y*> ) holds f is being_homeomorphism proof reconsider f1 = proj1 , f2 = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:17; let f be Function of [:R^1,R^1:],(TOP-REAL 2); ::_thesis: ( ( for x, y being Real holds f . [x,y] = <*x,y*> ) implies f is being_homeomorphism ) assume A1: for x, y being Real holds f . [x,y] = <*x,y*> ; ::_thesis: f is being_homeomorphism thus dom f = [#] [:R^1,R^1:] by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng f = [#] (TOP-REAL 2) & f is one-to-one & f is continuous & f " is continuous ) A2: the carrier of [:R^1,R^1:] = [: the carrier of R^1, the carrier of R^1:] by BORSUK_1:def_2; then A3: dom f = [: the carrier of R^1, the carrier of R^1:] by FUNCT_2:def_1; thus A4: rng f = [#] (TOP-REAL 2) ::_thesis: ( f is one-to-one & f is continuous & f " is continuous ) proof thus rng f c= [#] (TOP-REAL 2) ; :: according to XBOOLE_0:def_10 ::_thesis: [#] (TOP-REAL 2) c= rng f let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [#] (TOP-REAL 2) or y in rng f ) assume y in [#] (TOP-REAL 2) ; ::_thesis: y in rng f then consider a, b being Real such that A5: y = <*a,b*> by EUCLID:51; A6: f . [a,b] = <*a,b*> by A1; [a,b] in dom f by A3, TOPMETR:17, ZFMISC_1:87; hence y in rng f by A5, A6, FUNCT_1:def_3; ::_thesis: verum end; thus A7: f is one-to-one ::_thesis: ( f is continuous & f " is continuous ) proof let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume x in dom f ; ::_thesis: ( not y in dom f or not f . x = f . y or x = y ) then consider x1, x2 being set such that A8: x1 in REAL and A9: x2 in REAL and A10: x = [x1,x2] by A2, TOPMETR:17, ZFMISC_1:def_2; assume y in dom f ; ::_thesis: ( not f . x = f . y or x = y ) then consider y1, y2 being set such that A11: y1 in REAL and A12: y2 in REAL and A13: y = [y1,y2] by A2, TOPMETR:17, ZFMISC_1:def_2; reconsider x1 = x1, x2 = x2, y1 = y1, y2 = y2 as Real by A8, A9, A11, A12; assume A14: f . x = f . y ; ::_thesis: x = y A15: f . [y1,y2] = <*y1,y2*> by A1; A16: f . [x1,x2] = <*x1,x2*> by A1; then x1 = y1 by A10, A13, A15, A14, FINSEQ_1:77; hence x = y by A10, A13, A16, A15, A14, FINSEQ_1:77; ::_thesis: verum end; A17: now__::_thesis:_for_x_being_set_st_x_in_dom_(f_")_holds_ (f_")_._x_=_<:f1,f2:>_._x A18: dom f2 = the carrier of (TOP-REAL 2) by FUNCT_2:def_1; let x be set ; ::_thesis: ( x in dom (f ") implies (f ") . x = <:f1,f2:> . x ) A19: dom f1 = the carrier of (TOP-REAL 2) by FUNCT_2:def_1; assume A20: x in dom (f ") ; ::_thesis: (f ") . x = <:f1,f2:> . x then consider a, b being Real such that A21: x = <*a,b*> by EUCLID:51; reconsider p = x as Point of (TOP-REAL 2) by A20; A22: [a,b] in dom f by A3, TOPMETR:17, ZFMISC_1:87; A23: f . [a,b] = <*a,b*> by A1; f is onto by A4, FUNCT_2:def_3; hence (f ") . x = (f ") . x by A7, TOPS_2:def_4 .= [a,b] by A7, A21, A22, A23, FUNCT_1:32 .= [(p `1),b] by A21, EUCLID:52 .= [(p `1),(p `2)] by A21, EUCLID:52 .= [(f1 . x),(p `2)] by PSCOMP_1:def_5 .= [(f1 . x),(f2 . x)] by PSCOMP_1:def_6 .= <:f1,f2:> . x by A20, A19, A18, FUNCT_3:49 ; ::_thesis: verum end; thus f is continuous ::_thesis: f " is continuous proof let w be Point of [:R^1,R^1:]; :: according to BORSUK_1:def_1 ::_thesis: for b1 being a_neighborhood of f . w ex b2 being a_neighborhood of w st f .: b2 c= b1 let G be a_neighborhood of f . w; ::_thesis: ex b1 being a_neighborhood of w st f .: b1 c= G reconsider fw = f . w as Point of (Euclid 2) by TOPREAL3:8; consider x, y being set such that A24: x in the carrier of R^1 and A25: y in the carrier of R^1 and A26: w = [x,y] by A2, ZFMISC_1:def_2; reconsider x = x, y = y as Real by A24, A25, TOPMETR:17; fw in Int G by CONNSP_2:def_1; then consider r being real number such that A27: r > 0 and A28: Ball (fw,r) c= G by GOBOARD6:5; reconsider r = r as Real by XREAL_0:def_1; set A = ].(((f . w) `1) - (r / (sqrt 2))),(((f . w) `1) + (r / (sqrt 2))).[; set B = ].(((f . w) `2) - (r / (sqrt 2))),(((f . w) `2) + (r / (sqrt 2))).[; reconsider 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))).[ as Subset of R^1 by TOPMETR:17; A29: f . [x,y] = <*x,y*> by A1; then y = (f . w) `2 by A26, EUCLID:52; then A30: y in B by A27, Th15, SQUARE_1:19, XREAL_1:139; x = (f . w) `1 by A26, A29, EUCLID:52; then x in A by A27, Th15, SQUARE_1:19, XREAL_1:139; then A31: w in [:A,B:] by A26, A30, ZFMISC_1:87; take [:A,B:] ; ::_thesis: ( [:A,B:] is a_neighborhood of w & f .: [:A,B:] c= G ) A32: B is open by JORDAN6:35; A is open by JORDAN6:35; then [:A,B:] in Base-Appr [:A,B:] by A32; then w in union (Base-Appr [:A,B:]) by A31, TARSKI:def_4; then w in Int [:A,B:] by BORSUK_1:14; hence [:A,B:] is a_neighborhood of w by CONNSP_2:def_1; ::_thesis: f .: [:A,B:] c= G product ((1,2) --> (A,B)) c= Ball (fw,r) by Th41; then f .: [:A,B:] c= Ball (fw,r) by A1, Th75; hence f .: [:A,B:] c= G by A28, XBOOLE_1:1; ::_thesis: verum end; A33: f1 is continuous by JORDAN5A:27; A34: f2 is continuous by JORDAN5A:27; dom <:f1,f2:> = the carrier of (TOP-REAL 2) by FUNCT_2:def_1; then f " = <:f1,f2:> by A4, A7, A17, FUNCT_1:2, TOPS_2:49; hence f " is continuous by A33, A34, YELLOW12:41; ::_thesis: verum end; theorem :: TOPREAL6:77 [:R^1,R^1:], TOP-REAL 2 are_homeomorphic proof defpred S1[ Element of REAL , Element of REAL , set ] means ex c being Element of REAL 2 st ( c = \$3 & \$3 = <*\$1,\$2*> ); A1: the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22; A2: for x, y being Element of REAL ex u being Element of REAL 2 st S1[x,y,u] proof let x, y be Element of REAL ; ::_thesis: ex u being Element of REAL 2 st S1[x,y,u] take <*x,y*> ; ::_thesis: ( <*x,y*> is Element of REAL 2 & S1[x,y,<*x,y*>] ) thus <*x,y*> is Element of REAL 2 by FINSEQ_2:137; ::_thesis: S1[x,y,<*x,y*>] <*x,y*> in 2 -tuples_on REAL by FINSEQ_2:137; hence S1[x,y,<*x,y*>] ; ::_thesis: verum end; consider f being Function of [:REAL,REAL:],(REAL 2) such that A3: for x, y being Element of REAL holds S1[x,y,f . (x,y)] from BINOP_1:sch_3(A2); the carrier of [:R^1,R^1:] = [: the carrier of R^1, the carrier of R^1:] by BORSUK_1:def_2; then reconsider f = f as Function of [:R^1,R^1:],(TOP-REAL 2) by A1, TOPMETR:17; take f ; :: according to T_0TOPSP:def_1 ::_thesis: f is being_homeomorphism for x, y being Real holds f . [x,y] = <*x,y*> proof let x, y be Real; ::_thesis: f . [x,y] = <*x,y*> S1[x,y,f . (x,y)] by A3; hence f . [x,y] = <*x,y*> ; ::_thesis: verum end; hence f is being_homeomorphism by Th76; ::_thesis: verum end; begin theorem Th78: :: TOPREAL6:78 for A, B being compact Subset of REAL holds product ((1,2) --> (A,B)) is compact Subset of (TOP-REAL 2) proof defpred S1[ Element of REAL , Element of REAL , set ] means ex c being Element of REAL 2 st ( c = \$3 & \$3 = <*\$1,\$2*> ); let A, B be compact Subset of REAL; ::_thesis: product ((1,2) --> (A,B)) is compact Subset of (TOP-REAL 2) reconsider X = product ((1,2) --> (A,B)) as Subset of (TOP-REAL 2) by Th22; reconsider A1 = A, B1 = B as Subset of R^1 by TOPMETR:17; A1: the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22; A2: for x, y being Element of REAL ex u being Element of REAL 2 st S1[x,y,u] proof let x, y be Element of REAL ; ::_thesis: ex u being Element of REAL 2 st S1[x,y,u] take <*x,y*> ; ::_thesis: ( <*x,y*> is Element of REAL 2 & S1[x,y,<*x,y*>] ) thus <*x,y*> is Element of REAL 2 by FINSEQ_2:137; ::_thesis: S1[x,y,<*x,y*>] <*x,y*> in 2 -tuples_on REAL by FINSEQ_2:137; hence S1[x,y,<*x,y*>] ; ::_thesis: verum end; consider h being Function of [:REAL,REAL:],(REAL 2) such that A3: for x, y being Element of REAL holds S1[x,y,h . (x,y)] from BINOP_1:sch_3(A2); the carrier of [:R^1,R^1:] = [: the carrier of R^1, the carrier of R^1:] by BORSUK_1:def_2; then reconsider h = h as Function of [:R^1,R^1:],(TOP-REAL 2) by A1, TOPMETR:17; A4: for x, y being Real holds h . [x,y] = <*x,y*> proof let x, y be Real; ::_thesis: h . [x,y] = <*x,y*> S1[x,y,h . (x,y)] by A3; hence h . [x,y] = <*x,y*> ; ::_thesis: verum end; then A5: h is being_homeomorphism by Th76; A6: B1 is compact by JORDAN5A:25; A1 is compact by JORDAN5A:25; then A7: [:A1,B1:] is compact by A6, BORSUK_3:23; h .: [:A1,B1:] = X by A4, Th75; hence product ((1,2) --> (A,B)) is compact Subset of (TOP-REAL 2) by A7, A5, WEIERSTR:8; ::_thesis: verum end; theorem Th79: :: TOPREAL6:79 for P being Subset of (TOP-REAL 2) st P is bounded & P is closed holds P is compact proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is bounded & P is closed implies P is compact ) assume A1: ( P is bounded & P is closed ) ; ::_thesis: P is compact then reconsider C = P as bounded Subset of (Euclid 2) by JORDAN2C:11; consider r being Real, e being Point of (Euclid 2) such that 0 < r and A2: C c= Ball (e,r) by METRIC_6:def_3; reconsider p = e as Point of (TOP-REAL 2) by TOPREAL3:8; A3: ].((p `2) - r),((p `2) + r).[ c= [.((p `2) - r),((p `2) + r).] by XXREAL_1:25; A4: Ball (e,r) c= product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) by Th42; ].((p `1) - r),((p `1) + r).[ c= [.((p `1) - r),((p `1) + r).] by XXREAL_1:25; 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 A3, Th21; then A5: Ball (e,r) c= product ((1,2) --> ([.((p `1) - r),((p `1) + r).],[.((p `2) - r),((p `2) + r).])) by 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 Th78; hence P is compact by A1, A2, A5, COMPTS_1:9, XBOOLE_1:1; ::_thesis: verum end; theorem Th80: :: TOPREAL6:80 for P being Subset of (TOP-REAL 2) st P is bounded holds for g being continuous RealMap of (TOP-REAL 2) holds Cl (g .: P) c= g .: (Cl P) proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is bounded implies for g being continuous RealMap of (TOP-REAL 2) holds Cl (g .: P) c= g .: (Cl P) ) assume P is bounded ; ::_thesis: for g being continuous RealMap of (TOP-REAL 2) holds Cl (g .: P) c= g .: (Cl P) then A1: Cl P is compact by Th79; let g be continuous RealMap of (TOP-REAL 2); ::_thesis: Cl (g .: P) c= g .: (Cl P) reconsider f = g as Function of (TOP-REAL 2),R^1 by TOPMETR:17; f is continuous by JORDAN5A:27; then f .: (Cl P) is closed by A1, COMPTS_1:7, WEIERSTR:9; then A2: g .: (Cl P) is closed by JORDAN5A:23; g .: P c= g .: (Cl P) by PRE_TOPC:18, RELAT_1:123; hence Cl (g .: P) c= g .: (Cl P) by A2, MEASURE6:57; ::_thesis: verum end; theorem Th81: :: TOPREAL6:81 for P being Subset of (TOP-REAL 2) holds proj1 .: (Cl P) c= Cl (proj1 .: P) proof let P be Subset of (TOP-REAL 2); ::_thesis: proj1 .: (Cl P) c= Cl (proj1 .: P) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in proj1 .: (Cl P) or y in Cl (proj1 .: P) ) assume y in proj1 .: (Cl P) ; ::_thesis: y in Cl (proj1 .: 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:64; reconsider x = 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 not O /\ (proj1 .: P) is empty proof reconsider e = x as Point of (Euclid 2) by TOPREAL3:8; let O be open Subset of REAL; ::_thesis: ( y in O implies not O /\ (proj1 .: P) is empty ) assume y in O ; ::_thesis: not O /\ (proj1 .: P) is empty then consider g being real number such that A4: 0 < g and A5: ].((proj1 . x) - g),((proj1 . x) + g).[ c= O by A3, RCOMP_1:19; reconsider g = g as Real by XREAL_0:def_1; reconsider B = Ball (e,(g / 2)) as Subset of (TOP-REAL 2) by TOPREAL3:8; A6: B is open by GOBOARD6:3; e in B by A4, TBSP_1:11, XREAL_1:139; then P meets B by A2, A6, TOPS_1:12; 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:4; A8: d in B by A7, XBOOLE_0:def_4; then (x `1) - (g / 2) < d `1 by Th39; then A9: (proj1 . x) - (g / 2) < d `1 by PSCOMP_1:def_5; d `1 < (x `1) + (g / 2) by A8, Th39; then A10: d `1 < (proj1 . x) + (g / 2) by PSCOMP_1:def_5; d in P by A7, XBOOLE_0:def_4; then proj1 . d in proj1 .: P by FUNCT_2:35; then A11: d `1 in proj1 .: P by PSCOMP_1:def_5; A12: g / 2 < g / 1 by A4, XREAL_1:76; then (proj1 . x) - g < (proj1 . x) - (g / 2) by XREAL_1:15; then A13: (proj1 . x) - g < d `1 by A9, XXREAL_0:2; (proj1 . x) + (g / 2) < (proj1 . x) + g by A12, XREAL_1:6; then A14: d `1 < (proj1 . x) + g by A10, XXREAL_0:2; ].((proj1 . x) - g),((proj1 . x) + g).[ = { t where t is Real : ( (proj1 . x) - g < t & t < (proj1 . x) + g ) } by RCOMP_1:def_2; then d `1 in ].((proj1 . x) - g),((proj1 . x) + g).[ by A13, A14; hence not O /\ (proj1 .: P) is empty by A5, A11, XBOOLE_0:def_4; ::_thesis: verum end; hence y in Cl (proj1 .: P) by A3, MEASURE6:63; ::_thesis: verum end; theorem Th82: :: TOPREAL6:82 for P being Subset of (TOP-REAL 2) holds proj2 .: (Cl P) c= Cl (proj2 .: P) proof let P be Subset of (TOP-REAL 2); ::_thesis: proj2 .: (Cl P) c= Cl (proj2 .: P) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in proj2 .: (Cl P) or y in Cl (proj2 .: P) ) assume y in proj2 .: (Cl P) ; ::_thesis: y in Cl (proj2 .: 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:64; reconsider x = 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 not O /\ (proj2 .: P) is empty proof reconsider e = x as Point of (Euclid 2) by TOPREAL3:8; let O be open Subset of REAL; ::_thesis: ( y in O implies not O /\ (proj2 .: P) is empty ) assume y in O ; ::_thesis: not O /\ (proj2 .: P) is empty then consider g being real number such that A4: 0 < g and A5: ].((proj2 . x) - g),((proj2 . x) + g).[ c= O by A3, RCOMP_1:19; reconsider g = g as Real by XREAL_0:def_1; reconsider B = Ball (e,(g / 2)) as Subset of (TOP-REAL 2) by TOPREAL3:8; A6: B is open by GOBOARD6:3; e in B by A4, TBSP_1:11, XREAL_1:139; then P meets B by A2, A6, TOPS_1:12; 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:4; A8: d in B by A7, XBOOLE_0:def_4; then (x `2) - (g / 2) < d `2 by Th40; then A9: (proj2 . x) - (g / 2) < d `2 by PSCOMP_1:def_6; d `2 < (x `2) + (g / 2) by A8, Th40; then A10: d `2 < (proj2 . x) + (g / 2) by PSCOMP_1:def_6; d in P by A7, XBOOLE_0:def_4; then proj2 . d in proj2 .: P by FUNCT_2:35; then A11: d `2 in proj2 .: P by PSCOMP_1:def_6; A12: g / 2 < g / 1 by A4, XREAL_1:76; then (proj2 . x) - g < (proj2 . x) - (g / 2) by XREAL_1:15; then A13: (proj2 . x) - g < d `2 by A9, XXREAL_0:2; (proj2 . x) + (g / 2) < (proj2 . x) + g by A12, XREAL_1:6; then A14: d `2 < (proj2 . x) + g by A10, XXREAL_0:2; ].((proj2 . x) - g),((proj2 . x) + g).[ = { t where t is Real : ( (proj2 . x) - g < t & t < (proj2 . x) + g ) } by RCOMP_1:def_2; then d `2 in ].((proj2 . x) - g),((proj2 . x) + g).[ by A13, A14; hence not O /\ (proj2 .: P) is empty by A5, A11, XBOOLE_0:def_4; ::_thesis: verum end; hence y in Cl (proj2 .: P) by A3, MEASURE6:63; ::_thesis: verum end; theorem Th83: :: TOPREAL6:83 for P being Subset of (TOP-REAL 2) st P is bounded holds Cl (proj1 .: P) = proj1 .: (Cl P) proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is bounded implies Cl (proj1 .: P) = proj1 .: (Cl P) ) assume P is bounded ; ::_thesis: Cl (proj1 .: P) = proj1 .: (Cl P) hence Cl (proj1 .: P) c= proj1 .: (Cl P) by Th80; :: according to XBOOLE_0:def_10 ::_thesis: proj1 .: (Cl P) c= Cl (proj1 .: P) thus proj1 .: (Cl P) c= Cl (proj1 .: P) by Th81; ::_thesis: verum end; theorem Th84: :: TOPREAL6:84 for P being Subset of (TOP-REAL 2) st P is bounded holds Cl (proj2 .: P) = proj2 .: (Cl P) proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is bounded implies Cl (proj2 .: P) = proj2 .: (Cl P) ) assume P is bounded ; ::_thesis: Cl (proj2 .: P) = proj2 .: (Cl P) hence Cl (proj2 .: P) c= proj2 .: (Cl P) by Th80; :: according to XBOOLE_0:def_10 ::_thesis: proj2 .: (Cl P) c= Cl (proj2 .: P) thus proj2 .: (Cl P) c= Cl (proj2 .: P) by Th82; ::_thesis: verum end; theorem :: TOPREAL6:85 for D being non empty Subset of (TOP-REAL 2) st D is bounded holds W-bound D = W-bound (Cl D) proof let D be non empty Subset of (TOP-REAL 2); ::_thesis: ( D is bounded implies W-bound D = W-bound (Cl D) ) A1: D c= Cl D by PRE_TOPC:18; assume A2: D is bounded ; ::_thesis: W-bound D = W-bound (Cl D) then Cl D is compact by Th79; then proj1 .: (Cl D) is bounded_below ; then proj1 .: D is bounded_below by A1, RELAT_1:123, XXREAL_2:44; then A3: lower_bound (proj1 .: D) = lower_bound (Cl (proj1 .: D)) by Th68 .= lower_bound (proj1 .: (Cl D)) by A2, Th83 ; W-bound D = lower_bound (proj1 .: D) by SPRECT_1:43; hence W-bound D = W-bound (Cl D) by A3, SPRECT_1:43; ::_thesis: verum end; theorem :: TOPREAL6:86 for D being non empty Subset of (TOP-REAL 2) st D is bounded holds E-bound D = E-bound (Cl D) proof let D be non empty Subset of (TOP-REAL 2); ::_thesis: ( D is bounded implies E-bound D = E-bound (Cl D) ) A1: D c= Cl D by PRE_TOPC:18; assume A2: D is bounded ; ::_thesis: E-bound D = E-bound (Cl D) then Cl D is compact by Th79; then proj1 .: (Cl D) is bounded_above ; then proj1 .: D is bounded_above by A1, RELAT_1:123, XXREAL_2:43; then A3: upper_bound (proj1 .: D) = upper_bound (Cl (proj1 .: D)) by Th69 .= upper_bound (proj1 .: (Cl D)) by A2, Th83 ; E-bound D = upper_bound (proj1 .: D) by SPRECT_1:46; hence E-bound D = E-bound (Cl D) by A3, SPRECT_1:46; ::_thesis: verum end; theorem :: TOPREAL6:87 for D being non empty Subset of (TOP-REAL 2) st D is bounded holds N-bound D = N-bound (Cl D) proof let D be non empty Subset of (TOP-REAL 2); ::_thesis: ( D is bounded implies N-bound D = N-bound (Cl D) ) A1: D c= Cl D by PRE_TOPC:18; assume A2: D is bounded ; ::_thesis: N-bound D = N-bound (Cl D) then Cl D is compact by Th79; then proj2 .: (Cl D) is bounded_above ; then proj2 .: D is bounded_above by A1, RELAT_1:123, XXREAL_2:43; then A3: upper_bound (proj2 .: D) = upper_bound (Cl (proj2 .: D)) by Th69 .= upper_bound (proj2 .: (Cl D)) by A2, Th84 ; N-bound D = upper_bound (proj2 .: D) by SPRECT_1:45; hence N-bound D = N-bound (Cl D) by A3, SPRECT_1:45; ::_thesis: verum end; theorem :: TOPREAL6:88 for D being non empty Subset of (TOP-REAL 2) st D is bounded holds S-bound D = S-bound (Cl D) proof let D be non empty Subset of (TOP-REAL 2); ::_thesis: ( D is bounded implies S-bound D = S-bound (Cl D) ) A1: D c= Cl D by PRE_TOPC:18; assume A2: D is bounded ; ::_thesis: S-bound D = S-bound (Cl D) then Cl D is compact by Th79; then proj2 .: (Cl D) is bounded_below ; then proj2 .: D is bounded_below by A1, RELAT_1:123, XXREAL_2:44; then A3: lower_bound (proj2 .: D) = lower_bound (Cl (proj2 .: D)) by Th68 .= lower_bound (proj2 .: (Cl D)) by A2, Th84 ; S-bound D = lower_bound (proj2 .: D) by SPRECT_1:44; hence S-bound D = S-bound (Cl D) by A3, SPRECT_1:44; ::_thesis: verum end; theorem Th89: :: TOPREAL6:89 for n being Element of NAT for A, B being Subset of (TOP-REAL n) st ( A is bounded or B is bounded ) holds A /\ B is bounded proof let n be Element of NAT ; ::_thesis: for A, B being Subset of (TOP-REAL n) st ( A is bounded or B is bounded ) holds A /\ B is bounded let A, B be Subset of (TOP-REAL n); ::_thesis: ( ( A is bounded or B is bounded ) implies A /\ B is bounded ) assume A1: ( A is bounded or B is bounded ) ; ::_thesis: A /\ B is bounded percases ( A is bounded or B is bounded ) by A1; suppose A is bounded ; ::_thesis: A /\ B is bounded hence A /\ B is bounded by RLTOPSP1:42, XBOOLE_1:17; ::_thesis: verum end; suppose B is bounded ; ::_thesis: A /\ B is bounded hence A /\ B is bounded by RLTOPSP1:42, XBOOLE_1:17; ::_thesis: verum end; end; end; theorem :: TOPREAL6:90 for n being Element of NAT for A, B being Subset of (TOP-REAL n) st not A is bounded & B is bounded holds not A \ B is bounded proof let n be Element of NAT ; ::_thesis: for A, B being Subset of (TOP-REAL n) st not A is bounded & B is bounded holds not A \ B is bounded let A, B be Subset of (TOP-REAL n); ::_thesis: ( not A is bounded & B is bounded implies not A \ B is bounded ) assume that A1: not A is bounded and A2: B is bounded ; ::_thesis: not A \ B is bounded A3: (A \ B) \/ (A /\ B) = A \ (B \ B) by XBOOLE_1:52 .= A \ {} by XBOOLE_1:37 .= A ; A /\ B is bounded by A2, Th89; hence not A \ B is bounded by A1, A3, Th67; ::_thesis: verum end; begin definition let n be Element of NAT ; let a, b be Point of (TOP-REAL n); func dist (a,b) -> Real means :Def1: :: TOPREAL6:def 1 ex p, q being Point of (Euclid n) st ( p = a & q = b & it = dist (p,q) ); existence ex b1 being Real ex p, q being Point of (Euclid n) st ( p = a & q = b & b1 = dist (p,q) ) proof reconsider p = a, q = b as Point of (Euclid n) by TOPREAL3:8; take dist (p,q) ; ::_thesis: ex p, q being Point of (Euclid n) st ( p = a & q = b & dist (p,q) = dist (p,q) ) thus ex p, q being Point of (Euclid n) st ( p = a & q = b & dist (p,q) = dist (p,q) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Real st ex p, q being Point of (Euclid n) st ( p = a & q = b & b1 = dist (p,q) ) & ex p, q being Point of (Euclid n) st ( p = a & q = b & b2 = dist (p,q) ) holds b1 = b2 ; commutativity for b1 being Real for a, b being Point of (TOP-REAL n) st ex p, q being Point of (Euclid n) st ( p = a & q = b & b1 = dist (p,q) ) holds ex p, q being Point of (Euclid n) st ( p = b & q = a & b1 = dist (p,q) ) ; end; :: deftheorem Def1 defines dist TOPREAL6:def_1_:_ for n being Element of NAT for a, b being Point of (TOP-REAL n) for b4 being Real holds ( b4 = dist (a,b) iff ex p, q being Point of (Euclid n) st ( p = a & q = b & b4 = dist (p,q) ) ); theorem Th91: :: TOPREAL6:91 for r1, s1, r2, s2 being real number for u, v being Point of (Euclid 2) st u = |[r1,s1]| & v = |[r2,s2]| holds dist (u,v) = sqrt (((r1 - r2) ^2) + ((s1 - s2) ^2)) proof let r1, s1, r2, s2 be real number ; ::_thesis: for u, v being Point of (Euclid 2) st u = |[r1,s1]| & v = |[r2,s2]| holds dist (u,v) = sqrt (((r1 - r2) ^2) + ((s1 - s2) ^2)) let u, v be Point of (Euclid 2); ::_thesis: ( u = |[r1,s1]| & v = |[r2,s2]| implies dist (u,v) = sqrt (((r1 - r2) ^2) + ((s1 - s2) ^2)) ) assume that A1: u = |[r1,s1]| and A2: v = |[r2,s2]| ; ::_thesis: dist (u,v) = sqrt (((r1 - r2) ^2) + ((s1 - s2) ^2)) A3: |[r1,s1]| `1 = r1 by EUCLID:52; A4: |[r2,s2]| `2 = s2 by EUCLID:52; A5: |[r2,s2]| `1 = r2 by EUCLID:52; A6: |[r1,s1]| `2 = s1 by EUCLID:52; thus dist (u,v) = (Pitag_dist 2) . (u,v) by METRIC_1:def_1 .= sqrt (((r1 - r2) ^2) + ((s1 - s2) ^2)) by A1, A2, A3, A6, A5, A4, TOPREAL3:7 ; ::_thesis: verum end; theorem Th92: :: TOPREAL6:92 for p, q being Point of (TOP-REAL 2) holds dist (p,q) = sqrt ((((p `1) - (q `1)) ^2) + (((p `2) - (q `2)) ^2)) proof let p, q be Point of (TOP-REAL 2); ::_thesis: dist (p,q) = sqrt ((((p `1) - (q `1)) ^2) + (((p `2) - (q `2)) ^2)) A1: p = |[(p `1),(p `2)]| by EUCLID:53; A2: q = |[(q `1),(q `2)]| by EUCLID:53; ex a, b being Point of (Euclid 2) st ( p = a & q = b & dist (a,b) = dist (p,q) ) by Def1; hence dist (p,q) = sqrt ((((p `1) - (q `1)) ^2) + (((p `2) - (q `2)) ^2)) by A1, A2, Th91; ::_thesis: verum end; theorem :: TOPREAL6:93 for n being Element of NAT for p being Point of (TOP-REAL n) holds dist (p,p) = 0 proof let n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL n) holds dist (p,p) = 0 let p be Point of (TOP-REAL n); ::_thesis: dist (p,p) = 0 ex a, b being Point of (Euclid n) st ( a = p & b = p & dist (a,b) = dist (p,p) ) by Def1; hence dist (p,p) = 0 by METRIC_1:1; ::_thesis: verum end; theorem :: TOPREAL6:94 for n being Element of NAT for p, q, r being Point of (TOP-REAL n) holds dist (p,r) <= (dist (p,q)) + (dist (q,r)) proof let n be Element of NAT ; ::_thesis: for p, q, r being Point of (TOP-REAL n) holds dist (p,r) <= (dist (p,q)) + (dist (q,r)) let p, q, r be Point of (TOP-REAL n); ::_thesis: dist (p,r) <= (dist (p,q)) + (dist (q,r)) A1: ex a, b being Point of (Euclid n) st ( a = p & b = r & dist (a,b) = dist (p,r) ) by Def1; A2: ex a, b being Point of (Euclid n) st ( a = q & b = r & dist (a,b) = dist (q,r) ) by Def1; ex a, b being Point of (Euclid n) st ( a = p & b = q & dist (a,b) = dist (p,q) ) by Def1; hence dist (p,r) <= (dist (p,q)) + (dist (q,r)) by A1, A2, METRIC_1:4; ::_thesis: verum end; theorem :: TOPREAL6:95 for x1, x2, y1, y2 being real number for a, b being Point of (TOP-REAL 2) st x1 <= a `1 & a `1 <= x2 & y1 <= a `2 & a `2 <= y2 & x1 <= b `1 & b `1 <= x2 & y1 <= b `2 & b `2 <= y2 holds dist (a,b) <= (x2 - x1) + (y2 - y1) proof let x1, x2, y1, y2 be real number ; ::_thesis: for a, b being Point of (TOP-REAL 2) st x1 <= a `1 & a `1 <= x2 & y1 <= a `2 & a `2 <= y2 & x1 <= b `1 & b `1 <= x2 & y1 <= b `2 & b `2 <= y2 holds dist (a,b) <= (x2 - x1) + (y2 - y1) let a, b be Point of (TOP-REAL 2); ::_thesis: ( x1 <= a `1 & a `1 <= x2 & y1 <= a `2 & a `2 <= y2 & x1 <= b `1 & b `1 <= x2 & y1 <= b `2 & b `2 <= y2 implies dist (a,b) <= (x2 - x1) + (y2 - y1) ) assume that A1: x1 <= a `1 and A2: a `1 <= x2 and A3: y1 <= a `2 and A4: a `2 <= y2 and A5: x1 <= b `1 and A6: b `1 <= x2 and A7: y1 <= b `2 and A8: b `2 <= y2 ; ::_thesis: dist (a,b) <= (x2 - x1) + (y2 - y1) A9: y2 is Real by XREAL_0:def_1; y1 is Real by XREAL_0:def_1; then A10: abs ((a `2) - (b `2)) <= y2 - y1 by A3, A4, A7, A8, A9, JGRAPH_1:27; A11: ((a `1) - (b `1)) ^2 >= 0 by XREAL_1:63; A12: ((a `2) - (b `2)) ^2 >= 0 by XREAL_1:63; dist (a,b) = sqrt ((((a `1) - (b `1)) ^2) + (((a `2) - (b `2)) ^2)) by Th92; then dist (a,b) <= (sqrt (((a `1) - (b `1)) ^2)) + (sqrt (((a `2) - (b `2)) ^2)) by A11, A12, Th1; then dist (a,b) <= (abs ((a `1) - (b `1))) + (sqrt (((a `2) - (b `2)) ^2)) by COMPLEX1:72; then A13: dist (a,b) <= (abs ((a `1) - (b `1))) + (abs ((a `2) - (b `2))) by COMPLEX1:72; A14: x2 is Real by XREAL_0:def_1; x1 is Real by XREAL_0:def_1; then abs ((a `1) - (b `1)) <= x2 - x1 by A1, A2, A5, A6, A14, JGRAPH_1:27; then (abs ((a `1) - (b `1))) + (abs ((a `2) - (b `2))) <= (x2 - x1) + (y2 - y1) by A10, XREAL_1:7; hence dist (a,b) <= (x2 - x1) + (y2 - y1) by A13, XXREAL_0:2; ::_thesis: verum end;