:: 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;