let n be Nat; :: thesis: for e being positive Real
for g being continuous Function of I[01],(TOP-REAL n) ex h being FinSequence of REAL st
( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Nat
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds
diameter W < e ) )
1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then A1: 1 in [.0,1.] by RCOMP_1:def 1;
{1} c= [.0,1.] by A1, TARSKI:def 1;
then A2: [.0,1.] \/ {1} = [.0,1.] by XBOOLE_1:12;
Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:def 7;
then A3: the carrier of I[01] = the carrier of (Closed-Interval-MSpace (0,1)) by TOPMETR:12, TOPMETR:20
.= [.0,1.] by TOPMETR:10 ;
let e be positive Real; :: thesis: for g being continuous Function of I[01],(TOP-REAL n) ex h being FinSequence of REAL st
( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Nat
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds
diameter W < e ) )
let g be continuous Function of I[01],(TOP-REAL n); :: thesis: ex h being FinSequence of REAL st
( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Nat
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds
diameter W < e ) )
reconsider e = e as positive Real ;
A4: n in NAT by ORDINAL1:def 12;
then reconsider f = g as Function of (Closed-Interval-MSpace (0,1)),(Euclid n) by UNIFORM1:10;
A5: e / 2 < e by XREAL_1:216;
A6: e / 2 > 0 by XREAL_1:215;
f is uniformly_continuous by UNIFORM1:8, A4;
then consider s1 being Real such that
A7: 0 < s1 and
A8: for u1, u2 being Element of (Closed-Interval-MSpace (0,1)) st dist (u1,u2) < s1 holds
dist ((f /. u1),(f /. u2)) < e / 2 by A6, UNIFORM1:def 1;
set s = min (s1,(1 / 2));
defpred S1[ Nat, object ] means $2 = ((min (s1,(1 / 2))) / 2) * ($1 - 1);
A9: 0 <= min (s1,(1 / 2)) by A7, XXREAL_0:20;
then reconsider j = [/(2 / (min (s1,(1 / 2))))\] as Nat by INT_1:53;
A10: 2 / (min (s1,(1 / 2))) <= j by INT_1:def 7;
A11: min (s1,(1 / 2)) <= s1 by XXREAL_0:17;
A12: for u1, u2 being Element of (Closed-Interval-MSpace (0,1)) st dist (u1,u2) < min (s1,(1 / 2)) holds
dist ((f /. u1),(f /. u2)) < e / 2
proof
let u1, u2 be Element of (Closed-Interval-MSpace (0,1)); :: thesis: ( dist (u1,u2) < min (s1,(1 / 2)) implies dist ((f /. u1),(f /. u2)) < e / 2 )
assume dist (u1,u2) < min (s1,(1 / 2)) ; :: thesis: dist ((f /. u1),(f /. u2)) < e / 2
then dist (u1,u2) < s1 by A11, XXREAL_0:2;
hence dist ((f /. u1),(f /. u2)) < e / 2 by A8; :: thesis: verum
end;
A13: 2 / (min (s1,(1 / 2))) <= [/(2 / (min (s1,(1 / 2))))\] by INT_1:def 7;
then (2 / (min (s1,(1 / 2)))) - j <= 0 by XREAL_1:47;
then 1 + ((2 / (min (s1,(1 / 2)))) - j) <= 1 + 0 by XREAL_1:6;
then A14: ((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - j)) <= ((min (s1,(1 / 2))) / 2) * 1 by A9, XREAL_1:64;
A15: for k being Nat st k in Seg j holds
ex x being object st S1[k,x] ;
consider p being FinSequence such that
A16: ( dom p = Seg j & ( for k being Nat st k in Seg j holds
S1[k,p . k] ) ) from FINSEQ_1:sch 1(A15);
 A17: Seg (len p) = Seg j by A16, FINSEQ_1:def 3;
