:: JORDAN5A semantic presentation
begin
theorem Th1: :: JORDAN5A:1
for n being Element of NAT
for p, q being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st P is_an_arc_of p,q holds
P is compact
proof
let n be Element of NAT ; ::_thesis: for p, q being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st P is_an_arc_of p,q holds
P is compact
let p, q be Point of (TOP-REAL n); ::_thesis: for P being Subset of (TOP-REAL n) st P is_an_arc_of p,q holds
P is compact
let P be Subset of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p,q implies P is compact )
assume P is_an_arc_of p,q ; ::_thesis: P is compact
then consider f being Function of I[01],((TOP-REAL n) | P) such that
A1: f is being_homeomorphism and
f . 0 = p and
f . 1 = q by TOPREAL1:def_1;
percases ( P <> {} or P = {} (TOP-REAL n) ) ;
suppose P <> {} ; ::_thesis: P is compact
then reconsider P9 = P as non empty Subset of (TOP-REAL n) ;
( f is continuous & rng f = [#] ((TOP-REAL n) | P9) ) by A1, TOPS_2:def_5;
then (TOP-REAL n) | P9 is compact by COMPTS_1:14;
hence P is compact by COMPTS_1:3; ::_thesis: verum
end;
suppose P = {} (TOP-REAL n) ; ::_thesis: P is compact
hence P is compact ; ::_thesis: verum
end;
end;
end;
Lm1: for n being Element of NAT holds
( the carrier of (Euclid n) = REAL n & the carrier of (TOP-REAL n) = REAL n )
proof
let n be Element of NAT ; ::_thesis: ( the carrier of (Euclid n) = REAL n & the carrier of (TOP-REAL n) = REAL n )
Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #) by EUCLID:def_7;
hence ( the carrier of (Euclid n) = REAL n & the carrier of (TOP-REAL n) = REAL n ) by EUCLID:67; ::_thesis: verum
end;
theorem Th2: :: JORDAN5A:2
for n being Element of NAT
for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being real number holds
( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 )
proof
let n be Element of NAT ; ::_thesis: for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being real number holds
( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 )
let p1, p2 be Point of (TOP-REAL n); ::_thesis: for r1, r2 being real number holds
( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 )
let r1, r2 be real number ; ::_thesis: ( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 )
assume A1: ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) ; ::_thesis: ( r1 = r2 or p1 = p2 )
A2: (1 * p1) + ((- (r1 * p1)) + (r1 * p2)) = ((1 * p1) + (- (r1 * p1))) + (r1 * p2) by EUCLID:26
.= ((1 * p1) - (r1 * p1)) + (r1 * p2) by EUCLID:41
.= ((1 - r2) * p1) + (r2 * p2) by A1, EUCLID:50
.= ((1 * p1) - (r2 * p1)) + (r2 * p2) by EUCLID:50
.= ((1 * p1) + (- (r2 * p1))) + (r2 * p2) by EUCLID:41
.= (1 * p1) + ((- (r2 * p1)) + (r2 * p2)) by EUCLID:26 ;
A3: ((r2 - r1) * p1) + (r1 * p2) = ((r2 * p1) - (r1 * p1)) + (r1 * p2) by EUCLID:50
.= ((r2 * p1) + (- (r1 * p1))) + (r1 * p2) by EUCLID:41
.= (r2 * p1) + ((- (r1 * p1)) + (r1 * p2)) by EUCLID:26
.= (r2 * p1) + ((- (r2 * p1)) + (r2 * p2)) by A2, GOBOARD7:4
.= ((r2 * p1) + (- (r2 * p1))) + (r2 * p2) by EUCLID:26
.= (0. (TOP-REAL n)) + (r2 * p2) by EUCLID:36
.= r2 * p2 by EUCLID:27 ;
(r2 - r1) * p1 = ((r2 - r1) * p1) + (0. (TOP-REAL n)) by EUCLID:27
.= ((r2 - r1) * p1) + ((r1 * p2) - (r1 * p2)) by EUCLID:42
.= (r2 * p2) - (r1 * p2) by A3, EUCLID:45
.= (r2 - r1) * p2 by EUCLID:50 ;
then ( r2 - r1 = 0 or p1 = p2 ) by EUCLID:34;
hence ( r1 = r2 or p1 = p2 ) ; ::_thesis: verum
end;
theorem Th3: :: JORDAN5A:3
for n being Element of NAT
for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds
ex f being Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) st
( ( for x being Real st x in [.0,1.] holds
f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 )
proof
let n be Element of NAT ; ::_thesis: for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds
ex f being Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) st
( ( for x being Real st x in [.0,1.] holds
f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 )
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p1 <> p2 implies ex f being Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) st
( ( for x being Real st x in [.0,1.] holds
f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) )
reconsider p19 = p1, p29 = p2 as Element of REAL n by Lm1;
set P = LSeg (p1,p2);
reconsider PP = LSeg (p1,p2) as Subset of (Euclid n) by TOPREAL3:8;
reconsider PP = PP as non empty Subset of (Euclid n) ;
defpred S1[ set , set ] means for x being Real st x = $1 holds
$2 = ((1 - x) * p1) + (x * p2);
A1: for a being set st a in [.0,1.] holds
ex u being set st S1[a,u]
proof
let a be set ; ::_thesis: ( a in [.0,1.] implies ex u being set st S1[a,u] )
assume a in [.0,1.] ; ::_thesis: ex u being set st S1[a,u]
then reconsider x = a as Real ;
take ((1 - x) * p1) + (x * p2) ; ::_thesis: S1[a,((1 - x) * p1) + (x * p2)]
thus S1[a,((1 - x) * p1) + (x * p2)] ; ::_thesis: verum
end;
consider f being Function such that
A2: dom f = [.0,1.] and
A3: for a being set st a in [.0,1.] holds
S1[a,f . a] from CLASSES1:sch_1(A1);
rng f c= the carrier of ((TOP-REAL n) | (LSeg (p1,p2)))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) )
assume y in rng f ; ::_thesis: y in the carrier of ((TOP-REAL n) | (LSeg (p1,p2)))
then consider x being set such that
A4: x in dom f and
A5: y = f . x by FUNCT_1:def_3;
x in { r where r is Real : ( 0 <= r & r <= 1 ) } by A2, A4, RCOMP_1:def_1;
then consider r being Real such that
A6: r = x and
A7: ( 0 <= r & r <= 1 ) ;
y = ((1 - r) * p1) + (r * p2) by A2, A3, A4, A5, A6;
then y in LSeg (p1,p2) by A7;
then y in [#] ((TOP-REAL n) | (LSeg (p1,p2))) by PRE_TOPC:def_5;
hence y in the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) ; ::_thesis: verum
end;
then reconsider f = f as Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) by A2, BORSUK_1:40, FUNCT_2:def_1, RELSET_1:4;
assume A8: p1 <> p2 ; ::_thesis: ex f being Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) st
( ( for x being Real st x in [.0,1.] holds
f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 )
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A9: x1 in dom f and
A10: x2 in dom f and
A11: f . x1 = f . x2 ; ::_thesis: x1 = x2
x2 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A2, A10, RCOMP_1:def_1;
then consider r2 being Real such that
A12: r2 = x2 and
0 <= r2 and
r2 <= 1 ;
A13: f . x2 = ((1 - r2) * p1) + (r2 * p2) by A2, A3, A10, A12;
x1 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A2, A9, RCOMP_1:def_1;
then consider r1 being Real such that
A14: r1 = x1 and
0 <= r1 and
r1 <= 1 ;
f . x1 = ((1 - r1) * p1) + (r1 * p2) by A2, A3, A9, A14;
hence x1 = x2 by A8, A11, A14, A12, A13, Th2; ::_thesis: verum
end;
then A15: f is one-to-one by FUNCT_1:def_4;
A16: (TOP-REAL n) | (LSeg (p1,p2)) = TopSpaceMetr ((Euclid n) | PP) by EUCLID:63;
for W being Point of I[01]
for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G
proof
reconsider p11 = p1, p22 = p2 as Point of (Euclid n) by TOPREAL3:8;
let W be Point of I[01]; ::_thesis: for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G
let G be a_neighborhood of f . W; ::_thesis: ex H being a_neighborhood of W st f .: H c= G
reconsider W9 = W as Point of (Closed-Interval-MSpace (0,1)) by BORSUK_1:40, TOPMETR:10;
reconsider W1 = W as Real by BORSUK_1:40, TARSKI:def_3;
f . W in Int G by CONNSP_2:def_1;
then consider Q being Subset of ((TOP-REAL n) | (LSeg (p1,p2))) such that
A17: Q is open and
A18: Q c= G and
A19: f . W in Q by TOPS_1:22;
[#] ((TOP-REAL n) | (LSeg (p1,p2))) = LSeg (p1,p2) by PRE_TOPC:def_5;
then reconsider Y = f . W as Point of ((Euclid n) | PP) by TOPMETR:def_2;
consider r being real number such that
A20: r > 0 and
A21: Ball (Y,r) c= Q by A16, A17, A19, TOPMETR:15;
reconsider r = r as Element of REAL by XREAL_0:def_1;
set delta = r / ((Pitag_dist n) . (p19,p29));
reconsider H = Ball (W9,(r / ((Pitag_dist n) . (p19,p29)))) as Subset of I[01] by BORSUK_1:40, TOPMETR:10;
Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:def_7;
then A22: H is open by TOPMETR:14, TOPMETR:20;
LSeg (p1,p2) = the carrier of ((Euclid n) | PP) by TOPMETR:def_2;
then reconsider WW9 = Y as Point of (Euclid n) by TARSKI:def_3;
Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #) by EUCLID:def_7;
then A23: (Pitag_dist n) . (p19,p29) = dist (p11,p22) by METRIC_1:def_1;
A24: ( dist (p11,p22) >= 0 & dist (p11,p22) <> 0 ) by A8, METRIC_1:2, METRIC_1:5;
then W in H by A20, A23, TBSP_1:11, XREAL_1:139;
then W in Int H by A22, TOPS_1:23;
then reconsider H = H as a_neighborhood of W by CONNSP_2:def_1;
take H ; ::_thesis: f .: H c= G
A25: r / ((Pitag_dist n) . (p19,p29)) > 0 by A20, A23, A24, XREAL_1:139;
f .: H c= Ball (Y,r)
proof
reconsider WW1 = WW9 as Element of REAL n by Lm1;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f .: H or a in Ball (Y,r) )
A26: [#] ((TOP-REAL n) | (LSeg (p1,p2))) = LSeg (p1,p2) by PRE_TOPC:def_5;
assume a in f .: H ; ::_thesis: a in Ball (Y,r)
then consider u being set such that
A27: u in dom f and
A28: u in H and
A29: a = f . u by FUNCT_1:def_6;
reconsider u1 = u as Real by A2, A27;
A30: f . W = ((1 - W1) * p1) + (W1 * p2) by A3, BORSUK_1:40;
reconsider u9 = u as Point of (Closed-Interval-MSpace (0,1)) by A28;
reconsider W99 = W9, u99 = u9 as Point of RealSpace by TOPMETR:8;
A31: dist (W9,u9) = the distance of (Closed-Interval-MSpace (0,1)) . (W9,u9) by METRIC_1:def_1
.= the distance of RealSpace . (W99,u99) by TOPMETR:def_1
.= dist (W99,u99) by METRIC_1:def_1 ;
dist (W9,u9) < r / ((Pitag_dist n) . (p19,p29)) by A28, METRIC_1:11;
then abs (W1 - u1) < r / ((Pitag_dist n) . (p19,p29)) by A31, TOPMETR:11;
then abs (- (u1 - W1)) < r / ((Pitag_dist n) . (p19,p29)) ;
then A32: abs (u1 - W1) < r / ((Pitag_dist n) . (p19,p29)) by COMPLEX1:52;
A33: r / ((Pitag_dist n) . (p19,p29)) <> 0 by A20, A23, A24, XREAL_1:139;
then (Pitag_dist n) . (p19,p29) = r / (r / ((Pitag_dist n) . (p19,p29))) by XCMPLX_1:54;
then A34: |.(p19 - p29).| = r / (r / ((Pitag_dist n) . (p19,p29))) by EUCLID:def_6;
f . u in rng f by A27, FUNCT_1:def_3;
then reconsider aa = a as Point of ((Euclid n) | PP) by A29, A26, TOPMETR:def_2;
LSeg (p1,p2) = the carrier of ((Euclid n) | PP) by TOPMETR:def_2;
then reconsider aa9 = aa as Point of (Euclid n) by TARSKI:def_3;
reconsider aa1 = aa9 as Element of REAL n by Lm1;
aa1 = ((1 - u1) * p1) + (u1 * p2) by A2, A3, A27, A29;
then WW1 - aa1 = (((1 - W1) * p1) + (W1 * p2)) - (((1 - u1) * p1) + (u1 * p2)) by A30
.= (((W1 * p2) + ((1 - W1) * p1)) - ((1 - u1) * p1)) - (u1 * p2) by EUCLID:46
.= ((W1 * p2) + (((1 - W1) * p1) - ((1 - u1) * p1))) - (u1 * p2) by EUCLID:45
.= ((W1 * p2) + (((1 - W1) - (1 - u1)) * p1)) - (u1 * p2) by EUCLID:50
.= ((u1 - W1) * p1) + ((W1 * p2) - (u1 * p2)) by EUCLID:45
.= ((u1 - W1) * p1) + ((W1 - u1) * p2) by EUCLID:50
.= ((u1 - W1) * p1) + ((- (u1 - W1)) * p2)
.= ((u1 - W1) * p1) + (- ((u1 - W1) * p2)) by EUCLID:40
.= ((u1 - W1) * p1) - ((u1 - W1) * p2) by EUCLID:41
.= (u1 - W1) * (p1 - p2) by EUCLID:49
.= (u1 - W1) * (p19 - p29) ;
then A35: |.(WW1 - aa1).| = (abs (u1 - W1)) * |.(p19 - p29).| by EUCLID:11;
r / (r / ((Pitag_dist n) . (p19,p29))) > 0 by A20, A25, XREAL_1:139;
then |.(WW1 - aa1).| < (r / ((Pitag_dist n) . (p19,p29))) * (r / (r / ((Pitag_dist n) . (p19,p29)))) by A35, A32, A34, XREAL_1:68;
then ( Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #) & |.(WW1 - aa1).| < r ) by A33, EUCLID:def_7, XCMPLX_1:87;
then the distance of (Euclid n) . (WW9,aa9) < r by EUCLID:def_6;
then the distance of ((Euclid n) | PP) . (Y,aa) < r by TOPMETR:def_1;
then dist (Y,aa) < r by METRIC_1:def_1;
hence a in Ball (Y,r) by METRIC_1:11; ::_thesis: verum
end;
then f .: H c= Q by A21, XBOOLE_1:1;
hence f .: H c= G by A18, XBOOLE_1:1; ::_thesis: verum
end;
then A36: f is continuous by BORSUK_1:def_1;
take f ; ::_thesis: ( ( for x being Real st x in [.0,1.] holds
f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 )
thus for x being Real st x in [.0,1.] holds
f . x = ((1 - x) * p1) + (x * p2) by A3; ::_thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 )
[#] ((TOP-REAL n) | (LSeg (p1,p2))) c= rng f
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [#] ((TOP-REAL n) | (LSeg (p1,p2))) or a in rng f )
assume a in [#] ((TOP-REAL n) | (LSeg (p1,p2))) ; ::_thesis: a in rng f
then a in { (((1 - l) * p1) + (l * p2)) where l is Real : ( 0 <= l & l <= 1 ) } by PRE_TOPC:def_5;
then consider lambda being Real such that
A37: a = ((1 - lambda) * p1) + (lambda * p2) and
A38: ( 0 <= lambda & lambda <= 1 ) ;
lambda in { r where r is Real : ( 0 <= r & r <= 1 ) } by A38;
then A39: lambda in dom f by A2, RCOMP_1:def_1;
then a = f . lambda by A2, A3, A37;
hence a in rng f by A39, FUNCT_1:def_3; ::_thesis: verum
end;
then ( [#] I[01] = [.0,1.] & rng f = [#] ((TOP-REAL n) | (LSeg (p1,p2))) ) by BORSUK_1:40, XBOOLE_0:def_10;
hence f is being_homeomorphism by A2, A15, A36, COMPTS_1:17; ::_thesis: ( f . 0 = p1 & f . 1 = p2 )
0 in [.0,1.] by XXREAL_1:1;
hence f . 0 = ((1 - 0) * p1) + (0 * p2) by A3
.= p1 + (0 * p2) by EUCLID:29
.= p1 + (0. (TOP-REAL n)) by EUCLID:29
.= p1 by EUCLID:27 ;
::_thesis: f . 1 = p2
1 in [.0,1.] by XXREAL_1:1;
hence f . 1 = ((1 - 1) * p1) + (1 * p2) by A3
.= (0. (TOP-REAL n)) + (1 * p2) by EUCLID:29
.= 1 * p2 by EUCLID:27
.= p2 by EUCLID:29 ;
::_thesis: verum
end;
Lm2: for n being Element of NAT holds TOP-REAL n is pathwise_connected
proof
let n be Element of NAT ; ::_thesis: TOP-REAL n is pathwise_connected
set T = TOP-REAL n;
let a, b be Point of (TOP-REAL n); :: according to BORSUK_2:def_3 ::_thesis: a,b are_connected
set L = LSeg (a,b);
percases ( a <> b or a = b ) ;
suppose a <> b ; ::_thesis: a,b are_connected
then consider f being Function of I[01],((TOP-REAL n) | (LSeg (a,b))) such that
for x being Real st x in [.0,1.] holds
f . x = ((1 - x) * a) + (x * b) and
A1: f is being_homeomorphism and
A2: ( f . 0 = a & f . 1 = b ) by Th3;
rng f c= [#] ((TOP-REAL n) | (LSeg (a,b))) ;
then rng f c= LSeg (a,b) by PRE_TOPC:def_5;
then ( dom f = the carrier of I[01] & rng f c= the carrier of (TOP-REAL n) ) by FUNCT_2:def_1, XBOOLE_1:1;
then reconsider g = f as Function of I[01],(TOP-REAL n) by RELSET_1:4;
f is continuous by A1, TOPS_2:def_5;
then g is continuous by PRE_TOPC:26;
hence a,b are_connected by A2, BORSUK_2:def_1; ::_thesis: verum
end;
suppose a = b ; ::_thesis: a,b are_connected
hence a,b are_connected ; ::_thesis: verum
end;
end;
end;
registration
let n be Element of NAT ;
cluster TOP-REAL n -> pathwise_connected ;
coherence
TOP-REAL n is pathwise_connected by Lm2;
end;
registration
let n be Element of NAT ;
cluster non empty strict TopSpace-like T_0 T_1 T_2 compact for SubSpace of TOP-REAL n;
existence
ex b1 being SubSpace of TOP-REAL n st
( b1 is compact & not b1 is empty & b1 is strict )
proof
set A = the non empty compact Subset of (TOP-REAL n);
reconsider T = (TOP-REAL n) | the non empty compact Subset of (TOP-REAL n) as non empty SubSpace of TOP-REAL n ;
T is compact ;
hence ex b1 being SubSpace of TOP-REAL n st
( b1 is compact & not b1 is empty & b1 is strict ) ; ::_thesis: verum
end;
end;
theorem :: JORDAN5A:4
for a, b being Point of (TOP-REAL 2)
for f being Path of a,b
for P being non empty compact SubSpace of TOP-REAL 2
for g being Function of I[01],P st f is one-to-one & g = f & [#] P = rng f holds
g is being_homeomorphism
proof
let a, b be Point of (TOP-REAL 2); ::_thesis: for f being Path of a,b
for P being non empty compact SubSpace of TOP-REAL 2
for g being Function of I[01],P st f is one-to-one & g = f & [#] P = rng f holds
g is being_homeomorphism
let f be Path of a,b; ::_thesis: for P being non empty compact SubSpace of TOP-REAL 2
for g being Function of I[01],P st f is one-to-one & g = f & [#] P = rng f holds
g is being_homeomorphism
let P be non empty compact SubSpace of TOP-REAL 2; ::_thesis: for g being Function of I[01],P st f is one-to-one & g = f & [#] P = rng f holds
g is being_homeomorphism
let g be Function of I[01],P; ::_thesis: ( f is one-to-one & g = f & [#] P = rng f implies g is being_homeomorphism )
A1: dom g = [#] I[01] by FUNCT_2:def_1;
assume ( f is one-to-one & g = f & [#] P = rng f ) ; ::_thesis: g is being_homeomorphism
hence g is being_homeomorphism by A1, COMPTS_1:17, PRE_TOPC:27; ::_thesis: verum
end;
Lm3: for X being Subset of REAL st X is open holds
X in Family_open_set RealSpace
proof
let X be Subset of REAL; ::_thesis: ( X is open implies X in Family_open_set RealSpace )
reconsider V = X as Subset of RealSpace by METRIC_1:def_13;
assume A1: X is open ; ::_thesis: X in Family_open_set RealSpace
for x being Element of RealSpace st x in X holds
ex r being Real st
( r > 0 & Ball (x,r) c= X )
proof
let x be Element of RealSpace; ::_thesis: ( x in X implies ex r being Real st
( r > 0 & Ball (x,r) c= X ) )
reconsider r = x as Real by METRIC_1:def_13;
assume x in X ; ::_thesis: ex r being Real st
( r > 0 & Ball (x,r) c= X )
then consider N being Neighbourhood of r such that
A2: N c= X by A1, RCOMP_1:18;
consider g being real number such that
A3: 0 < g and
A4: N = ].(r - g),(r + g).[ by RCOMP_1:def_6;
reconsider g = g as Real by XREAL_0:def_1;
A5: N c= Ball (x,g)
proof
reconsider r9 = r as Element of RealSpace ;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in N or a in Ball (x,g) )
assume A6: a in N ; ::_thesis: a in Ball (x,g)
then reconsider a9 = a as Real ;
reconsider a1 = a9, r1 = r9 as Element of REAL ;
a9 is Element of REAL ;
then reconsider a99 = a as Element of RealSpace by METRIC_1:def_13;
abs (a9 - r) < g by A4, A6, RCOMP_1:1;
then real_dist . (a9,r) < g by METRIC_1:def_12;
then ( dist (r9,a99) = real_dist . (r,a9) & real_dist . (r1,a1) < g ) by METRIC_1:9, METRIC_1:def_1, METRIC_1:def_13;
hence a in Ball (x,g) by METRIC_1:11; ::_thesis: verum
end;
Ball (x,g) c= N
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Ball (x,g) or a in N )
assume a in Ball (x,g) ; ::_thesis: a in N
then a in { q where q is Element of RealSpace : dist (x,q) < g } by METRIC_1:17;
then consider q being Element of RealSpace such that
A7: q = a and
A8: dist (x,q) < g ;
reconsider a9 = a as Real by A7, METRIC_1:def_13;
reconsider x1 = x, q1 = q as Element of REAL by METRIC_1:def_13;
real_dist . (q1,x1) < g by A8, METRIC_1:def_1, METRIC_1:def_13;
then abs (a9 - r) < g by A7, METRIC_1:def_12;
hence a in N by A4, RCOMP_1:1; ::_thesis: verum
end;
then N = Ball (x,g) by A5, XBOOLE_0:def_10;
hence ex r being Real st
( r > 0 & Ball (x,r) c= X ) by A2, A3; ::_thesis: verum
end;
then V in Family_open_set RealSpace by PCOMPS_1:def_4;
hence X in Family_open_set RealSpace ; ::_thesis: verum
end;
Lm4: for X being Subset of REAL st X in Family_open_set RealSpace holds
X is open
proof
let X be Subset of REAL; ::_thesis: ( X in Family_open_set RealSpace implies X is open )
assume A1: X in Family_open_set RealSpace ; ::_thesis: X is open
for r being real number st r in X holds
ex N being Neighbourhood of r st N c= X
proof
let r be real number ; ::_thesis: ( r in X implies ex N being Neighbourhood of r st N c= X )
assume A2: r in X ; ::_thesis: ex N being Neighbourhood of r st N c= X
reconsider r = r as Real by XREAL_0:def_1;
reconsider x = r as Element of RealSpace by METRIC_1:def_13;
ex N being Neighbourhood of r st N c= X
proof
consider r1 being Real such that
A3: r1 > 0 and
A4: Ball (x,r1) c= X by A1, A2, PCOMPS_1:def_4;
reconsider N1 = Ball (x,r1) as Subset of REAL by METRIC_1:def_13;
ex g being Real st
( 0 < g & Ball (x,r1) = ].(r - g),(r + g).[ )
proof
take g = r1; ::_thesis: ( 0 < g & Ball (x,r1) = ].(r - g),(r + g).[ )
A5: ].(r - g),(r + g).[ c= N1
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ].(r - g),(r + g).[ or a in N1 )
assume A6: a in ].(r - g),(r + g).[ ; ::_thesis: a in N1
then reconsider a9 = a as Real ;
a9 is Element of REAL ;
then reconsider a99 = a, r9 = r as Element of RealSpace by METRIC_1:def_13;
reconsider a1 = a9, r1 = r9 as Element of REAL ;
abs (a9 - r) < g by A6, RCOMP_1:1;
then real_dist . (a9,r) < g by METRIC_1:def_12;
then ( dist (r9,a99) = real_dist . (r,a9) & real_dist . (r1,a1) < g ) by METRIC_1:9, METRIC_1:def_1, METRIC_1:def_13;
hence a in N1 by METRIC_1:11; ::_thesis: verum
end;
N1 c= ].(r - g),(r + g).[
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in N1 or a in ].(r - g),(r + g).[ )
assume a in N1 ; ::_thesis: a in ].(r - g),(r + g).[
then a in { q where q is Element of RealSpace : dist (x,q) < g } by METRIC_1:17;
then consider q being Element of RealSpace such that
A7: q = a and
A8: dist (x,q) < g ;
reconsider a9 = a as Real by A7, METRIC_1:def_13;
reconsider x1 = x, q1 = q as Element of REAL by METRIC_1:def_13;
real_dist . (q1,x1) < g by A8, METRIC_1:def_1, METRIC_1:def_13;
then abs (a9 - r) < g by A7, METRIC_1:def_12;
hence a in ].(r - g),(r + g).[ by RCOMP_1:1; ::_thesis: verum
end;
hence ( 0 < g & Ball (x,r1) = ].(r - g),(r + g).[ ) by A3, A5, XBOOLE_0:def_10; ::_thesis: verum
end;
then reconsider N = N1 as Neighbourhood of r by RCOMP_1:def_6;
take N ; ::_thesis: N c= X
thus N c= X by A4; ::_thesis: verum
end;
hence ex N being Neighbourhood of r st N c= X ; ::_thesis: verum
end;
hence X is open by RCOMP_1:20; ::_thesis: verum
end;
begin
theorem Th5: :: JORDAN5A:5
for X being Subset of REAL holds
( X in Family_open_set RealSpace iff X is open ) by Lm3, Lm4;
theorem Th6: :: JORDAN5A:6
for f being Function of R^1,R^1
for x being Point of R^1
for g being PartFunc of REAL,REAL
for x1 being Real st f is_continuous_at x & f = g & x = x1 holds
g is_continuous_in x1
proof
let f be Function of R^1,R^1; ::_thesis: for x being Point of R^1
for g being PartFunc of REAL,REAL
for x1 being Real st f is_continuous_at x & f = g & x = x1 holds
g is_continuous_in x1
let x be Point of R^1; ::_thesis: for g being PartFunc of REAL,REAL
for x1 being Real st f is_continuous_at x & f = g & x = x1 holds
g is_continuous_in x1
let g be PartFunc of REAL,REAL; ::_thesis: for x1 being Real st f is_continuous_at x & f = g & x = x1 holds
g is_continuous_in x1
let x1 be Real; ::_thesis: ( f is_continuous_at x & f = g & x = x1 implies g is_continuous_in x1 )
assume that
A1: f is_continuous_at x and
A2: f = g and
A3: x = x1 ; ::_thesis: g is_continuous_in x1
for N1 being Neighbourhood of g . x1 ex N being Neighbourhood of x1 st g .: N c= N1
proof
reconsider fx = f . x as Point of R^1 ;
let N1 be Neighbourhood of g . x1; ::_thesis: ex N being Neighbourhood of x1 st g .: N c= N1
reconsider N19 = N1 as Subset of R^1 by TOPMETR:17;
reconsider N2 = N1 as Subset of RealSpace by TOPMETR:12, TOPMETR:17, TOPMETR:def_6;
N2 in Family_open_set RealSpace by Lm3;
then N2 in the topology of (TopSpaceMetr RealSpace) by TOPMETR:12;
then N19 is open by PRE_TOPC:def_2, TOPMETR:def_6;
then reconsider G = N19 as a_neighborhood of fx by A2, A3, CONNSP_2:3, RCOMP_1:16;
consider H being a_neighborhood of x such that
A4: f .: H c= G by A1, TMAP_1:def_2;
consider V being Subset of R^1 such that
A5: V is open and
A6: V c= H and
A7: x in V by CONNSP_2:6;
reconsider V1 = V as Subset of REAL by TOPMETR:17;
V in the topology of R^1 by A5, PRE_TOPC:def_2;
then V in Family_open_set RealSpace by TOPMETR:12, TOPMETR:def_6;
then V1 is open by Lm4;
then consider N being Neighbourhood of x1 such that
A8: N c= V1 by A3, A7, RCOMP_1:18;
N c= H by A6, A8, XBOOLE_1:1;
then g .: N c= g .: H by RELAT_1:123;
hence ex N being Neighbourhood of x1 st g .: N c= N1 by A2, A4, XBOOLE_1:1; ::_thesis: verum
end;
hence g is_continuous_in x1 by FCONT_1:5; ::_thesis: verum
end;
theorem Th7: :: JORDAN5A:7
for f being continuous Function of R^1,R^1
for g being PartFunc of REAL,REAL st f = g holds
g is continuous
proof
let f be continuous Function of R^1,R^1; ::_thesis: for g being PartFunc of REAL,REAL st f = g holds
g is continuous
let g be PartFunc of REAL,REAL; ::_thesis: ( f = g implies g is continuous )
assume A1: f = g ; ::_thesis: g is continuous
for x0 being real number st x0 in dom g holds
g is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom g implies g is_continuous_in x0 )
assume x0 in dom g ; ::_thesis: g is_continuous_in x0
reconsider x0 = x0 as Real by XREAL_0:def_1;
reconsider x1 = x0 as Point of R^1 by TOPMETR:17;
f is_continuous_at x1 by TMAP_1:44;
hence g is_continuous_in x0 by A1, Th6; ::_thesis: verum
end;
hence g is continuous by FCONT_1:def_2; ::_thesis: verum
end;
Lm5: for f being one-to-one continuous Function of R^1,R^1
for g being PartFunc of REAL,REAL holds
( not f = g or g | [.0,1.] is increasing or g | [.0,1.] is decreasing )
proof
let f be one-to-one continuous Function of R^1,R^1; ::_thesis: for g being PartFunc of REAL,REAL holds
( not f = g or g | [.0,1.] is increasing or g | [.0,1.] is decreasing )
let g be PartFunc of REAL,REAL; ::_thesis: ( not f = g or g | [.0,1.] is increasing or g | [.0,1.] is decreasing )
assume A1: f = g ; ::_thesis: ( g | [.0,1.] is increasing or g | [.0,1.] is decreasing )
then ( dom f = REAL & g is continuous ) by Th7, FUNCT_2:def_1, TOPMETR:17;
hence ( g | [.0,1.] is increasing or g | [.0,1.] is decreasing ) by A1, FCONT_2:17; ::_thesis: verum
end;
theorem :: JORDAN5A:8
for f being one-to-one continuous Function of R^1,R^1 holds
( for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy or for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx > fy )
proof
let f be one-to-one continuous Function of R^1,R^1; ::_thesis: ( for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy or for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx > fy )
A1: [.0,1.] /\ (dom f) = [.0,1.] /\ the carrier of R^1 by FUNCT_2:def_1
.= [.0,1.] by BORSUK_1:1, BORSUK_1:40, TOPMETR:20, XBOOLE_1:28 ;
reconsider g = f as PartFunc of REAL,REAL by TOPMETR:17;
percases ( g | [.0,1.] is increasing or g | [.0,1.] is decreasing ) by Lm5;
suppose g | [.0,1.] is increasing ; ::_thesis: ( for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy or for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx > fy )
hence ( for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy or for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx > fy ) by A1, BORSUK_1:40, RFUNCT_2:20; ::_thesis: verum
end;
suppose g | [.0,1.] is decreasing ; ::_thesis: ( for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy or for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx > fy )
hence ( for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy or for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx > fy ) by A1, BORSUK_1:40, RFUNCT_2:21; ::_thesis: verum
end;
end;
end;
theorem Th9: :: JORDAN5A:9
for r, gg, a, b being Real
for x being Element of (Closed-Interval-MSpace (a,b)) st a <= b & x = r & ].(r - gg),(r + gg).[ c= [.a,b.] holds
].(r - gg),(r + gg).[ = Ball (x,gg)
proof
let r, gg, a, b be Real; ::_thesis: for x being Element of (Closed-Interval-MSpace (a,b)) st a <= b & x = r & ].(r - gg),(r + gg).[ c= [.a,b.] holds
].(r - gg),(r + gg).[ = Ball (x,gg)
let x be Element of (Closed-Interval-MSpace (a,b)); ::_thesis: ( a <= b & x = r & ].(r - gg),(r + gg).[ c= [.a,b.] implies ].(r - gg),(r + gg).[ = Ball (x,gg) )
assume that
A1: a <= b and
A2: x = r and
A3: ].(r - gg),(r + gg).[ c= [.a,b.] ; ::_thesis: ].(r - gg),(r + gg).[ = Ball (x,gg)
set g = gg;
set CM = Closed-Interval-MSpace (a,b);
set N1 = Ball (x,gg);
A4: the carrier of (Closed-Interval-MSpace (a,b)) c= the carrier of RealSpace by TOPMETR:def_1;
A5: Ball (x,gg) c= ].(r - gg),(r + gg).[
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in Ball (x,gg) or i in ].(r - gg),(r + gg).[ )
assume i in Ball (x,gg) ; ::_thesis: i in ].(r - gg),(r + gg).[
then i in { q where q is Element of (Closed-Interval-MSpace (a,b)) : dist (x,q) < gg } by METRIC_1:17;
then consider q being Element of (Closed-Interval-MSpace (a,b)) such that
A6: q = i and
A7: dist (x,q) < gg ;
reconsider a9 = i as Real by A4, A6, METRIC_1:def_13, TARSKI:def_3;
reconsider x2 = x, q2 = q as Element of (Closed-Interval-MSpace (a,b)) ;
reconsider x1 = x, q1 = q as Element of REAL by A4, METRIC_1:def_13, TARSKI:def_3;
dist (x2,q2) = the distance of (Closed-Interval-MSpace (a,b)) . (x2,q2) by METRIC_1:def_1
.= real_dist . (x2,q2) by METRIC_1:def_13, TOPMETR:def_1 ;
then real_dist . (q1,x1) < gg by A7, METRIC_1:9;
then abs (a9 - r) < gg by A2, A6, METRIC_1:def_12;
hence i in ].(r - gg),(r + gg).[ by RCOMP_1:1; ::_thesis: verum
end;
].(r - gg),(r + gg).[ c= Ball (x,gg)
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in ].(r - gg),(r + gg).[ or i in Ball (x,gg) )
assume A8: i in ].(r - gg),(r + gg).[ ; ::_thesis: i in Ball (x,gg)
then reconsider a9 = i as Real ;
reconsider a99 = i as Element of (Closed-Interval-MSpace (a,b)) by A1, A3, A8, TOPMETR:10;
abs (a9 - r) < gg by A8, RCOMP_1:1;
then A9: real_dist . (a9,r) < gg by METRIC_1:def_12;
dist (x,a99) = the distance of (Closed-Interval-MSpace (a,b)) . (x,a99) by METRIC_1:def_1
.= real_dist . (x,a99) by METRIC_1:def_13, TOPMETR:def_1 ;
then dist (x,a99) < gg by A2, A9, METRIC_1:9;
hence i in Ball (x,gg) by METRIC_1:11; ::_thesis: verum
end;
hence ].(r - gg),(r + gg).[ = Ball (x,gg) by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th10: :: JORDAN5A:10
for a, b being Real
for X being Subset of REAL st a < b & not a in X & not b in X & X in Family_open_set (Closed-Interval-MSpace (a,b)) holds
X is open
proof
let a, b be Real; ::_thesis: for X being Subset of REAL st a < b & not a in X & not b in X & X in Family_open_set (Closed-Interval-MSpace (a,b)) holds
X is open
let X be Subset of REAL; ::_thesis: ( a < b & not a in X & not b in X & X in Family_open_set (Closed-Interval-MSpace (a,b)) implies X is open )
assume that
A1: a < b and
A2: not a in X and
A3: not b in X ; ::_thesis: ( not X in Family_open_set (Closed-Interval-MSpace (a,b)) or X is open )
assume A4: X in Family_open_set (Closed-Interval-MSpace (a,b)) ; ::_thesis: X is open
then reconsider V = X as Subset of (Closed-Interval-MSpace (a,b)) ;
for r being real number st r in X holds
ex N being Neighbourhood of r st N c= X
proof
let r be real number ; ::_thesis: ( r in X implies ex N being Neighbourhood of r st N c= X )
assume A5: r in X ; ::_thesis: ex N being Neighbourhood of r st N c= X
reconsider r = r as Real by XREAL_0:def_1;
r in V by A5;
then reconsider x = r as Element of (Closed-Interval-MSpace (a,b)) ;
the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by A1, TOPMETR:10;
then x in [.a,b.] ;
then x in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def_1;
then A6: ex r2 being Real st
( r2 = x & a <= r2 & r2 <= b ) ;
A7: r - a <> 0 by A2, A5;
ex N being Neighbourhood of r st N c= X
proof
consider r1 being Real such that
A8: r1 > 0 and
A9: Ball (x,r1) c= X by A4, A5, PCOMPS_1:def_4;
percases ( r <= (a + b) / 2 or r > (a + b) / 2 ) ;
supposeA10: r <= (a + b) / 2 ; ::_thesis: ex N being Neighbourhood of r st N c= X
set gg = min ((r - a),r1);
min ((r - a),r1) > 0
proof
percases ( min ((r - a),r1) = r - a or min ((r - a),r1) = r1 ) by XXREAL_0:15;
suppose min ((r - a),r1) = r - a ; ::_thesis: min ((r - a),r1) > 0
hence min ((r - a),r1) > 0 by A7, A6, XREAL_1:48; ::_thesis: verum
end;
suppose min ((r - a),r1) = r1 ; ::_thesis: min ((r - a),r1) > 0
hence min ((r - a),r1) > 0 by A8; ::_thesis: verum
end;
end;
end;
then reconsider N = ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ as Neighbourhood of r by RCOMP_1:def_6;
take N ; ::_thesis: N c= X
].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ c= [.a,b.]
proof
2 * r <= 2 * ((a + b) / 2) by A10, XREAL_1:64;
then A11: (2 * r) - a <= (a + b) - a by XREAL_1:13;
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ or i in [.a,b.] )
assume i in ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ ; ::_thesis: i in [.a,b.]
then i in { l where l is Real : ( r - (min ((r - a),r1)) < l & l < r + (min ((r - a),r1)) ) } by RCOMP_1:def_2;
then consider j being Real such that
A12: j = i and
A13: r - (min ((r - a),r1)) < j and
A14: j < r + (min ((r - a),r1)) ;
A15: min ((r - a),r1) <= r - a by XXREAL_0:17;
then r + (min ((r - a),r1)) <= r + (r - a) by XREAL_1:6;
then r + (min ((r - a),r1)) <= (a + b) - a by A11, XXREAL_0:2;
then A16: j <= b by A14, XXREAL_0:2;
(min ((r - a),r1)) + a <= r by A15, XREAL_1:19;
then r - (min ((r - a),r1)) >= a by XREAL_1:19;
then a <= j by A13, XXREAL_0:2;
then j in { l where l is Real : ( a <= l & l <= b ) } by A16;
hence i in [.a,b.] by A12, RCOMP_1:def_1; ::_thesis: verum
end;
then ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ = Ball (x,(min ((r - a),r1))) by A1, Th9;
then ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ c= Ball (x,r1) by PCOMPS_1:1, XXREAL_0:17;
hence N c= X by A9, XBOOLE_1:1; ::_thesis: verum
end;
supposeA17: r > (a + b) / 2 ; ::_thesis: ex N being Neighbourhood of r st N c= X
set gg = min ((b - r),r1);
A18: b - r <> 0 by A3, A5;
min ((b - r),r1) > 0
proof
percases ( min ((b - r),r1) = b - r or min ((b - r),r1) = r1 ) by XXREAL_0:15;
suppose min ((b - r),r1) = b - r ; ::_thesis: min ((b - r),r1) > 0
hence min ((b - r),r1) > 0 by A6, A18, XREAL_1:48; ::_thesis: verum
end;
suppose min ((b - r),r1) = r1 ; ::_thesis: min ((b - r),r1) > 0
hence min ((b - r),r1) > 0 by A8; ::_thesis: verum
end;
end;
end;
then reconsider N = ].(r - (min ((b - r),r1))),(r + (min ((b - r),r1))).[ as Neighbourhood of r by RCOMP_1:def_6;
take N ; ::_thesis: N c= X
].(r - (min ((b - r),r1))),(r + (min ((b - r),r1))).[ c= [.a,b.]
proof
2 * r >= ((a + b) / 2) * 2 by A17, XREAL_1:64;
then A19: (2 * r) - b >= (a + b) - b by XREAL_1:13;
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in ].(r - (min ((b - r),r1))),(r + (min ((b - r),r1))).[ or i in [.a,b.] )
assume i in ].(r - (min ((b - r),r1))),(r + (min ((b - r),r1))).[ ; ::_thesis: i in [.a,b.]
then i in { l where l is Real : ( r - (min ((b - r),r1)) < l & l < r + (min ((b - r),r1)) ) } by RCOMP_1:def_2;
then consider j being Real such that
A20: j = i and
A21: r - (min ((b - r),r1)) < j and
A22: j < r + (min ((b - r),r1)) ;
A23: min ((b - r),r1) <= b - r by XXREAL_0:17;
then r + (min ((b - r),r1)) <= b by XREAL_1:19;
then A24: j <= b by A22, XXREAL_0:2;
r - (min ((b - r),r1)) >= r - (b - r) by A23, XREAL_1:13;
then r - (min ((b - r),r1)) >= a by A19, XXREAL_0:2;
then a <= j by A21, XXREAL_0:2;
then j in { l where l is Real : ( a <= l & l <= b ) } by A24;
hence i in [.a,b.] by A20, RCOMP_1:def_1; ::_thesis: verum
end;
then ].(r - (min ((b - r),r1))),(r + (min ((b - r),r1))).[ = Ball (x,(min ((b - r),r1))) by A1, Th9;
then N c= Ball (x,r1) by PCOMPS_1:1, XXREAL_0:17;
hence N c= X by A9, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
hence ex N being Neighbourhood of r st N c= X ; ::_thesis: verum
end;
hence X is open by RCOMP_1:20; ::_thesis: verum
end;
theorem Th11: :: JORDAN5A:11
for X being open Subset of REAL
for a, b being Real st X c= [.a,b.] holds
( not a in X & not b in X )
proof
let X be open Subset of REAL; ::_thesis: for a, b being Real st X c= [.a,b.] holds
( not a in X & not b in X )
let a, b be Real; ::_thesis: ( X c= [.a,b.] implies ( not a in X & not b in X ) )
assume A1: X c= [.a,b.] ; ::_thesis: ( not a in X & not b in X )
assume A2: ( a in X or b in X ) ; ::_thesis: contradiction
percases ( a in X or b in X ) by A2;
suppose a in X ; ::_thesis: contradiction
then consider g being real number such that
A3: 0 < g and
A4: ].(a - g),(a + g).[ c= X by RCOMP_1:19;
g / 2 <> 0 by A3;
then A5: a - (g / 2) < a - 0 by A3, XREAL_1:15;
g > g / 2 by A3, XREAL_1:216;
then A6: a - g < a - (g / 2) by XREAL_1:15;
a + 0 < a + g by A3, XREAL_1:8;
then a - (g / 2) < a + g by A5, XXREAL_0:2;
then a - (g / 2) in { l where l is Real : ( a - g < l & l < a + g ) } by A6;
then A7: a - (g / 2) in ].(a - g),(a + g).[ by RCOMP_1:def_2;
].(a - g),(a + g).[ c= [.a,b.] by A1, A4, XBOOLE_1:1;
then a - (g / 2) in [.a,b.] by A7;
then a - (g / 2) in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def_1;
then ex l being Real st
( l = a - (g / 2) & a <= l & l <= b ) ;
hence contradiction by A5; ::_thesis: verum
end;
suppose b in X ; ::_thesis: contradiction
then consider g being real number such that
A8: 0 < g and
A9: ].(b - g),(b + g).[ c= X by RCOMP_1:19;
g / 2 <> 0 by A8;
then A10: b + (g / 2) > b + 0 by A8, XREAL_1:6;
g > g / 2 by A8, XREAL_1:216;
then A11: b + (g / 2) < b + g by XREAL_1:8;
b - g < b - 0 by A8, XREAL_1:15;
then b - g < b + (g / 2) by A10, XXREAL_0:2;
then b + (g / 2) in { l where l is Real : ( b - g < l & l < b + g ) } by A11;
then A12: b + (g / 2) in ].(b - g),(b + g).[ by RCOMP_1:def_2;
].(b - g),(b + g).[ c= [.a,b.] by A1, A9, XBOOLE_1:1;
then b + (g / 2) in [.a,b.] by A12;
then b + (g / 2) in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def_1;
then ex l being Real st
( l = b + (g / 2) & a <= l & l <= b ) ;
hence contradiction by A10; ::_thesis: verum
end;
end;
end;
theorem Th12: :: JORDAN5A:12
for a, b being Real
for X being Subset of REAL
for V being Subset of (Closed-Interval-MSpace (a,b)) st V = X & X is open holds
V in Family_open_set (Closed-Interval-MSpace (a,b))
proof
let a, b be Real; ::_thesis: for X being Subset of REAL
for V being Subset of (Closed-Interval-MSpace (a,b)) st V = X & X is open holds
V in Family_open_set (Closed-Interval-MSpace (a,b))
let X be Subset of REAL; ::_thesis: for V being Subset of (Closed-Interval-MSpace (a,b)) st V = X & X is open holds
V in Family_open_set (Closed-Interval-MSpace (a,b))
let V be Subset of (Closed-Interval-MSpace (a,b)); ::_thesis: ( V = X & X is open implies V in Family_open_set (Closed-Interval-MSpace (a,b)) )
assume A1: V = X ; ::_thesis: ( not X is open or V in Family_open_set (Closed-Interval-MSpace (a,b)) )
assume A2: X is open ; ::_thesis: V in Family_open_set (Closed-Interval-MSpace (a,b))
for x being Element of (Closed-Interval-MSpace (a,b)) st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V )
proof
let x be Element of (Closed-Interval-MSpace (a,b)); ::_thesis: ( x in V implies ex r being Real st
( r > 0 & Ball (x,r) c= V ) )
assume A3: x in V ; ::_thesis: ex r being Real st
( r > 0 & Ball (x,r) c= V )
then reconsider r = x as Real by A1;
consider N being Neighbourhood of r such that
A4: N c= X by A1, A2, A3, RCOMP_1:18;
consider g being real number such that
A5: 0 < g and
A6: N = ].(r - g),(r + g).[ by RCOMP_1:def_6;
reconsider g = g as Real by XREAL_0:def_1;
A7: Ball (x,g) c= N
proof
let aa be set ; :: according to TARSKI:def_3 ::_thesis: ( not aa in Ball (x,g) or aa in N )
assume aa in Ball (x,g) ; ::_thesis: aa in N
then aa in { q where q is Element of (Closed-Interval-MSpace (a,b)) : dist (x,q) < g } by METRIC_1:17;
then consider q being Element of (Closed-Interval-MSpace (a,b)) such that
A8: q = aa and
A9: dist (x,q) < g ;
A10: ( q in the carrier of (Closed-Interval-MSpace (a,b)) & the carrier of (Closed-Interval-MSpace (a,b)) c= the carrier of RealSpace ) by TOPMETR:def_1;
then reconsider a9 = aa as Real by A8, METRIC_1:def_13;
reconsider x1 = x, q1 = q as Element of REAL by A1, A3, A10, METRIC_1:def_13;
dist (x,q) = the distance of (Closed-Interval-MSpace (a,b)) . (x,q) by METRIC_1:def_1
.= real_dist . (x,q) by METRIC_1:def_13, TOPMETR:def_1 ;
then real_dist . (q1,x1) < g by A9, METRIC_1:9;
then abs (a9 - r) < g by A8, METRIC_1:def_12;
hence aa in N by A6, RCOMP_1:1; ::_thesis: verum
end;
N c= Ball (x,g)
proof
let aa be set ; :: according to TARSKI:def_3 ::_thesis: ( not aa in N or aa in Ball (x,g) )
assume A11: aa in N ; ::_thesis: aa in Ball (x,g)
then reconsider a9 = aa as Real ;
abs (a9 - r) < g by A6, A11, RCOMP_1:1;
then A12: real_dist . (a9,r) < g by METRIC_1:def_12;
aa in X by A4, A11;
then reconsider a99 = aa, r9 = r as Element of (Closed-Interval-MSpace (a,b)) by A1;
dist (r9,a99) = the distance of (Closed-Interval-MSpace (a,b)) . (r9,a99) by METRIC_1:def_1
.= real_dist . (r9,a99) by METRIC_1:def_13, TOPMETR:def_1 ;
then dist (r9,a99) < g by A12, METRIC_1:9;
hence aa in Ball (x,g) by METRIC_1:11; ::_thesis: verum
end;
then N = Ball (x,g) by A7, XBOOLE_0:def_10;
hence ex r being Real st
( r > 0 & Ball (x,r) c= V ) by A1, A4, A5; ::_thesis: verum
end;
hence V in Family_open_set (Closed-Interval-MSpace (a,b)) by PCOMPS_1:def_4; ::_thesis: verum
end;
Lm6: for a, b, c being real number st a <= b holds
( c in the carrier of (Closed-Interval-TSpace (a,b)) iff ( a <= c & c <= b ) )
proof
let a, b, c be real number ; ::_thesis: ( a <= b implies ( c in the carrier of (Closed-Interval-TSpace (a,b)) iff ( a <= c & c <= b ) ) )
A1: c is Real by XREAL_0:def_1;
assume a <= b ; ::_thesis: ( c in the carrier of (Closed-Interval-TSpace (a,b)) iff ( a <= c & c <= b ) )
then A2: the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by TOPMETR:18;
hereby ::_thesis: ( a <= c & c <= b implies c in the carrier of (Closed-Interval-TSpace (a,b)) )
assume c in the carrier of (Closed-Interval-TSpace (a,b)) ; ::_thesis: ( a <= c & c <= b )
then c in { l where l is Real : ( a <= l & l <= b ) } by A2, RCOMP_1:def_1;
then ex c1 being Real st
( c1 = c & a <= c1 & c1 <= b ) ;
hence ( a <= c & c <= b ) ; ::_thesis: verum
end;
assume ( a <= c & c <= b ) ; ::_thesis: c in the carrier of (Closed-Interval-TSpace (a,b))
then c in { l where l is Real : ( a <= l & l <= b ) } by A1;
hence c in the carrier of (Closed-Interval-TSpace (a,b)) by A2, RCOMP_1:def_1; ::_thesis: verum
end;
Lm7: for a, b, c, d being Real
for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
for x being Point of (Closed-Interval-TSpace (a,b))
for g being PartFunc of REAL,REAL
for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g is_continuous_in x1
proof
let a, b, c, d be Real; ::_thesis: for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
for x being Point of (Closed-Interval-TSpace (a,b))
for g being PartFunc of REAL,REAL
for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g is_continuous_in x1
let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ::_thesis: for x being Point of (Closed-Interval-TSpace (a,b))
for g being PartFunc of REAL,REAL
for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g is_continuous_in x1
let x be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: for g being PartFunc of REAL,REAL
for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g is_continuous_in x1
let g be PartFunc of REAL,REAL; ::_thesis: for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g is_continuous_in x1
let x1 be Real; ::_thesis: ( a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 implies g is_continuous_in x1 )
assume that
A1: a < b and
A2: c < d and
A3: f is_continuous_at x and
A4: x <> a and
A5: x <> b and
A6: f . a = c and
A7: f . b = d and
A8: f is one-to-one and
A9: f = g and
A10: x = x1 ; ::_thesis: g is_continuous_in x1
A11: dom f = the carrier of (Closed-Interval-TSpace (a,b)) by FUNCT_2:def_1;
for N1 being Neighbourhood of g . x1 ex N being Neighbourhood of x1 st g .: N c= N1
proof
reconsider fx = f . x as Point of (Closed-Interval-TSpace (c,d)) ;
set Rm = min (((g . x1) - c),(d - (g . x1)));
let N1 be Neighbourhood of g . x1; ::_thesis: ex N being Neighbourhood of x1 st g .: N c= N1
Closed-Interval-TSpace (c,d) = TopSpaceMetr (Closed-Interval-MSpace (c,d)) by TOPMETR:def_7;
then A12: the topology of (Closed-Interval-TSpace (c,d)) = Family_open_set (Closed-Interval-MSpace (c,d)) by TOPMETR:12;
min (((g . x1) - c),(d - (g . x1))) > 0
proof
A13: b in dom f by A1, A11, Lm6;
A14: a in dom f by A1, A11, Lm6;
percases ( min (((g . x1) - c),(d - (g . x1))) = (g . x1) - c or min (((g . x1) - c),(d - (g . x1))) = d - (g . x1) ) by XXREAL_0:15;
supposeA15: min (((g . x1) - c),(d - (g . x1))) = (g . x1) - c ; ::_thesis: min (((g . x1) - c),(d - (g . x1))) > 0
g . x1 in the carrier of (Closed-Interval-TSpace (c,d)) by A9, A10, FUNCT_2:5;
then A16: g . x1 >= c by A2, Lm6;
min (((g . x1) - c),(d - (g . x1))) <> 0 by A4, A6, A8, A9, A10, A11, A14, A15, FUNCT_1:def_4;
hence min (((g . x1) - c),(d - (g . x1))) > 0 by A15, A16, XREAL_1:48; ::_thesis: verum
end;
supposeA17: min (((g . x1) - c),(d - (g . x1))) = d - (g . x1) ; ::_thesis: min (((g . x1) - c),(d - (g . x1))) > 0
g . x1 in the carrier of (Closed-Interval-TSpace (c,d)) by A9, A10, FUNCT_2:5;
then A18: g . x1 <= d by A2, Lm6;
d - (g . x1) <> d - d by A5, A7, A8, A9, A10, A11, A13, FUNCT_1:def_4;
hence min (((g . x1) - c),(d - (g . x1))) > 0 by A17, A18, XREAL_1:48; ::_thesis: verum
end;
end;
end;
then reconsider Wuj = ].((g . x1) - (min (((g . x1) - c),(d - (g . x1))))),((g . x1) + (min (((g . x1) - c),(d - (g . x1))))).[ as Neighbourhood of g . x1 by RCOMP_1:def_6;
consider Ham being Neighbourhood of g . x1 such that
A19: Ham c= N1 and
A20: Ham c= Wuj by RCOMP_1:17;
A21: Wuj c= ].c,d.[
proof
let aa be set ; :: according to TARSKI:def_3 ::_thesis: ( not aa in Wuj or aa in ].c,d.[ )
assume aa in Wuj ; ::_thesis: aa in ].c,d.[
then aa in { l where l is Real : ( (g . x1) - (min (((g . x1) - c),(d - (g . x1)))) < l & l < (g . x1) + (min (((g . x1) - c),(d - (g . x1)))) ) } by RCOMP_1:def_2;
then consider A being Real such that
A22: A = aa and
A23: (g . x1) - (min (((g . x1) - c),(d - (g . x1)))) < A and
A24: A < (g . x1) + (min (((g . x1) - c),(d - (g . x1)))) ;
min (((g . x1) - c),(d - (g . x1))) <= d - (g . x1) by XXREAL_0:17;
then (g . x1) + (min (((g . x1) - c),(d - (g . x1)))) <= (g . x1) + (d - (g . x1)) by XREAL_1:6;
then A25: A < d by A24, XXREAL_0:2;
min (((g . x1) - c),(d - (g . x1))) <= (g . x1) - c by XXREAL_0:17;
then c + (min (((g . x1) - c),(d - (g . x1)))) <= g . x1 by XREAL_1:19;
then c <= (g . x1) - (min (((g . x1) - c),(d - (g . x1)))) by XREAL_1:19;
then c < A by A23, XXREAL_0:2;
then A in { l where l is Real : ( c < l & l < d ) } by A25;
hence aa in ].c,d.[ by A22, RCOMP_1:def_2; ::_thesis: verum
end;
].c,d.[ c= [.c,d.] by XXREAL_1:25;
then A26: Wuj c= [.c,d.] by A21, XBOOLE_1:1;
then Wuj c= the carrier of (Closed-Interval-MSpace (c,d)) by A2, TOPMETR:10;
then reconsider N21 = Ham as Subset of (Closed-Interval-MSpace (c,d)) by A20, XBOOLE_1:1;
the carrier of (Closed-Interval-MSpace (c,d)) = the carrier of (TopSpaceMetr (Closed-Interval-MSpace (c,d))) by TOPMETR:12
.= the carrier of (Closed-Interval-TSpace (c,d)) by TOPMETR:def_7 ;
then reconsider N19 = N21 as Subset of (Closed-Interval-TSpace (c,d)) ;
N21 in Family_open_set (Closed-Interval-MSpace (c,d)) by Th12;
then N19 is open by A12, PRE_TOPC:def_2;
then reconsider G = N19 as a_neighborhood of fx by A9, A10, CONNSP_2:3, RCOMP_1:16;
consider H being a_neighborhood of x such that
A27: f .: H c= G by A3, TMAP_1:def_2;
consider V being Subset of (Closed-Interval-TSpace (a,b)) such that
A28: V is open and
A29: V c= H and
A30: x in V by CONNSP_2:6;
A31: the carrier of (Closed-Interval-MSpace (a,b)) = the carrier of (TopSpaceMetr (Closed-Interval-MSpace (a,b))) by TOPMETR:12
.= the carrier of (Closed-Interval-TSpace (a,b)) by TOPMETR:def_7 ;
then reconsider V2 = V as Subset of (Closed-Interval-MSpace (a,b)) ;
V c= the carrier of (Closed-Interval-MSpace (a,b)) by A31;
then V c= [.a,b.] by A1, TOPMETR:10;
then reconsider V1 = V as Subset of REAL by XBOOLE_1:1;
A32: Ham c= [.c,d.] by A20, A26, XBOOLE_1:1;
A33: ( not a in V1 & not b in V1 )
proof
assume A34: ( a in V1 or b in V1 ) ; ::_thesis: contradiction
percases ( a in V1 or b in V1 ) by A34;
suppose a in V1 ; ::_thesis: contradiction
then f . a in f .: H by A11, A29, FUNCT_1:def_6;
hence contradiction by A6, A32, A27, Th11; ::_thesis: verum
end;
suppose b in V1 ; ::_thesis: contradiction
then f . b in f .: H by A11, A29, FUNCT_1:def_6;
hence contradiction by A7, A32, A27, Th11; ::_thesis: verum
end;
end;
end;
Closed-Interval-TSpace (a,b) = TopSpaceMetr (Closed-Interval-MSpace (a,b)) by TOPMETR:def_7;
then the topology of (Closed-Interval-TSpace (a,b)) = Family_open_set (Closed-Interval-MSpace (a,b)) by TOPMETR:12;
then V2 in Family_open_set (Closed-Interval-MSpace (a,b)) by A28, PRE_TOPC:def_2;
then V1 is open by A1, A33, Th10;
then consider N being Neighbourhood of x1 such that
A35: N c= V1 by A10, A30, RCOMP_1:18;
N c= H by A29, A35, XBOOLE_1:1;
then A36: g .: N c= g .: H by RELAT_1:123;
f .: H c= N1 by A19, A27, XBOOLE_1:1;
hence ex N being Neighbourhood of x1 st g .: N c= N1 by A9, A36, XBOOLE_1:1; ::_thesis: verum
end;
hence g is_continuous_in x1 by FCONT_1:5; ::_thesis: verum
end;
theorem Th13: :: JORDAN5A:13
for a, b, c, d, x1 being Real
for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
for x being Point of (Closed-Interval-TSpace (a,b))
for g being PartFunc of REAL,REAL st a < b & c < d & f is_continuous_at x & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g | [.a,b.] is_continuous_in x1
proof
let a, b, c, d, x1 be Real; ::_thesis: for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
for x being Point of (Closed-Interval-TSpace (a,b))
for g being PartFunc of REAL,REAL st a < b & c < d & f is_continuous_at x & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g | [.a,b.] is_continuous_in x1
let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ::_thesis: for x being Point of (Closed-Interval-TSpace (a,b))
for g being PartFunc of REAL,REAL st a < b & c < d & f is_continuous_at x & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g | [.a,b.] is_continuous_in x1
let x be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: for g being PartFunc of REAL,REAL st a < b & c < d & f is_continuous_at x & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g | [.a,b.] is_continuous_in x1
let g be PartFunc of REAL,REAL; ::_thesis: ( a < b & c < d & f is_continuous_at x & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 implies g | [.a,b.] is_continuous_in x1 )
assume that
A1: a < b and
A2: c < d and
A3: f is_continuous_at x and
A4: f . a = c and
A5: f . b = d and
A6: f is one-to-one and
A7: f = g and
A8: x = x1 ; ::_thesis: g | [.a,b.] is_continuous_in x1
A9: for c being Element of REAL st c in dom g holds
g /. c = g /. c ;
dom g = the carrier of (Closed-Interval-TSpace (a,b)) by A7, FUNCT_2:def_1;
then dom g = [.a,b.] by A1, TOPMETR:18;
then dom g = (dom g) /\ [.a,b.] ;
then A10: g = g | [.a,b.] by A9, PARTFUN2:15;
percases ( x1 = a or x1 = b or ( x1 <> a & x1 <> b ) ) ;
supposeA11: x1 = a ; ::_thesis: g | [.a,b.] is_continuous_in x1
for N1 being Neighbourhood of g . x1 ex N being Neighbourhood of x1 st g .: N c= N1
proof
reconsider f0 = f . a as Point of (Closed-Interval-TSpace (c,d)) by A2, A4, Lm6;
let N1 be Neighbourhood of g . x1; ::_thesis: ex N being Neighbourhood of x1 st g .: N c= N1
reconsider N2 = N1 as Subset of RealSpace by METRIC_1:def_13;
set NN1 = N1 /\ [.c,d.];
N2 in Family_open_set RealSpace by Lm3;
then A12: N2 in the topology of (TopSpaceMetr RealSpace) by TOPMETR:12;
N1 /\ [.c,d.] = N1 /\ the carrier of (Closed-Interval-TSpace (c,d)) by A2, TOPMETR:18;
then reconsider NN = N1 /\ [.c,d.] as Subset of (Closed-Interval-TSpace (c,d)) by XBOOLE_1:17;
N1 /\ [.c,d.] = N1 /\ ([#] (Closed-Interval-TSpace (c,d))) by A2, TOPMETR:18;
then NN in the topology of (Closed-Interval-TSpace (c,d)) by A12, PRE_TOPC:def_4, TOPMETR:def_6;
then A13: NN is open by PRE_TOPC:def_2;
f . a in the carrier of (Closed-Interval-TSpace (c,d)) by A2, A4, Lm6;
then ( g . x1 in N1 & g . x1 in [.c,d.] ) by A2, A7, A11, RCOMP_1:16, TOPMETR:18;
then g . x1 in N1 /\ [.c,d.] by XBOOLE_0:def_4;
then reconsider N19 = NN as a_neighborhood of f0 by A7, A11, A13, CONNSP_2:3;
consider H being a_neighborhood of x such that
A14: f .: H c= N19 by A3, A8, A11, TMAP_1:def_2;
consider H1 being Subset of (Closed-Interval-TSpace (a,b)) such that
A15: H1 is open and
A16: H1 c= H and
A17: x in H1 by CONNSP_2:6;
H1 in the topology of (Closed-Interval-TSpace (a,b)) by A15, PRE_TOPC:def_2;
then consider Q being Subset of R^1 such that
A18: Q in the topology of R^1 and
A19: H1 = Q /\ ([#] (Closed-Interval-TSpace (a,b))) by PRE_TOPC:def_4;
reconsider Q9 = Q as Subset of RealSpace by TOPMETR:12, TOPMETR:def_6;
reconsider Q1 = Q9 as Subset of REAL by METRIC_1:def_13;
Q9 in Family_open_set RealSpace by A18, TOPMETR:12, TOPMETR:def_6;
then A20: Q1 is open by Lm4;
x1 in Q1 by A8, A17, A19, XBOOLE_0:def_4;
then consider N being Neighbourhood of x1 such that
A21: N c= Q1 by A20, RCOMP_1:18;
take N ; ::_thesis: g .: N c= N1
g .: N c= N1
proof
let aa be set ; :: according to TARSKI:def_3 ::_thesis: ( not aa in g .: N or aa in N1 )
assume A22: aa in g .: N ; ::_thesis: aa in N1
then reconsider a9 = aa as Element of REAL ;
consider cc being Element of REAL such that
A23: cc in dom g and
A24: cc in N and
A25: a9 = g . cc by A22, PARTFUN2:59;
cc in the carrier of (Closed-Interval-TSpace (a,b)) by A7, A23, FUNCT_2:def_1;
then cc in H1 by A19, A21, A24, XBOOLE_0:def_4;
then g . cc in f .: H by A7, A16, FUNCT_2:35;
hence aa in N1 by A14, A25, XBOOLE_0:def_4; ::_thesis: verum
end;
hence g .: N c= N1 ; ::_thesis: verum
end;
hence g | [.a,b.] is_continuous_in x1 by A10, FCONT_1:5; ::_thesis: verum
end;
supposeA26: x1 = b ; ::_thesis: g | [.a,b.] is_continuous_in x1
for N1 being Neighbourhood of g . x1 ex N being Neighbourhood of x1 st g .: N c= N1
proof
reconsider f0 = f . b as Point of (Closed-Interval-TSpace (c,d)) by A2, A5, Lm6;
let N1 be Neighbourhood of g . x1; ::_thesis: ex N being Neighbourhood of x1 st g .: N c= N1
reconsider N2 = N1 as Subset of RealSpace by METRIC_1:def_13;
set NN1 = N1 /\ ([#] (Closed-Interval-TSpace (c,d)));
reconsider NN = N1 /\ ([#] (Closed-Interval-TSpace (c,d))) as Subset of (Closed-Interval-TSpace (c,d)) ;
N2 in Family_open_set RealSpace by Lm3;
then N2 in the topology of (TopSpaceMetr RealSpace) by TOPMETR:12;
then NN in the topology of (Closed-Interval-TSpace (c,d)) by PRE_TOPC:def_4, TOPMETR:def_6;
then A27: NN is open by PRE_TOPC:def_2;
( g . x1 in N1 & g . x1 in [#] (Closed-Interval-TSpace (c,d)) ) by A2, A5, A7, A26, Lm6, RCOMP_1:16;
then g . x1 in N1 /\ ([#] (Closed-Interval-TSpace (c,d))) by XBOOLE_0:def_4;
then reconsider N19 = NN as a_neighborhood of f0 by A7, A26, A27, CONNSP_2:3;
consider H being a_neighborhood of x such that
A28: f .: H c= N19 by A3, A8, A26, TMAP_1:def_2;
consider H1 being Subset of (Closed-Interval-TSpace (a,b)) such that
A29: H1 is open and
A30: H1 c= H and
A31: x in H1 by CONNSP_2:6;
H1 in the topology of (Closed-Interval-TSpace (a,b)) by A29, PRE_TOPC:def_2;
then consider Q being Subset of R^1 such that
A32: Q in the topology of R^1 and
A33: H1 = Q /\ ([#] (Closed-Interval-TSpace (a,b))) by PRE_TOPC:def_4;
reconsider Q9 = Q as Subset of RealSpace by TOPMETR:12, TOPMETR:def_6;
reconsider Q1 = Q9 as Subset of REAL by METRIC_1:def_13;
Q9 in Family_open_set RealSpace by A32, TOPMETR:12, TOPMETR:def_6;
then A34: Q1 is open by Lm4;
x1 in Q1 by A8, A31, A33, XBOOLE_0:def_4;
then consider N being Neighbourhood of x1 such that
A35: N c= Q1 by A34, RCOMP_1:18;
take N ; ::_thesis: g .: N c= N1
g .: N c= N1
proof
let aa be set ; :: according to TARSKI:def_3 ::_thesis: ( not aa in g .: N or aa in N1 )
assume A36: aa in g .: N ; ::_thesis: aa in N1
then reconsider a9 = aa as Element of REAL ;
consider cc being Element of REAL such that
A37: cc in dom g and
A38: cc in N and
A39: a9 = g . cc by A36, PARTFUN2:59;
cc in the carrier of (Closed-Interval-TSpace (a,b)) by A7, A37, FUNCT_2:def_1;
then cc in H1 by A33, A35, A38, XBOOLE_0:def_4;
then g . cc in f .: H by A7, A30, FUNCT_2:35;
hence aa in N1 by A28, A39, XBOOLE_0:def_4; ::_thesis: verum
end;
hence g .: N c= N1 ; ::_thesis: verum
end;
hence g | [.a,b.] is_continuous_in x1 by A10, FCONT_1:5; ::_thesis: verum
end;
suppose ( x1 <> a & x1 <> b ) ; ::_thesis: g | [.a,b.] is_continuous_in x1
hence g | [.a,b.] is_continuous_in x1 by A1, A2, A3, A4, A5, A6, A7, A8, A10, Lm7; ::_thesis: verum
end;
end;
end;
theorem Th14: :: JORDAN5A:14
for a, b, c, d being Real
for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
for g being PartFunc of REAL,REAL st f is continuous & f is one-to-one & a < b & c < d & f = g & f . a = c & f . b = d holds
g | [.a,b.] is continuous
proof
let a, b, c, d be Real; ::_thesis: for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
for g being PartFunc of REAL,REAL st f is continuous & f is one-to-one & a < b & c < d & f = g & f . a = c & f . b = d holds
g | [.a,b.] is continuous
let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ::_thesis: for g being PartFunc of REAL,REAL st f is continuous & f is one-to-one & a < b & c < d & f = g & f . a = c & f . b = d holds
g | [.a,b.] is continuous
let g be PartFunc of REAL,REAL; ::_thesis: ( f is continuous & f is one-to-one & a < b & c < d & f = g & f . a = c & f . b = d implies g | [.a,b.] is continuous )
assume that
A1: ( f is continuous & f is one-to-one ) and
A2: a < b and
A3: ( c < d & f = g & f . a = c & f . b = d ) ; ::_thesis: g | [.a,b.] is continuous
for x0 being real number st x0 in dom (g | [.a,b.]) holds
g | [.a,b.] is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom (g | [.a,b.]) implies g | [.a,b.] is_continuous_in x0 )
assume x0 in dom (g | [.a,b.]) ; ::_thesis: g | [.a,b.] is_continuous_in x0
then x0 in [.a,b.] by RELAT_1:57;
then reconsider x1 = x0 as Point of (Closed-Interval-TSpace (a,b)) by A2, TOPMETR:18;
( f is_continuous_at x1 & x0 is Real ) by A1, TMAP_1:44, XREAL_0:def_1;
hence g | [.a,b.] is_continuous_in x0 by A1, A2, A3, Th13; ::_thesis: verum
end;
hence g | [.a,b.] is continuous by FCONT_1:def_2; ::_thesis: verum
end;
begin
theorem Th15: :: JORDAN5A:15
for a, b, c, d being Real
for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) st a < b & c < d & f is continuous & f is one-to-one & f . a = c & f . b = d holds
for x, y being Point of (Closed-Interval-TSpace (a,b))
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy
proof
let a, b, c, d be Real; ::_thesis: for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) st a < b & c < d & f is continuous & f is one-to-one & f . a = c & f . b = d holds
for x, y being Point of (Closed-Interval-TSpace (a,b))
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy
let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ::_thesis: ( a < b & c < d & f is continuous & f is one-to-one & f . a = c & f . b = d implies for x, y being Point of (Closed-Interval-TSpace (a,b))
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy )
assume that
A1: a < b and
A2: c < d and
A3: ( f is continuous & f is one-to-one ) and
A4: ( f . a = c & f . b = d ) ; ::_thesis: for x, y being Point of (Closed-Interval-TSpace (a,b))
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy
A5: [.a,b.] = the carrier of (Closed-Interval-TSpace (a,b)) by A1, TOPMETR:18;
A6: dom f = the carrier of (Closed-Interval-TSpace (a,b)) by FUNCT_2:def_1;
rng f c= REAL by MEMBERED:3;
then reconsider g = f as PartFunc of [.a,b.],REAL by A5, A6, RELSET_1:4;
reconsider g = g as PartFunc of REAL,REAL by A5, A6, RELSET_1:5;
A7: g | [.a,b.] is continuous by A1, A2, A3, A4, Th14;
A8: [.a,b.] /\ (dom f) = [.a,b.] /\ the carrier of (Closed-Interval-TSpace (a,b)) by FUNCT_2:def_1
.= [.a,b.] by A5 ;
percases ( g | [.a,b.] is increasing or g | [.a,b.] is decreasing ) by A1, A3, A8, A7, FCONT_2:17, XBOOLE_1:18;
supposeA9: g | [.a,b.] is increasing ; ::_thesis: for x, y being Point of (Closed-Interval-TSpace (a,b))
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy
for x, y being Point of (Closed-Interval-TSpace (a,b))
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy
proof
let x, y be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy
let p, q, fx, fy be Real; ::_thesis: ( x = p & y = q & p < q & fx = f . x & fy = f . y implies fx < fy )
assume that
A10: x = p and
A11: y = q and
A12: ( p < q & fx = f . x & fy = f . y ) ; ::_thesis: fx < fy
y in the carrier of (Closed-Interval-TSpace (a,b)) ;
then A13: q in [.a,b.] /\ (dom g) by A1, A8, A11, TOPMETR:18;
x in the carrier of (Closed-Interval-TSpace (a,b)) ;
then p in [.a,b.] /\ (dom g) by A1, A8, A10, TOPMETR:18;
hence fx < fy by A9, A10, A11, A12, A13, RFUNCT_2:20; ::_thesis: verum
end;
hence for x, y being Point of (Closed-Interval-TSpace (a,b))
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy ; ::_thesis: verum
end;
supposeA14: g | [.a,b.] is decreasing ; ::_thesis: for x, y being Point of (Closed-Interval-TSpace (a,b))
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy
( a in [.a,b.] /\ (dom g) & b in [.a,b.] /\ (dom g) ) by A1, A5, A8, Lm6;
hence for x, y being Point of (Closed-Interval-TSpace (a,b))
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy by A1, A2, A4, A14, RFUNCT_2:21; ::_thesis: verum
end;
end;
end;
theorem :: JORDAN5A:16
for f being one-to-one continuous Function of I[01],I[01] st f . 0 = 0 & f . 1 = 1 holds
for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy by Th15, TOPMETR:20;
theorem :: JORDAN5A:17
for a, b, c, d being Real
for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
for P being non empty Subset of (Closed-Interval-TSpace (a,b))
for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ holds
f . (lower_bound ([#] PP)) = lower_bound ([#] QQ)
proof
let a, b, c, d be Real; ::_thesis: for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
for P being non empty Subset of (Closed-Interval-TSpace (a,b))
for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ holds
f . (lower_bound ([#] PP)) = lower_bound ([#] QQ)
let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ::_thesis: for P being non empty Subset of (Closed-Interval-TSpace (a,b))
for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ holds
f . (lower_bound ([#] PP)) = lower_bound ([#] QQ)
let P be non empty Subset of (Closed-Interval-TSpace (a,b)); ::_thesis: for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ holds
f . (lower_bound ([#] PP)) = lower_bound ([#] QQ)
let PP, QQ be Subset of R^1; ::_thesis: ( a < b & c < d & PP = P & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ implies f . (lower_bound ([#] PP)) = lower_bound ([#] QQ) )
assume that
A1: ( a < b & c < d ) and
A2: PP = P and
A3: f is continuous and
A4: f is one-to-one and
A5: PP is compact and
A6: ( f . a = c & f . b = d ) and
A7: f .: P = QQ ; ::_thesis: f . (lower_bound ([#] PP)) = lower_bound ([#] QQ)
A8: [#] (Closed-Interval-TSpace (c,d)) = the carrier of (Closed-Interval-TSpace (c,d)) ;
set IT = f . (lower_bound ([#] PP));
A9: [#] PP is real-bounded by A5, WEIERSTR:11;
[#] PP <> {} by A2, WEIERSTR:def_1;
then A10: lower_bound ([#] PP) in [#] PP by A5, A9, RCOMP_1:13, WEIERSTR:12;
then A11: lower_bound ([#] PP) in P by A2, WEIERSTR:def_1;
P c= the carrier of (Closed-Interval-TSpace (a,b)) ;
then A12: [#] PP c= the carrier of (Closed-Interval-TSpace (a,b)) by A2, WEIERSTR:def_1;
then A13: f . (lower_bound ([#] PP)) in the carrier of (Closed-Interval-TSpace (c,d)) by A10, FUNCT_2:5;
A14: [#] R^1 = the carrier of R^1 ;
then A15: the carrier of (Closed-Interval-TSpace (c,d)) c= the carrier of R^1 by A8, PRE_TOPC:def_4;
then reconsider IT = f . (lower_bound ([#] PP)) as Real by A13, TOPMETR:17;
[#] (Closed-Interval-TSpace (a,b)) = the carrier of (Closed-Interval-TSpace (a,b)) ;
then A16: the carrier of (Closed-Interval-TSpace (a,b)) c= the carrier of R^1 by A14, PRE_TOPC:def_4;
A17: for r being real number st r in [#] QQ holds
IT <= r
proof
let r be real number ; ::_thesis: ( r in [#] QQ implies IT <= r )
assume r in [#] QQ ; ::_thesis: IT <= r
then r in f .: P by A7, WEIERSTR:def_1;
then r in f .: ([#] PP) by A2, WEIERSTR:def_1;
then consider x being set such that
A18: x in dom f and
A19: x in [#] PP and
A20: r = f . x by FUNCT_1:def_6;
reconsider x1 = x, x2 = lower_bound ([#] PP) as Point of (Closed-Interval-TSpace (a,b)) by A11, A18;
x1 in the carrier of (Closed-Interval-TSpace (a,b)) ;
then reconsider r1 = x, r2 = x2 as Real by A16, TOPMETR:17;
A21: r2 <= r1 by A9, A19, SEQ_4:def_2;
( f . x1 in the carrier of (Closed-Interval-TSpace (c,d)) & f . x2 in the carrier of (Closed-Interval-TSpace (c,d)) ) ;
then reconsider fr = f . x2, fx = f . x1 as Real by A15, TOPMETR:17;
percases ( r2 <> r1 or r2 = r1 ) ;
suppose r2 <> r1 ; ::_thesis: IT <= r
then r2 < r1 by A21, XXREAL_0:1;
then fr < fx by A1, A3, A4, A6, Th15;
hence IT <= r by A20; ::_thesis: verum
end;
suppose r2 = r1 ; ::_thesis: IT <= r
hence IT <= r by A20; ::_thesis: verum
end;
end;
end;
[#] (Closed-Interval-TSpace (a,b)) = the carrier of (Closed-Interval-TSpace (a,b)) ;
then P is compact by A2, A5, COMPTS_1:2;
then for P1 being Subset of (Closed-Interval-TSpace (c,d)) st P1 = QQ holds
P1 is compact by A3, A7, WEIERSTR:8;
then QQ is compact by A7, A8, COMPTS_1:2;
then A22: [#] QQ is real-bounded by WEIERSTR:11;
lower_bound ([#] PP) in the carrier of (Closed-Interval-TSpace (a,b)) by A12, A10;
then lower_bound ([#] PP) in dom f by FUNCT_2:def_1;
then IT in QQ by A7, A11, FUNCT_1:def_6;
then A23: IT in [#] QQ by WEIERSTR:def_1;
for s being real number st 0 < s holds
ex r being real number st
( r in [#] QQ & r < IT + s )
proof
given s being real number such that A24: 0 < s and
A25: for r being real number holds
( not r in [#] QQ or not r < IT + s ) ; ::_thesis: contradiction
IT + 0 < IT + s by A24, XREAL_1:8;
hence contradiction by A23, A25; ::_thesis: verum
end;
hence f . (lower_bound ([#] PP)) = lower_bound ([#] QQ) by A22, A23, A17, SEQ_4:def_2; ::_thesis: verum
end;
theorem :: JORDAN5A:18
for a, b, c, d being Real
for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
for P, Q being non empty Subset of (Closed-Interval-TSpace (a,b))
for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q holds
f . (upper_bound ([#] PP)) = upper_bound ([#] QQ)
proof
let a, b, c, d be Real; ::_thesis: for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
for P, Q being non empty Subset of (Closed-Interval-TSpace (a,b))
for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q holds
f . (upper_bound ([#] PP)) = upper_bound ([#] QQ)
let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ::_thesis: for P, Q being non empty Subset of (Closed-Interval-TSpace (a,b))
for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q holds
f . (upper_bound ([#] PP)) = upper_bound ([#] QQ)
let P, Q be non empty Subset of (Closed-Interval-TSpace (a,b)); ::_thesis: for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q holds
f . (upper_bound ([#] PP)) = upper_bound ([#] QQ)
let PP, QQ be Subset of R^1; ::_thesis: ( a < b & c < d & PP = P & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q implies f . (upper_bound ([#] PP)) = upper_bound ([#] QQ) )
assume that
A1: ( a < b & c < d ) and
A2: PP = P and
A3: QQ = Q and
A4: ( f is continuous & f is one-to-one ) and
A5: PP is compact and
A6: ( f . a = c & f . b = d ) and
A7: f .: P = Q ; ::_thesis: f . (upper_bound ([#] PP)) = upper_bound ([#] QQ)
A8: [#] (Closed-Interval-TSpace (c,d)) = the carrier of (Closed-Interval-TSpace (c,d)) ;
set IT = f . (upper_bound ([#] PP));
A9: [#] PP is real-bounded by A5, WEIERSTR:11;
[#] PP <> {} by A2, WEIERSTR:def_1;
then A10: upper_bound ([#] PP) in [#] PP by A5, A9, RCOMP_1:12, WEIERSTR:12;
then A11: upper_bound ([#] PP) in P by A2, WEIERSTR:def_1;
P c= the carrier of (Closed-Interval-TSpace (a,b)) ;
then A12: [#] PP c= the carrier of (Closed-Interval-TSpace (a,b)) by A2, WEIERSTR:def_1;
then A13: f . (upper_bound ([#] PP)) in the carrier of (Closed-Interval-TSpace (c,d)) by A10, FUNCT_2:5;
A14: [#] R^1 = the carrier of R^1 ;
then A15: the carrier of (Closed-Interval-TSpace (c,d)) c= the carrier of R^1 by A8, PRE_TOPC:def_4;
then reconsider IT = f . (upper_bound ([#] PP)) as Real by A13, TOPMETR:17;
[#] (Closed-Interval-TSpace (a,b)) = the carrier of (Closed-Interval-TSpace (a,b)) ;
then A16: the carrier of (Closed-Interval-TSpace (a,b)) c= the carrier of R^1 by A14, PRE_TOPC:def_4;
A17: for r being real number st r in [#] QQ holds
IT >= r
proof
let r be real number ; ::_thesis: ( r in [#] QQ implies IT >= r )
assume r in [#] QQ ; ::_thesis: IT >= r
then r in f .: P by A3, A7, WEIERSTR:def_1;
then r in f .: ([#] PP) by A2, WEIERSTR:def_1;
then consider x being set such that
A18: x in dom f and
A19: x in [#] PP and
A20: r = f . x by FUNCT_1:def_6;
reconsider x1 = x, x2 = upper_bound ([#] PP) as Point of (Closed-Interval-TSpace (a,b)) by A11, A18;
x1 in the carrier of (Closed-Interval-TSpace (a,b)) ;
then reconsider r1 = x, r2 = x2 as Real by A16, TOPMETR:17;
A21: r2 >= r1 by A9, A19, SEQ_4:def_1;
( f . x1 in the carrier of (Closed-Interval-TSpace (c,d)) & f . x2 in the carrier of (Closed-Interval-TSpace (c,d)) ) ;
then reconsider fr = f . x2, fx = f . x1 as Real by A15, TOPMETR:17;
percases ( r2 <> r1 or r2 = r1 ) ;
suppose r2 <> r1 ; ::_thesis: IT >= r
then r2 > r1 by A21, XXREAL_0:1;
then fr > fx by A1, A4, A6, Th15;
hence IT >= r by A20; ::_thesis: verum
end;
suppose r2 = r1 ; ::_thesis: IT >= r
hence IT >= r by A20; ::_thesis: verum
end;
end;
end;
[#] (Closed-Interval-TSpace (a,b)) = the carrier of (Closed-Interval-TSpace (a,b)) ;
then P is compact by A2, A5, COMPTS_1:2;
then for P1 being Subset of (Closed-Interval-TSpace (c,d)) st P1 = QQ holds
P1 is compact by A3, A4, A7, WEIERSTR:8;
then QQ is compact by A3, A7, A8, COMPTS_1:2;
then A22: [#] QQ is real-bounded by WEIERSTR:11;
upper_bound ([#] PP) in the carrier of (Closed-Interval-TSpace (a,b)) by A12, A10;
then upper_bound ([#] PP) in dom f by FUNCT_2:def_1;
then IT in QQ by A3, A7, A11, FUNCT_1:def_6;
then A23: IT in [#] QQ by WEIERSTR:def_1;
for s being real number st 0 < s holds
ex r being real number st
( r in [#] QQ & r > IT - s )
proof
given s being real number such that A24: 0 < s and
A25: for r being real number holds
( not r in [#] QQ or not r > IT - s ) ; ::_thesis: contradiction
IT - s < IT - 0 by A24, XREAL_1:15;
hence contradiction by A23, A25; ::_thesis: verum
end;
hence f . (upper_bound ([#] PP)) = upper_bound ([#] QQ) by A22, A23, A17, SEQ_4:def_1; ::_thesis: verum
end;
theorem :: JORDAN5A:19
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.];
a is Real by XREAL_0:def_1;
then A2: a in { l where l is Real : ( a <= l & l <= b ) } by A1;
A3: 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 A4: 0 < s ; ::_thesis: ex r being real number st
( r in [.a,b.] & r < a + s )
A5: a in [.a,b.] by A2, RCOMP_1:def_1;
assume for r being real number st r in [.a,b.] holds
r >= a + s ; ::_thesis: contradiction
hence contradiction by A4, A5, XREAL_1:29; ::_thesis: verum
end;
b is Real by XREAL_0:def_1;
then A6: b in { l1 where l1 is Real : ( a <= l1 & l1 <= b ) } by A1;
A7: 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 A8: 0 < s ; ::_thesis: ex r being real number st
( r in [.a,b.] & b - s < r )
A9: b in [.a,b.] by A6, RCOMP_1:def_1;
assume for r being real number st r in [.a,b.] holds
r <= b - s ; ::_thesis: contradiction
hence contradiction by A8, A9, XREAL_1:44; ::_thesis: verum
end;
A10: 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_1;
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_1;
then ex r1 being Real st
( r1 = r & a <= r1 & r1 <= b ) ;
hence r <= b ; ::_thesis: verum
end;
then A11: [.a,b.] is bounded_above by XXREAL_2:def_10;
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_1;
then ex r1 being Real st
( r1 = r & a <= r1 & r1 <= b ) ;
hence a <= r ; ::_thesis: verum
end;
then A12: [.a,b.] is bounded_below by XXREAL_2:def_9;
A13: 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_1;
then ex r1 being Real st
( r1 = r & a <= r1 & r1 <= b ) ;
hence b >= r ; ::_thesis: verum
end;
a in [.a,b.] by A2, RCOMP_1:def_1;
hence ( lower_bound [.a,b.] = a & upper_bound [.a,b.] = b ) by A12, A11, A10, A3, A13, A7, SEQ_4:def_1, SEQ_4:def_2; ::_thesis: verum
end;
theorem :: JORDAN5A:20
for a, b, c, d, e, f, g, h being Real
for F being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) st a < b & c < d & e < f & a <= e & f <= b & F is being_homeomorphism & F . a = c & F . b = d & g = F . e & h = F . f holds
F .: [.e,f.] = [.g,h.]
proof
let a, b, c, d, e, f, g, h be Real; ::_thesis: for F being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) st a < b & c < d & e < f & a <= e & f <= b & F is being_homeomorphism & F . a = c & F . b = d & g = F . e & h = F . f holds
F .: [.e,f.] = [.g,h.]
let F be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ::_thesis: ( a < b & c < d & e < f & a <= e & f <= b & F is being_homeomorphism & F . a = c & F . b = d & g = F . e & h = F . f implies F .: [.e,f.] = [.g,h.] )
assume that
A1: a < b and
A2: c < d and
A3: e < f and
A4: a <= e and
A5: f <= b and
A6: F is being_homeomorphism and
A7: ( F . a = c & F . b = d ) and
A8: g = F . e and
A9: h = F . f ; ::_thesis: F .: [.e,f.] = [.g,h.]
a <= f by A3, A4, XXREAL_0:2;
then f in { l1 where l1 is Real : ( a <= l1 & l1 <= b ) } by A5;
then A10: f in [.a,b.] by RCOMP_1:def_1;
then f in the carrier of (Closed-Interval-TSpace (a,b)) by A1, TOPMETR:18;
then h in the carrier of (Closed-Interval-TSpace (c,d)) by A9, FUNCT_2:5;
then A11: h in [.c,d.] by A2, TOPMETR:18;
e <= b by A3, A5, XXREAL_0:2;
then e in { l1 where l1 is Real : ( a <= l1 & l1 <= b ) } by A4;
then A12: e in [.a,b.] by RCOMP_1:def_1;
then e in the carrier of (Closed-Interval-TSpace (a,b)) by A1, TOPMETR:18;
then g in the carrier of (Closed-Interval-TSpace (c,d)) by A8, FUNCT_2:5;
then g in [.c,d.] by A2, TOPMETR:18;
then [.g,h.] c= [.c,d.] by A11, XXREAL_2:def_12;
then A13: [.g,h.] c= the carrier of (Closed-Interval-TSpace (c,d)) by A2, TOPMETR:18;
A14: ( F is continuous & F is one-to-one ) by A6, TOPS_2:def_5;
A15: [.g,h.] c= F .: [.e,f.]
proof
let aa be set ; :: according to TARSKI:def_3 ::_thesis: ( not aa in [.g,h.] or aa in F .: [.e,f.] )
A16: F is one-to-one by A6, TOPS_2:def_5;
assume aa in [.g,h.] ; ::_thesis: aa in F .: [.e,f.]
then aa in { l1 where l1 is Real : ( g <= l1 & l1 <= h ) } by RCOMP_1:def_1;
then consider l being Real such that
A17: aa = l and
A18: g <= l and
A19: l <= h ;
A20: rng F = [#] (Closed-Interval-TSpace (c,d)) by A6, TOPS_2:def_5;
l in { l1 where l1 is Real : ( g <= l1 & l1 <= h ) } by A18, A19;
then A21: l in [.g,h.] by RCOMP_1:def_1;
then l in rng F by A13, A20;
then l in dom (F ") by A16, A20, TOPS_2:49;
then (F ") . l in rng (F ") by FUNCT_1:def_3;
then (F ") . l in [#] (Closed-Interval-TSpace (a,b)) ;
then (F ") . l in [.a,b.] by A1, TOPMETR:18;
then reconsider x = (F ") . l as Real ;
F is onto by A20, FUNCT_2:def_3;
then A22: x = (F ") . l by A16, TOPS_2:def_4;
then A23: x in dom F by A13, A16, A20, A21, FUNCT_1:32;
dom F = [#] (Closed-Interval-TSpace (a,b)) by A6, TOPS_2:def_5;
then reconsider e9 = e, f9 = f, x9 = x as Point of (Closed-Interval-TSpace (a,b)) by A1, A12, A10, A13, A16, A20, A21, A22, FUNCT_1:32, TOPMETR:18;
reconsider g9 = F . e9, h9 = F . f9, l9 = F . x9 as Point of (Closed-Interval-TSpace (c,d)) ;
l9 in the carrier of (Closed-Interval-TSpace (c,d)) ;
then l9 in [.c,d.] by A2, TOPMETR:18;
then reconsider gg = g9, hh = h9, ll = l9 as Real by A8, A9;
A24: x <= f
proof
assume x > f ; ::_thesis: contradiction
then ll > hh by A1, A2, A7, A14, Th15;
hence contradiction by A9, A13, A19, A16, A20, A21, A22, FUNCT_1:32; ::_thesis: verum
end;
e <= x
proof
assume e > x ; ::_thesis: contradiction
then gg > ll by A1, A2, A7, A14, Th15;
hence contradiction by A8, A13, A18, A16, A20, A21, A22, FUNCT_1:32; ::_thesis: verum
end;
then x in { l1 where l1 is Real : ( e <= l1 & l1 <= f ) } by A24;
then A25: x in [.e,f.] by RCOMP_1:def_1;
aa = F . x by A13, A17, A16, A20, A21, A22, FUNCT_1:32;
hence aa in F .: [.e,f.] by A23, A25, FUNCT_1:def_6; ::_thesis: verum
end;
F .: [.e,f.] c= [.g,h.]
proof
let aa be set ; :: according to TARSKI:def_3 ::_thesis: ( not aa in F .: [.e,f.] or aa in [.g,h.] )
assume aa in F .: [.e,f.] ; ::_thesis: aa in [.g,h.]
then consider x being set such that
A26: x in dom F and
A27: x in [.e,f.] and
A28: aa = F . x by FUNCT_1:def_6;
x in { l where l is Real : ( e <= l & l <= f ) } by A27, RCOMP_1:def_1;
then consider x9 being Real such that
A29: x9 = x and
A30: e <= x9 and
A31: x9 <= f ;
F . x9 in rng F by A26, A29, FUNCT_1:def_3;
then F . x9 in [#] (Closed-Interval-TSpace (c,d)) ;
then A32: F . x9 in [.c,d.] by A2, TOPMETR:18;
then reconsider Fx = F . x9 as Real ;
reconsider e1 = e, f1 = f, x1 = x9 as Point of (Closed-Interval-TSpace (a,b)) by A1, A12, A10, A26, A29, TOPMETR:18;
reconsider gg = F . e1, hh = F . f1, FFx = F . x1 as Real by A8, A9, A32;
A33: Fx <= h
proof
percases ( f = x or f <> x ) ;
suppose f = x ; ::_thesis: Fx <= h
hence Fx <= h by A9, A29; ::_thesis: verum
end;
suppose f <> x ; ::_thesis: Fx <= h
then f > x9 by A29, A31, XXREAL_0:1;
then hh > FFx by A1, A2, A7, A14, Th15;
hence Fx <= h by A9; ::_thesis: verum
end;
end;
end;
g <= Fx
proof
percases ( e = x or e <> x ) ;
suppose e = x ; ::_thesis: g <= Fx
hence g <= Fx by A8, A29; ::_thesis: verum
end;
suppose e <> x ; ::_thesis: g <= Fx
then e < x9 by A29, A30, XXREAL_0:1;
then gg < FFx by A1, A2, A7, A14, Th15;
hence g <= Fx by A8; ::_thesis: verum
end;
end;
end;
then Fx in { l1 where l1 is Real : ( g <= l1 & l1 <= h ) } by A33;
hence aa in [.g,h.] by A28, A29, RCOMP_1:def_1; ::_thesis: verum
end;
hence F .: [.e,f.] = [.g,h.] by A15, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: JORDAN5A:21
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
ex EX being Point of (TOP-REAL 2) st
( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) ) )
proof
let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
ex EX being Point of (TOP-REAL 2) st
( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) ) )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 implies ex EX being Point of (TOP-REAL 2) st
( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) ) ) )
assume that
A1: P meets Q and
A2: P /\ Q is closed and
A3: P is_an_arc_of p1,p2 ; ::_thesis: ex EX being Point of (TOP-REAL 2) st
( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) ) )
P /\ Q <> {} by A1, XBOOLE_0:def_7;
then reconsider P = P as non empty Subset of (TOP-REAL 2) ;
consider f being Function of I[01],((TOP-REAL 2) | P) such that
A4: f is being_homeomorphism and
A5: ( f . 0 = p1 & f . 1 = p2 ) by A3, TOPREAL1:def_1;
A6: f is one-to-one by A4, TOPS_2:def_5;
[#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5;
then reconsider PQ = P /\ Q as non empty Subset of ((TOP-REAL 2) | P) by A1, XBOOLE_0:def_7, XBOOLE_1:17;
reconsider P1 = P, Q1 = Q as non empty Subset of (TOP-REAL 2) by A1, A2, XBOOLE_0:def_7;
consider OO being set such that
A7: OO in PQ by XBOOLE_0:def_1;
reconsider PP = P as Subset of (TOP-REAL 2) ;
PP is compact by A3, Th1;
then A8: P /\ Q is compact by A2, COMPTS_1:9, XBOOLE_1:17;
PQ <> {} ((TOP-REAL 2) | P) ;
then reconsider PQ1 = P /\ Q as non empty Subset of ((TOP-REAL 2) | P1) ;
(TOP-REAL 2) | (P1 /\ Q1) = ((TOP-REAL 2) | P1) | PQ1 by GOBOARD9:2;
then A9: PQ is compact by A8, COMPTS_1:3;
set g = f " ;
reconsider g1 = f " as Function ;
A10: rng f = [#] ((TOP-REAL 2) | P) by A4, TOPS_2:def_5;
[#] I[01] c= [#] R^1 by PRE_TOPC:def_4;
then reconsider GPQ = (f ") .: PQ as Subset of R^1 by XBOOLE_1:1;
f " is continuous by A4, TOPS_2:def_5;
then ( (f ") .: PQ c= [#] I[01] & ( for P being Subset of I[01] st P = GPQ holds
P is compact ) ) by A9, WEIERSTR:8;
then A11: GPQ is compact by COMPTS_1:2;
then A12: [#] GPQ is real-bounded by WEIERSTR:11;
set Ex = lower_bound ([#] GPQ);
reconsider f1 = f as Function ;
take f . (lower_bound ([#] GPQ)) ; ::_thesis: ( f . (lower_bound ([#] GPQ)) is Point of (TOP-REAL 2) & f . (lower_bound ([#] GPQ)) in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = f . (lower_bound ([#] GPQ)) & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) ) )
A13: dom (f ") = the carrier of ((TOP-REAL 2) | P) by FUNCT_2:def_1;
dom (f ") = the carrier of ((TOP-REAL 2) | P) by FUNCT_2:def_1;
then (f ") . OO in GPQ by A7, FUNCT_1:def_6;
then [#] GPQ <> {} by WEIERSTR:def_1;
then lower_bound ([#] GPQ) in [#] GPQ by A11, A12, RCOMP_1:13, WEIERSTR:12;
then A14: lower_bound ([#] GPQ) in GPQ by WEIERSTR:def_1;
then A15: lower_bound ([#] GPQ) <= 1 by BORSUK_1:43;
A16: dom f = the carrier of I[01] by FUNCT_2:def_1;
A17: for t being Real st 0 <= t & t < lower_bound ([#] GPQ) holds
not f . t in Q
proof
let t be Real; ::_thesis: ( 0 <= t & t < lower_bound ([#] GPQ) implies not f . t in Q )
assume that
A18: 0 <= t and
A19: t < lower_bound ([#] GPQ) ; ::_thesis: not f . t in Q
A20: t <= 1 by A15, A19, XXREAL_0:2;
then t in the carrier of I[01] by A18, BORSUK_1:43;
then f . t in the carrier of ((TOP-REAL 2) | P) by FUNCT_2:5;
then A21: f . t in P by PRE_TOPC:8;
f is onto by A10, FUNCT_2:def_3;
then A22: f " = f1 " by A6, TOPS_2:def_4;
assume f . t in Q ; ::_thesis: contradiction
then f . t in PQ by A21, XBOOLE_0:def_4;
then A23: (f ") . (f . t) in GPQ by A13, FUNCT_1:def_6;
t in dom f by A16, A18, A20, BORSUK_1:43;
then (f ") . (f . t) = t by A6, A22, FUNCT_1:34;
then t in [#] GPQ by A23, WEIERSTR:def_1;
hence contradiction by A12, A19, SEQ_4:def_2; ::_thesis: verum
end;
A24: f " is one-to-one by A10, A6, TOPS_2:50;
f " is being_homeomorphism by A4, TOPS_2:56;
then rng (f ") = [#] I[01] by TOPS_2:def_5;
then f " is onto by FUNCT_2:def_3;
then (f ") " = g1 " by A24, TOPS_2:def_4;
then A25: f = g1 " by A10, A6, TOPS_2:51;
A26: ( ex pq being set st
( pq in dom (f ") & pq in PQ & lower_bound ([#] GPQ) = (f ") . pq ) & 0 <= lower_bound ([#] GPQ) ) by A14, BORSUK_1:43, FUNCT_1:def_6;
f " is one-to-one by A10, A6, TOPS_2:50;
hence ( f . (lower_bound ([#] GPQ)) is Point of (TOP-REAL 2) & f . (lower_bound ([#] GPQ)) in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = f . (lower_bound ([#] GPQ)) & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) ) ) by A4, A5, A25, A26, A15, A17, FUNCT_1:34; ::_thesis: verum
end;
theorem :: JORDAN5A:22
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
ex EX being Point of (TOP-REAL 2) st
( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) ) )
proof
let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
ex EX being Point of (TOP-REAL 2) st
( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) ) )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 implies ex EX being Point of (TOP-REAL 2) st
( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) ) ) )
assume that
A1: P meets Q and
A2: P /\ Q is closed and
A3: P is_an_arc_of p1,p2 ; ::_thesis: ex EX being Point of (TOP-REAL 2) st
( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) ) )
P /\ Q <> {} by A1, XBOOLE_0:def_7;
then reconsider P = P as non empty Subset of (TOP-REAL 2) ;
consider f being Function of I[01],((TOP-REAL 2) | P) such that
A4: f is being_homeomorphism and
A5: ( f . 0 = p1 & f . 1 = p2 ) by A3, TOPREAL1:def_1;
A6: f is one-to-one by A4, TOPS_2:def_5;
[#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5;
then reconsider PQ = P /\ Q as non empty Subset of ((TOP-REAL 2) | P) by A1, XBOOLE_0:def_7, XBOOLE_1:17;
reconsider P1 = P, Q1 = Q as non empty Subset of (TOP-REAL 2) by A1, A2, XBOOLE_0:def_7;
consider OO being set such that
A7: OO in PQ by XBOOLE_0:def_1;
reconsider PP = P as Subset of (TOP-REAL 2) ;
PP is compact by A3, Th1;
then A8: P /\ Q is compact by A2, COMPTS_1:9, XBOOLE_1:17;
PQ <> {} ((TOP-REAL 2) | P) ;
then reconsider PQ1 = P /\ Q as non empty Subset of ((TOP-REAL 2) | P1) ;
(TOP-REAL 2) | (P1 /\ Q1) = ((TOP-REAL 2) | P1) | PQ1 by GOBOARD9:2;
then A9: PQ is compact by A8, COMPTS_1:3;
set g = f " ;
reconsider g1 = f " as Function ;
A10: rng f = [#] ((TOP-REAL 2) | P) by A4, TOPS_2:def_5;
A11: f " is one-to-one by A10, A6, TOPS_2:50;
f " is being_homeomorphism by A4, TOPS_2:56;
then rng (f ") = [#] I[01] by TOPS_2:def_5;
then f " is onto by FUNCT_2:def_3;
then (f ") " = g1 " by A11, TOPS_2:def_4;
then A12: f = g1 " by A10, A6, TOPS_2:51;
[#] I[01] c= [#] R^1 by PRE_TOPC:def_4;
then reconsider GPQ = (f ") .: PQ as Subset of R^1 by XBOOLE_1:1;
f " is continuous by A4, TOPS_2:def_5;
then ( (f ") .: PQ c= [#] I[01] & ( for P being Subset of I[01] st P = GPQ holds
P is compact ) ) by A9, WEIERSTR:8;
then A13: GPQ is compact by COMPTS_1:2;
then A14: [#] GPQ is real-bounded by WEIERSTR:11;
set Ex = upper_bound ([#] GPQ);
reconsider f1 = f as Function ;
take f . (upper_bound ([#] GPQ)) ; ::_thesis: ( f . (upper_bound ([#] GPQ)) is Point of (TOP-REAL 2) & f . (upper_bound ([#] GPQ)) in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = f . (upper_bound ([#] GPQ)) & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) ) )
A15: dom (f ") = the carrier of ((TOP-REAL 2) | P) by FUNCT_2:def_1;
dom (f ") = the carrier of ((TOP-REAL 2) | P) by FUNCT_2:def_1;
then (f ") . OO in GPQ by A7, FUNCT_1:def_6;
then [#] GPQ <> {} by WEIERSTR:def_1;
then upper_bound ([#] GPQ) in [#] GPQ by A13, A14, RCOMP_1:12, WEIERSTR:12;
then A16: upper_bound ([#] GPQ) in GPQ by WEIERSTR:def_1;
then A17: 0 <= upper_bound ([#] GPQ) by BORSUK_1:43;
A18: dom f = the carrier of I[01] by FUNCT_2:def_1;
A19: for t being Real st 1 >= t & t > upper_bound ([#] GPQ) holds
not f . t in Q
proof
let t be Real; ::_thesis: ( 1 >= t & t > upper_bound ([#] GPQ) implies not f . t in Q )
assume that
A20: 1 >= t and
A21: t > upper_bound ([#] GPQ) ; ::_thesis: not f . t in Q
t in the carrier of I[01] by A17, A20, A21, BORSUK_1:43;
then f . t in the carrier of ((TOP-REAL 2) | P) by FUNCT_2:5;
then A22: f . t in P by PRE_TOPC:8;
f is onto by A10, FUNCT_2:def_3;
then A23: f " = f1 " by A6, TOPS_2:def_4;
assume f . t in Q ; ::_thesis: contradiction
then f . t in PQ by A22, XBOOLE_0:def_4;
then A24: (f ") . (f . t) in GPQ by A15, FUNCT_1:def_6;
t in dom f by A18, A17, A20, A21, BORSUK_1:43;
then (f ") . (f . t) = t by A6, A23, FUNCT_1:34;
then t in [#] GPQ by A24, WEIERSTR:def_1;
hence contradiction by A14, A21, SEQ_4:def_1; ::_thesis: verum
end;
A25: ( ex pq being set st
( pq in dom (f ") & pq in PQ & upper_bound ([#] GPQ) = (f ") . pq ) & upper_bound ([#] GPQ) <= 1 ) by A16, BORSUK_1:43, FUNCT_1:def_6;
f " is one-to-one by A10, A6, TOPS_2:50;
hence ( f . (upper_bound ([#] GPQ)) is Point of (TOP-REAL 2) & f . (upper_bound ([#] GPQ)) in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = f . (upper_bound ([#] GPQ)) & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) ) ) by A4, A5, A12, A17, A25, A19, FUNCT_1:34; ::_thesis: verum
end;
registration
cluster non empty V45() V46() V47() finite real-bounded for Element of K6(REAL);
existence
ex b1 being Subset of REAL st
( not b1 is empty & b1 is finite & b1 is real-bounded )
proof
reconsider a = {0} as finite Subset of REAL ;
take a ; ::_thesis: ( not a is empty & a is finite & a is real-bounded )
thus ( not a is empty & a is finite & a is real-bounded ) ; ::_thesis: verum
end;
end;
Lm8: R^1 = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #)
by PCOMPS_1:def_5, TOPMETR:def_6;
theorem Th23: :: JORDAN5A:23
for A being Subset of REAL
for B being Subset of R^1 st A = B holds
( A is closed iff B is closed )
proof
let A be Subset of REAL; ::_thesis: for B being Subset of R^1 st A = B holds
( A is closed iff B is closed )
let B be Subset of R^1; ::_thesis: ( A = B implies ( A is closed iff B is closed ) )
assume A1: A = B ; ::_thesis: ( A is closed iff B is closed )
thus ( A is closed implies B is closed ) ::_thesis: ( B is closed implies A is closed )
proof
assume A is closed ; ::_thesis: B is closed
then (A `) ` is closed ;
then A ` is open by RCOMP_1:def_5;
then A ` in the topology of R^1 by Lm8, Th5;
hence ([#] R^1) \ B is open by PRE_TOPC:def_2, A1, TOPMETR:17; :: according to PRE_TOPC:def_3 ::_thesis: verum
end;
assume B is closed ; ::_thesis: A is closed
then B ` in the topology of R^1 by PRE_TOPC:def_2;
then A ` is open by A1, Lm8, Th5, TOPMETR:17;
then (A `) ` is closed by RCOMP_1:def_5;
hence A is closed ; ::_thesis: verum
end;
theorem :: JORDAN5A:24
for A being Subset of REAL
for B being Subset of R^1 st A = B holds
Cl A = Cl B
proof
let A be Subset of REAL; ::_thesis: for B being Subset of R^1 st A = B holds
Cl A = Cl B
let B be Subset of R^1; ::_thesis: ( A = B implies Cl A = Cl B )
assume A1: A = B ; ::_thesis: Cl A = Cl B
thus Cl A c= Cl B :: according to XBOOLE_0:def_10 ::_thesis: Cl B c= Cl A
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cl A or a in Cl B )
assume A2: a in Cl A ; ::_thesis: a in Cl B
for G being Subset of R^1 st G is open & a in G holds
B meets G
proof
let G be Subset of R^1; ::_thesis: ( G is open & a in G implies B meets G )
assume that
A3: G is open and
A4: a in G ; ::_thesis: B meets G
reconsider H = G as Subset of REAL by TOPMETR:17;
G in Family_open_set RealSpace by A3, Lm8, PRE_TOPC:def_2;
then H is open by Th5;
then not A /\ H is empty by A2, A4, MEASURE6:63;
hence B meets G by A1, XBOOLE_0:def_7; ::_thesis: verum
end;
hence a in Cl B by A2, PRE_TOPC:def_7, TOPMETR:17; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cl B or a in Cl A )
assume A5: a in Cl B ; ::_thesis: a in Cl A
for O being open Subset of REAL st a in O holds
not O /\ A is empty
proof
let O be open Subset of REAL; ::_thesis: ( a in O implies not O /\ A is empty )
assume A6: a in O ; ::_thesis: not O /\ A is empty
reconsider P = O as Subset of R^1 by TOPMETR:17;
P in Family_open_set RealSpace by Th5;
then P is open by Lm8, PRE_TOPC:def_2;
then P meets B by A5, A6, PRE_TOPC:def_7;
hence not O /\ A is empty by A1, XBOOLE_0:def_7; ::_thesis: verum
end;
hence a in Cl A by A5, MEASURE6:63, TOPMETR:17; ::_thesis: verum
end;
registration
let a, b be real number ;
clusterK289(a,b) -> compact for Subset of REAL;
coherence
for b1 being Subset of REAL st b1 = [.a,b.] holds
b1 is compact by RCOMP_1:6;
end;
theorem Th25: :: JORDAN5A:25
for A being Subset of REAL
for B being Subset of R^1 st A = B holds
( A is compact iff B is compact )
proof
let A be Subset of REAL; ::_thesis: for B being Subset of R^1 st A = B holds
( A is compact iff B is compact )
let B be Subset of R^1; ::_thesis: ( A = B implies ( A is compact iff B is compact ) )
assume A1: A = B ; ::_thesis: ( A is compact iff B is compact )
thus ( A is compact implies B is compact ) ::_thesis: ( B is compact implies A is compact )
proof
assume A2: A is compact ; ::_thesis: B is compact
percases ( A = {} or A <> {} ) ;
suppose A = {} ; ::_thesis: B is compact
then reconsider C = B as empty Subset of R^1 by A1;
C is compact ;
hence B is compact ; ::_thesis: verum
end;
suppose A <> {} ; ::_thesis: B is compact
then reconsider A = A as non empty real-bounded Subset of REAL by A2, RCOMP_1:10;
reconsider i = inf A, s = sup A as real number ;
reconsider X = [.i,s.] as Subset of R^1 by TOPMETR:17;
A3: i <= s by XXREAL_2:40;
then A4: Closed-Interval-TSpace (i,s) = R^1 | X by TOPMETR:19;
A5: B is closed by A1, A2, Th23;
A6: X <> {} by A3, XXREAL_1:30;
A7: B c= X by A1, XXREAL_2:69;
Closed-Interval-TSpace (i,s) is compact by HEINE:4, A3;
then X is compact by A6, A4, COMPTS_1:3;
hence B is compact by A5, COMPTS_1:9, A7; ::_thesis: verum
end;
end;
end;
assume B is compact ; ::_thesis: A is compact
then [#] B is compact by WEIERSTR:13;
hence A is compact by A1, WEIERSTR:def_1; ::_thesis: verum
end;
registration
cluster finite -> compact for Element of K6(REAL);
coherence
for b1 being Subset of REAL st b1 is finite holds
b1 is compact by Th25, TOPMETR:17;
end;
theorem :: JORDAN5A:26
for a, b being real number holds
( a <> b iff Cl ].a,b.[ = [.a,b.] )
proof
let a, b be real number ; ::_thesis: ( a <> b iff Cl ].a,b.[ = [.a,b.] )
thus ( a <> b implies Cl ].a,b.[ = [.a,b.] ) ::_thesis: ( Cl ].a,b.[ = [.a,b.] implies a <> b )
proof
reconsider a1 = a, b1 = b as Real by XREAL_0:def_1;
assume A1: a <> b ; ::_thesis: Cl ].a,b.[ = [.a,b.]
percases ( a > b or a < b ) by A1, XXREAL_0:1;
supposeA2: a > b ; ::_thesis: Cl ].a,b.[ = [.a,b.]
hence Cl ].a,b.[ = {} by MEASURE6:60, XXREAL_1:28
.= [.a,b.] by A2, XXREAL_1:29 ;
::_thesis: verum
end;
supposeA3: a < b ; ::_thesis: Cl ].a,b.[ = [.a,b.]
then A4: (a1 + b1) / 2 < b1 by XREAL_1:226;
thus Cl ].a,b.[ c= [.a,b.] by MEASURE6:57, XXREAL_1:25; :: according to XBOOLE_0:def_10 ::_thesis: [.a,b.] c= Cl ].a,b.[
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in [.a,b.] or p in Cl ].a,b.[ )
A5: ].a,b.[ = { w where w is Real : ( a < w & w < b ) } by RCOMP_1:def_2;
assume A6: p in [.a,b.] ; ::_thesis: p in Cl ].a,b.[
[.a,b.] = { w where w is Real : ( a <= w & w <= b ) } by RCOMP_1:def_1;
then consider r being Real such that
A7: p = r and
A8: a <= r and
A9: r <= b by A6;
a1 < (a1 + b1) / 2 by A3, XREAL_1:226;
then A10: (a1 + b1) / 2 in ].a1,b1.[ by A5, A4;
now__::_thesis:_(_(_a_<_r_&_r_<_b_&_p_in_Cl_].a,b.[_)_or_(_a_=_r_&_p_in_Cl_].a,b.[_)_or_(_b_=_r_&_p_in_Cl_].a,b.[_)_)
percases ( ( a < r & r < b ) or a = r or b = r ) by A8, A9, XXREAL_0:1;
caseA11: ( a < r & r < b ) ; ::_thesis: p in Cl ].a,b.[
A12: ].a,b.[ c= Cl ].a,b.[ by MEASURE6:58;
r in ].a,b.[ by A5, A11;
hence p in Cl ].a,b.[ by A7, A12; ::_thesis: verum
end;
caseA13: a = r ; ::_thesis: p in Cl ].a,b.[
for O being open Subset of REAL st a in O holds
not O /\ ].a,b.[ is empty
proof
let O be open Subset of REAL; ::_thesis: ( a in O implies not O /\ ].a,b.[ is empty )
assume a in O ; ::_thesis: not O /\ ].a,b.[ is empty
then consider g being real number such that
A14: 0 < g and
A15: ].(a - g),(a + g).[ c= O by RCOMP_1:19;
reconsider g = g as Real by XREAL_0:def_1;
A16: a - g < a - 0 by A14, XREAL_1:15;
A17: ].(a - g),(a + g).[ = { w where w is Real : ( a - g < w & w < a + g ) } by RCOMP_1:def_2;
percases ( a + g < b or a + g >= b ) ;
supposeA18: a + g < b ; ::_thesis: not O /\ ].a,b.[ is empty
A19: a + 0 < a + g by A14, XREAL_1:6;
then A20: a1 < (a1 + (a1 + g)) / 2 by XREAL_1:226;
A21: (a1 + (a1 + g)) / 2 < a1 + g by A19, XREAL_1:226;
then (a + (a + g)) / 2 < b by A18, XXREAL_0:2;
then A22: (a1 + (a1 + g)) / 2 in ].a1,b1.[ by A5, A20;
a - g < (a + (a + g)) / 2 by A16, A20, XXREAL_0:2;
then (a1 + (a1 + g)) / 2 in ].(a1 - g),(a1 + g).[ by A17, A21;
hence not O /\ ].a,b.[ is empty by A15, A22, XBOOLE_0:def_4; ::_thesis: verum
end;
supposeA23: a + g >= b ; ::_thesis: not O /\ ].a,b.[ is empty
(a1 + b1) / 2 < b1 by A3, XREAL_1:226;
then A24: (a + b) / 2 < a + g by A23, XXREAL_0:2;
a1 < (a1 + b1) / 2 by A3, XREAL_1:226;
then a - g < (a + b) / 2 by A16, XXREAL_0:2;
then (a1 + b1) / 2 in ].(a1 - g),(a1 + g).[ by A17, A24;
hence not O /\ ].a,b.[ is empty by A10, A15, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
hence p in Cl ].a,b.[ by A7, A13, MEASURE6:63; ::_thesis: verum
end;
caseA25: b = r ; ::_thesis: p in Cl ].a,b.[
for O being open Subset of REAL st b in O holds
not O /\ ].a,b.[ is empty
proof
let O be open Subset of REAL; ::_thesis: ( b in O implies not O /\ ].a,b.[ is empty )
assume b in O ; ::_thesis: not O /\ ].a,b.[ is empty
then consider g being real number such that
A26: 0 < g and
A27: ].(b - g),(b + g).[ c= O by RCOMP_1:19;
reconsider g = g as Real by XREAL_0:def_1;
A28: b - g < b - 0 by A26, XREAL_1:15;
A29: b + 0 < b + g by A26, XREAL_1:6;
A30: ].(b - g),(b + g).[ = { w where w is Real : ( b - g < w & w < b + g ) } by RCOMP_1:def_2;
percases ( b - g > a or b - g <= a ) ;
supposeA31: b - g > a ; ::_thesis: not O /\ ].a,b.[ is empty
A32: (b1 + (b1 - g)) / 2 < b1 by A28, XREAL_1:226;
A33: b1 - g < (b1 + (b1 - g)) / 2 by A28, XREAL_1:226;
then a < (b + (b - g)) / 2 by A31, XXREAL_0:2;
then A34: (b1 + (b1 - g)) / 2 in ].a1,b1.[ by A5, A32;
(b1 + (b1 - g)) / 2 < b1 by A28, XREAL_1:226;
then (b + (b - g)) / 2 < b + g by A29, XXREAL_0:2;
then (b1 + (b1 - g)) / 2 in ].(b1 - g),(b1 + g).[ by A30, A33;
hence not O /\ ].a,b.[ is empty by A27, A34, XBOOLE_0:def_4; ::_thesis: verum
end;
supposeA35: b - g <= a ; ::_thesis: not O /\ ].a,b.[ is empty
(a1 + b1) / 2 < b1 by A3, XREAL_1:226;
then A36: (a + b) / 2 < b + g by A29, XXREAL_0:2;
a1 < (a1 + b1) / 2 by A3, XREAL_1:226;
then b - g < (a + b) / 2 by A35, XXREAL_0:2;
then (a1 + b1) / 2 in ].(b1 - g),(b1 + g).[ by A30, A36;
hence not O /\ ].a,b.[ is empty by A10, A27, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
hence p in Cl ].a,b.[ by A7, A25, MEASURE6:63; ::_thesis: verum
end;
end;
end;
hence p in Cl ].a,b.[ ; ::_thesis: verum
end;
end;
end;
assume that
A37: Cl ].a,b.[ = [.a,b.] and
A38: a = b ; ::_thesis: contradiction
[.a,b.] = {a} by A38, XXREAL_1:17;
hence contradiction by A37, A38, MEASURE6:60, XXREAL_1:28; ::_thesis: verum
end;
theorem :: JORDAN5A:27
for T being TopStruct
for f being RealMap of T
for g being Function of T,R^1 st f = g holds
( f is continuous iff g is continuous )
proof
let T be TopStruct ; ::_thesis: for f being RealMap of T
for g being Function of T,R^1 st f = g holds
( f is continuous iff g is continuous )
let f be RealMap of T; ::_thesis: for g being Function of T,R^1 st f = g holds
( f is continuous iff g is continuous )
let g be Function of T,R^1; ::_thesis: ( f = g implies ( f is continuous iff g is continuous ) )
assume A1: f = g ; ::_thesis: ( f is continuous iff g is continuous )
thus ( f is continuous implies g is continuous ) ::_thesis: ( g is continuous implies f is continuous )
proof
assume A2: for Y being Subset of REAL st Y is closed holds
f " Y is closed ; :: according to PSCOMP_1:def_3 ::_thesis: g is continuous
let P be Subset of R^1; :: according to PRE_TOPC:def_6 ::_thesis: ( not P is closed or g " P is closed )
assume A3: P is closed ; ::_thesis: g " P is closed
reconsider R = P as Subset of REAL by TOPMETR:17;
R is closed by A3, Th23;
hence g " P is closed by A1, A2; ::_thesis: verum
end;
assume A4: for Y being Subset of R^1 st Y is closed holds
g " Y is closed ; :: according to PRE_TOPC:def_6 ::_thesis: f is continuous
let P be Subset of REAL; :: according to PSCOMP_1:def_3 ::_thesis: ( not P is closed or f " P is closed )
assume A5: P is closed ; ::_thesis: f " P is closed
reconsider R = P as Subset of R^1 by TOPMETR:17;
R is closed by A5, Th23;
hence f " P is closed by A1, A4; ::_thesis: verum
end;