rng (p ^ <*1*>) c= REAL
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (p ^ <*1*>) or y in REAL )
A18: len (p ^ <*1*>) = (len p) + 1 by FINSEQ_2:16;
assume y in rng (p ^ <*1*>) ; :: thesis: y in REAL
then consider x being object such that
A19: x in dom (p ^ <*1*>) and
A20: y = (p ^ <*1*>) . x by FUNCT_1:def 3;
reconsider nx = x as Nat by A19;
A21: dom (p ^ <*1*>) = Seg (len (p ^ <*1*>)) by FINSEQ_1:def 3;
then A22: 1 <= nx by A19, FINSEQ_1:1;
A23: 1 <= nx by A19, A21, FINSEQ_1:1;
A24: nx <= len (p ^ <*1*>) by A19, A21, FINSEQ_1:1;
per cases ( nx < (len p) + 1 or nx >= (len p) + 1 ) ;
end;
end;
then reconsider h1 = p ^ <*1*> as FinSequence of REAL by FINSEQ_1:def 4;
A28: len h1 = (len p) + 1 by FINSEQ_2:16;
j in NAT by ORDINAL1:def 12;
then A29: len p = j by A16, FINSEQ_1:def 3;
A30: min (s1,(1 / 2)) <> 0 by A7, XXREAL_0:15;
then 2 / (min (s1,(1 / 2))) >= 2 / (1 / 2) by A9, XREAL_1:118, XXREAL_0:17;
then 4 <= j by A10, XXREAL_0:2;
then A31: 4 + 1 <= (len p) + 1 by A29, XREAL_1:6;
A32: (min (s1,(1 / 2))) / 2 > 0 by A9, A30, XREAL_1:215;
A33: for i being Nat
for r1, r2 being Real st 1 <= i & i < len p & r1 = p . i & r2 = p . (i + 1) holds
( r1 < r2 & r2 - r1 = (min (s1,(1 / 2))) / 2 )
proof
let i be Nat; :: thesis: for r1, r2 being Real st 1 <= i & i < len p & r1 = p . i & r2 = p . (i + 1) holds
( r1 < r2 & r2 - r1 = (min (s1,(1 / 2))) / 2 )
let r1, r2 be Real; :: thesis: ( 1 <= i & i < len p & r1 = p . i & r2 = p . (i + 1) implies ( r1 < r2 & r2 - r1 = (min (s1,(1 / 2))) / 2 ) )
assume that
A34: ( 1 <= i & i < len p ) and
A35: r1 = p . i and
A36: r2 = p . (i + 1) ; :: thesis: ( r1 < r2 & r2 - r1 = (min (s1,(1 / 2))) / 2 )
( 1 < i + 1 & i + 1 <= len p ) by A34, NAT_1:13;
then i + 1 in Seg j by A17, FINSEQ_1:1;
then A37: r2 = ((min (s1,(1 / 2))) / 2) * ((i + 1) - 1) by A16, A36;
i < i + 1 by NAT_1:13;
then A38: i - 1 < (i + 1) - 1 by XREAL_1:9;
A39: i in Seg j by A17, A34, FINSEQ_1:1;
then r1 = ((min (s1,(1 / 2))) / 2) * (i - 1) by A16, A35;
hence r1 < r2 by A32, A37, A38, XREAL_1:68; :: thesis: r2 - r1 = (min (s1,(1 / 2))) / 2
r2 - r1 = (((min (s1,(1 / 2))) / 2) * i) - (((min (s1,(1 / 2))) / 2) * (i - 1)) by A16, A35, A39, A37;
hence r2 - r1 = (min (s1,(1 / 2))) / 2 ; :: thesis: verum
end;
0 < min (s1,(1 / 2)) by A7, A30, XXREAL_0:20;
then 0 < j by A13, XREAL_1:139;
then A40: 0 + 1 <= j by NAT_1:13;
then 1 in Seg j by FINSEQ_1:1;
then p . 1 = ((min (s1,(1 / 2))) / 2) * (1 - 1) by A16
.= 0 ;
then A41: h1 . 1 = 0 by A40, A29, Lm2;
2 * (min (s1,(1 / 2))) <> 0 by A7, XXREAL_0:15;
then A42: ( ((min (s1,(1 / 2))) / 2) * (2 / (min (s1,(1 / 2)))) = (2 * (min (s1,(1 / 2)))) / (2 * (min (s1,(1 / 2)))) & (2 * (min (s1,(1 / 2)))) / (2 * (min (s1,(1 / 2)))) = 1 ) by XCMPLX_1:60, XCMPLX_1:76;
then A43: 1 - (((min (s1,(1 / 2))) / 2) * (j - 1)) = ((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - [/(2 / (min (s1,(1 / 2))))\])) ;
A44: for r1 being Real st r1 = p . (len p) holds
1 - r1 <= (min (s1,(1 / 2))) / 2 by A40, A29, FINSEQ_1:1, A14, A16, A43;
A45: for i being Nat st 1 <= i & i < len h1 holds
(h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2
proof
let i be Nat; :: thesis: ( 1 <= i & i < len h1 implies (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 )
assume that
A46: 1 <= i and
A47: i < len h1 ; :: thesis: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2
A48: i + 1 <= len h1 by A47, NAT_1:13;
A49: i <= len p by A28, A47, NAT_1:13;
A50: 1 < i + 1 by A46, NAT_1:13;
per cases ( i < len p or i >= len p ) ;
suppose A51: i < len p ; :: thesis: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2
then i + 1 <= len p by NAT_1:13;
then A52: h1 . (i + 1) = p . (i + 1) by A50, FINSEQ_1:64;
A53: h1 . i = p . i by A46, A51, FINSEQ_1:64;
( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A46, A47, A48, A50, FINSEQ_4:15;
hence (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 by A33, A46, A51, A53, A52; :: thesis: verum
end;
suppose i >= len p ; :: thesis: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2
then A54: i = len p by A49, XXREAL_0:1;
A55: h1 /. i = h1 . i by A46, A47, FINSEQ_4:15
.= p . i by A46, A49, FINSEQ_1:64 ;
h1 /. (i + 1) = h1 . (i + 1) by A48, A50, FINSEQ_4:15
.= 1 by A54, FINSEQ_1:42 ;
hence (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 by A44, A54, A55; :: thesis: verum
end;
end;
end;
[/(2 / (min (s1,(1 / 2))))\] < (2 / (min (s1,(1 / 2)))) + 1 by INT_1:def 7;
then [/(2 / (min (s1,(1 / 2))))\] - 1 < ((2 / (min (s1,(1 / 2)))) + 1) - 1 by XREAL_1:9;
then A56: ((min (s1,(1 / 2))) / 2) * (j - 1) < ((min (s1,(1 / 2))) / 2) * (2 / (min (s1,(1 / 2)))) by A32, XREAL_1:68;
A57: for i being Nat
for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds
r1 < 1
proof
let i be Nat; :: thesis: for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds
r1 < 1
let r1 be Real; :: thesis: ( 1 <= i & i <= len p & r1 = p . i implies r1 < 1 )
assume that
A58: 1 <= i and
A59: i <= len p and
A60: r1 = p . i ; :: thesis: r1 < 1
i - 1 <= j - 1 by A29, A59, XREAL_1:9;
then A61: ((min (s1,(1 / 2))) / 2) * (i - 1) <= ((min (s1,(1 / 2))) / 2) * (j - 1) by A9, XREAL_1:64;
i in Seg j by A17, A58, A59, FINSEQ_1:1;
then r1 = ((min (s1,(1 / 2))) / 2) * (i - 1) by A16, A60;
hence r1 < 1 by A56, A42, A61, XXREAL_0:2; :: thesis: verum
end;
A62: for i being Nat st 1 <= i & i < len h1 holds
h1 /. i < h1 /. (i + 1)
proof
let i be Nat; :: thesis: ( 1 <= i & i < len h1 implies h1 /. i < h1 /. (i + 1) )
assume that
A63: 1 <= i and
A64: i < len h1 ; :: thesis: h1 /. i < h1 /. (i + 1)
A65: i + 1 <= len h1 by A64, NAT_1:13;
A66: 1 < i + 1 by A63, NAT_1:13;
A67: i <= len p by A28, A64, NAT_1:13;
per cases ( i < len p or i >= len p ) ;
suppose A68: i < len p ; :: thesis: h1 /. i < h1 /. (i + 1)
then i + 1 <= len p by NAT_1:13;
then A69: h1 . (i + 1) = p . (i + 1) by A66, FINSEQ_1:64;
A70: h1 . i = p . i by A63, A68, FINSEQ_1:64;
( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A63, A64, A65, A66, FINSEQ_4:15;
hence h1 /. i < h1 /. (i + 1) by A33, A63, A68, A70, A69; :: thesis: verum
end;
suppose i >= len p ; :: thesis: h1 /. i < h1 /. (i + 1)
then A71: i = len p by A67, XXREAL_0:1;
A72: h1 /. (i + 1) = h1 . (i + 1) by A65, A66, FINSEQ_4:15
.= 1 by A71, FINSEQ_1:42 ;
h1 /. i = h1 . i by A63, A64, FINSEQ_4:15
.= p . i by A63, A67, FINSEQ_1:64 ;
hence h1 /. i < h1 /. (i + 1) by A57, A63, A67, A72; :: thesis: verum
end;
end;
end;
A73: dom g = the carrier of I[01] by FUNCT_2:def 1;
A74: for i being Nat
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g .: Q holds
diameter W < e
proof
let i be Nat; :: thesis: for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g .: Q holds
diameter W < e
let Q be Subset of I[01]; :: thesis: for W being Subset of (Euclid n) st 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g .: Q holds
diameter W < e
let W be Subset of (Euclid n); :: thesis: ( 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g .: Q implies diameter W < e )
assume that
A75: ( 1 <= i & i < len h1 ) and
A76: Q = [.(h1 /. i),(h1 /. (i + 1)).] and
A77: W = g .: Q ; :: thesis: diameter W < e
h1 /. i < h1 /. (i + 1) by A62, A75;
then A78: Q <> {} by A76, XXREAL_1:1;
A79: for x, y being Point of (Euclid n) st x in W & y in W holds
dist (x,y) <= e / 2
proof
let x, y be Point of (Euclid n); :: thesis: ( x in W & y in W implies dist (x,y) <= e / 2 )
assume that
A80: x in W and
A81: y in W ; :: thesis: dist (x,y) <= e / 2
consider x3 being object such that
A82: x3 in dom g and
A83: x3 in Q and
A84: x = g . x3 by A77, A80, FUNCT_1:def 6;
reconsider x3 = x3 as Element of (Closed-Interval-MSpace (0,1)) by A82, Lm1, TOPMETR:12;
reconsider r3 = x3 as Real by A83;
A85: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 by A45, A75;
consider y3 being object such that
A86: y3 in dom g and
A87: y3 in Q and
A88: y = g . y3 by A77, A81, FUNCT_1:def 6;
reconsider y3 = y3 as Element of (Closed-Interval-MSpace (0,1)) by A86, Lm1, TOPMETR:12;
reconsider s3 = y3 as Real by A87;
A89: ( f . x3 = f /. x3 & f . y3 = f /. y3 ) ;
|.(r3 - s3).| <= (h1 /. (i + 1)) - (h1 /. i) by A76, A83, A87, UNIFORM1:12;
then |.(r3 - s3).| <= (min (s1,(1 / 2))) / 2 by A85, XXREAL_0:2;
then A90: dist (x3,y3) <= (min (s1,(1 / 2))) / 2 by HEINE:1;
(min (s1,(1 / 2))) / 2 < min (s1,(1 / 2)) by A9, A30, XREAL_1:216;
then dist (x3,y3) < min (s1,(1 / 2)) by A90, XXREAL_0:2;
hence dist (x,y) <= e / 2 by A12, A84, A88, A89; :: thesis: verum
end;
then W is bounded by A6, TBSP_1:def 7;
then diameter W <= e / 2 by A73, A77, A78, A79, TBSP_1:def 8;
hence diameter W < e by A5, XXREAL_0:2; :: thesis: verum
end;
A91: rng p c= [.0,1.]
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in [.0,1.] )
assume y in rng p ; :: thesis: y in [.0,1.]
then consider x being object such that
A92: x in dom p and
A93: y = p . x by FUNCT_1:def 3;
reconsider nx = x as Nat by A92;
A94: p . nx = ((min (s1,(1 / 2))) / 2) * (nx - 1) by A16, A92;
then reconsider ry = p . nx as Real ;
A95: x in Seg (len p) by A92, FINSEQ_1:def 3;
then A96: 1 <= nx by FINSEQ_1:1;
then A97: nx - 1 >= 1 - 1 by XREAL_1:9;
nx <= len p by A95, FINSEQ_1:1;
then ry < 1 by A57, A96;
then y in { rs where rs is Real : ( 0 <= rs & rs <= 1 ) } by A9, A93, A94, A97;
hence y in [.0,1.] by RCOMP_1:def 1; :: thesis: verum
end;
rng <*1*> = {1} by FINSEQ_1:38;
then rng h1 = (rng p) \/ {1} by FINSEQ_1:31;
then A98: rng h1 c= [.0,1.] \/ {1} by A91, XBOOLE_1:13;
h1 . (len h1) = 1 by A28, FINSEQ_1:42;
hence ex h being FinSequence of REAL st
( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Nat
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds
diameter W < e ) ) by A28, A31, A41, A2, A98, A3, A62, A74, Lm3; :: thesis: verum