let n be Nat; :: thesis: for F being Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) st ( for x being Point of (TOP-REAL n)
for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) holds
F is continuous
set I = the carrier of I[01];
let F be Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n); :: thesis: ( ( for x being Point of (TOP-REAL n)
for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) implies F is continuous )
assume A1: for x being Point of (TOP-REAL n)
for i being Point of I[01] holds F . (x,i) = (1 - i) * x ; :: thesis: F is continuous
A2: REAL n = n -tuples_on REAL by EUCLID:def 1;
A3: [#] I[01] = the carrier of I[01] ;
for p being Point of [:(TOP-REAL n),I[01]:]
for V being Subset of (TOP-REAL n) st F . p in V & V is open holds
ex W being Subset of [:(TOP-REAL n),I[01]:] st
( p in W & W is open & F .: W c= V )
proof
let p be Point of [:(TOP-REAL n),I[01]:]; :: thesis: for V being Subset of (TOP-REAL n) st F . p in V & V is open holds
ex W being Subset of [:(TOP-REAL n),I[01]:] st
( p in W & W is open & F .: W c= V )
let V be Subset of (TOP-REAL n); :: thesis: ( F . p in V & V is open implies ex W being Subset of [:(TOP-REAL n),I[01]:] st
( p in W & W is open & F .: W c= V ) )
reconsider ep = F . p as Point of (Euclid n) by TOPREAL3:8;
consider x being Point of (TOP-REAL n), i being Point of I[01] such that
A4: p = [x,i] by BORSUK_1:10;
A5: ep = F . (x,i) by A4
.= (1 - i) * x by A1 ;
reconsider fx = x as Element of REAL n by EUCLID:22;
reconsider lx = x as Point of (Euclid n) by TOPREAL3:8;
assume ( F . p in V & V is open ) ; :: thesis: ex W being Subset of [:(TOP-REAL n),I[01]:] st
( p in W & W is open & F .: W c= V )
then F . p in Int V by TOPS_1:23;
then consider r0 being Real such that
A6: r0 > 0 and
A7: Ball (ep,r0) c= V by GOBOARD6:5;
A8: r0 / 2 > 0 by A6, XREAL_1:139;
per cases ( 1 - i > 0 or 1 - i <= 0 ) ;
suppose A9: 1 - i > 0 ; :: thesis: ex W being Subset of [:(TOP-REAL n),I[01]:] st
( p in W & W is open & F .: W c= V )
then - (- (1 - i)) > - 0 ;
then - (1 - i) < 0 ;
then A10: (i - 1) * ((2 * (1 - i)) * |.fx.|) <= 0 by A9;
set t = ((2 * (1 - i)) * |.fx.|) + r0;
set c = ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0);
i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) = ((i * (((2 * (1 - i)) * |.fx.|) + r0)) / (((2 * (1 - i)) * |.fx.|) + r0)) + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by A6, A9, XCMPLX_1:89
.= ((i * (((2 * (1 - i)) * |.fx.|) + r0)) + ((1 - i) * r0)) / (((2 * (1 - i)) * |.fx.|) + r0) by XCMPLX_1:62
.= ((((i * 2) * (1 - i)) * |.fx.|) + r0) / (((2 * (1 - i)) * |.fx.|) + r0) ;
then (i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))) - 1 = (((((i * 2) * (1 - i)) * |.fx.|) + r0) / (((2 * (1 - i)) * |.fx.|) + r0)) - ((((2 * (1 - i)) * |.fx.|) + r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by A6, A9, XCMPLX_1:60
.= (((((i * 2) * (1 - i)) * |.fx.|) + r0) - (((2 * (1 - i)) * |.fx.|) + r0)) / (((2 * (1 - i)) * |.fx.|) + r0) by XCMPLX_1:120 ;
then A11: ((i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))) - 1) + 1 <= 0 + 1 by A6, A9, A10, XREAL_1:7;
set X1 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[;
set X2 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ /\ the carrier of I[01];
reconsider X2 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ /\ the carrier of I[01] as Subset of I[01] by XBOOLE_1:17;
reconsider B = Ball (lx,((r0 / 2) / (1 - i))) as Subset of (TOP-REAL n) by TOPREAL3:8;
take W = [:B,X2:]; :: thesis: ( p in W & W is open & F .: W c= V )
0 < (1 - i) * r0 by A6, A9, XREAL_1:129;
then A12: 0 < ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0) by A6, A9, XREAL_1:139;
then |.(i - i).| < ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0) by ABSVALUE:def 1;
then i in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ by RCOMP_1:1;
then A13: i in X2 by XBOOLE_0:def 4;
0 <= i by BORSUK_1:43;
then A14: i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) is Point of I[01] by A6, A9, A11, BORSUK_1:43;
A15: now :: thesis: X2 is open
per cases ( 0 <= i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) or i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) < 0 ) ;
suppose A16: 0 <= i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) ; :: thesis: X2 is open
].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ c= the carrier of I[01]
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ or a in the carrier of I[01] )
assume A17: a in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ ; :: thesis: a in the carrier of I[01]
then reconsider a = a as Real ;
a < i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by A17, XXREAL_1:4;
then A18: a < 1 by A11, XXREAL_0:2;
0 < a by A16, A17, XXREAL_1:4;
hence a in the carrier of I[01] by A18, BORSUK_1:43; :: thesis: verum
end;
then reconsider X1 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ as Subset of I[01] ;
now :: thesis: X1 is open
per cases ( i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) <= i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) or i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) > i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) ) ;
suppose i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) <= i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) ; :: thesis: X1 is open
then i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) <= 1 by A11, XXREAL_0:2;
then i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) is Point of I[01] by A16, BORSUK_1:43;
hence X1 is open by A14, BORSUK_4:45; :: thesis: verum
end;
suppose i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) > i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) ; :: thesis: X1 is open
then X1 = {} I[01] by XXREAL_1:28;
hence X1 is open ; :: thesis: verum
end;
end;
end;
hence X2 is open by A3; :: thesis: verum
end;
suppose A19: i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) < 0 ; :: thesis: X2 is open
X2 = [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ c= X2
let a be object ; :: thesis: ( a in X2 implies a in [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ )
assume A20: a in X2 ; :: thesis: a in [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[
then reconsider b = a as Real ;
a in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ by A20, XBOOLE_0:def 4;
then A21: b < i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by XXREAL_1:4;
0 <= b by A20, BORSUK_1:43;
hence a in [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ by A21, XXREAL_1:3; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ or a in X2 )
assume A22: a in [.0,(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ ; :: thesis: a in X2
then reconsider b = a as Real ;
A23: 0 <= b by A22, XXREAL_1:3;
A24: b < i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by A22, XXREAL_1:3;
then b <= 1 by A11, XXREAL_0:2;
then A25: a in the carrier of I[01] by A23, BORSUK_1:40, XXREAL_1:1;
a in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ by A19, A24, A23, XXREAL_1:4;
hence a in X2 by A25, XBOOLE_0:def 4; :: thesis: verum
end;
hence X2 is open by A14, Th5; :: thesis: verum
end;
end;
end;
x in B by A8, A9, GOBOARD6:1, XREAL_1:139;
hence p in W by A4, A13, ZFMISC_1:87; :: thesis: ( W is open & F .: W c= V )
B is open by GOBOARD6:3;
hence W is open by A15, BORSUK_1:6; :: thesis: F .: W c= V
A26: 0 < 2 * (1 - i) by A9, XREAL_1:129;
F .: W c= Ball (ep,r0)
proof
let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in F .: W or m in Ball (ep,r0) )
assume m in F .: W ; :: thesis: m in Ball (ep,r0)
then consider z being object such that
A27: z in dom F and
A28: z in W and
A29: F . z = m by FUNCT_1:def 6;
reconsider z = z as Point of [:(TOP-REAL n),I[01]:] by A27;
consider y being Point of (TOP-REAL n), j being Point of I[01] such that
A30: z = [y,j] by BORSUK_1:10;
reconsider ez = F . z, ey = y as Point of (Euclid n) by TOPREAL3:8;
reconsider fp = ep, fz = ez, fe = (1 - i) * y, fy = y as Element of REAL n by EUCLID:22;
A31: ( (1 - i) * ((r0 / (1 - i)) / 2) = r0 / 2 & (r0 / 2) / (1 - i) = (r0 / (1 - i)) / 2 ) by A9, XCMPLX_1:48, XCMPLX_1:97;
fy in B by A28, A30, ZFMISC_1:87;
then A32: dist (lx,ey) < (r0 / 2) / (1 - i) by METRIC_1:11;
j in X2 by A28, A30, ZFMISC_1:87;
then j in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ by XBOOLE_0:def 4;
then |.(j - i).| < ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0) by RCOMP_1:1;
then |.(i - j).| < ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0) by UNIFORM1:11;
then A33: |.(i - j).| * |.fy.| <= (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * |.fy.| by XREAL_1:64;
reconsider yy = ey as Element of n -tuples_on REAL by A2, EUCLID:22;
ez = F . (y,j) by A30
.= (1 - j) * y by A1 ;
then fe - fz = ((1 - i) * yy) - ((1 - j) * yy) ;
then A34: |.(fe - fz).| = |.(((1 - i) - (1 - j)) * fy).| by Th8
.= |.(j - i).| * |.fy.| by EUCLID:11
.= |.(i - j).| * |.fy.| by UNIFORM1:11 ;
reconsider gx = fx, gy = fy as Element of n -tuples_on REAL by EUCLID:def 1;
A35: ( dist (ep,ez) = |.(fp - fz).| & |.(fp - fz).| <= |.(fp - fe).| + |.(fe - fz).| ) by EUCLID:19, SPPOL_1:5;
A36: (1 - i) * (fx - fy) = (1 - i) * (gx - gy)
.= ((1 - i) * gx) - ((1 - i) * gy) by Th7
.= ((1 - i) * fx) - ((1 - i) * fy)
.= ((1 - i) * fx) - fe ;
A37: dist (lx,ey) = |.(fx - fy).| by SPPOL_1:5;
then (1 - i) * |.(fx - fy).| < (1 - i) * ((r0 / 2) / (1 - i)) by A9, A32, XREAL_1:68;
then |.(1 - i).| * |.(fx - fy).| < r0 / 2 by A9, A31, ABSVALUE:def 1;
then A38: |.(((1 - i) * fx) - fe).| < r0 / 2 by A36, EUCLID:11;
( |.(fx - fy).| = |.(fy - fx).| & |.fy.| - |.fx.| <= |.(fy - fx).| ) by EUCLID:15, EUCLID:18;
then |.fy.| - |.fx.| < (r0 / 2) / (1 - i) by A32, A37, XXREAL_0:2;
then |.fy.| < |.fx.| + ((r0 / 2) / (1 - i)) by XREAL_1:19;
then A39: (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * |.fy.| < (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * (|.fx.| + ((r0 / 2) / (1 - i))) by A12, XREAL_1:68;
(((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * (|.fx.| + ((r0 / 2) / (1 - i))) = (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * (|.fx.| + (r0 / (2 * (1 - i)))) by XCMPLX_1:78
.= (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * (((|.fx.| * (2 * (1 - i))) / (2 * (1 - i))) + (r0 / (2 * (1 - i)))) by A26, XCMPLX_1:89
.= (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) * (((|.fx.| * (2 * (1 - i))) + r0) / (2 * (1 - i))) by XCMPLX_1:62
.= ((1 - i) * r0) / (2 * (1 - i)) by A6, A9, XCMPLX_1:98
.= r0 / 2 by A9, XCMPLX_1:91 ;
then A40: |.(i - j).| * |.fy.| <= r0 / 2 by A33, A39, XXREAL_0:2;
fp = (1 - i) * x by A5
.= (1 - i) * fx ;
then |.(fp - fe).| + |.(fe - fz).| < (r0 / 2) + (r0 / 2) by A34, A40, A38, XREAL_1:8;
then dist (ep,ez) < r0 by A35, XXREAL_0:2;
hence m in Ball (ep,r0) by A29, METRIC_1:11; :: thesis: verum
end;
hence F .: W c= V by A7; :: thesis: verum
end;
suppose A41: 1 - i <= 0 ; :: thesis: ex W being Subset of [:(TOP-REAL n),I[01]:] st
( p in W & W is open & F .: W c= V )
A42: i <= 1 by BORSUK_1:43;
(1 - i) + i <= 0 + i by A41, XREAL_1:6;
then A43: i = 1 by A42, XXREAL_0:1;
set t = |.fx.| + r0;
reconsider B = Ball (lx,r0) as Subset of (TOP-REAL n) by TOPREAL3:8;
set c = r0 / (|.fx.| + r0);
set X1 = ].(1 - (r0 / (|.fx.| + r0))),1.];
A44: x in B by A6, GOBOARD6:1;
0 + r0 <= |.fx.| + r0 by XREAL_1:7;
then A45: r0 / (|.fx.| + r0) <= 1 by A6, XREAL_1:185;
then A46: (r0 / (|.fx.| + r0)) - (r0 / (|.fx.| + r0)) <= 1 - (r0 / (|.fx.| + r0)) by XREAL_1:9;
].(1 - (r0 / (|.fx.| + r0))),1.] c= the carrier of I[01]
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in ].(1 - (r0 / (|.fx.| + r0))),1.] or s in the carrier of I[01] )
assume A47: s in ].(1 - (r0 / (|.fx.| + r0))),1.] ; :: thesis: s in the carrier of I[01]
then reconsider s = s as Real ;
( s <= 1 & 1 - (r0 / (|.fx.| + r0)) < s ) by A47, XXREAL_1:2;
hence s in the carrier of I[01] by A46, BORSUK_1:43; :: thesis: verum
end;
then reconsider X1 = ].(1 - (r0 / (|.fx.| + r0))),1.] as Subset of I[01] ;
r0 / (|.fx.| + r0) is Point of I[01] by A6, A45, BORSUK_1:43;
then 1 - (r0 / (|.fx.| + r0)) is Point of I[01] by JORDAN5B:4;
then A48: X1 is open by Th4;
take W = [:B,X1:]; :: thesis: ( p in W & W is open & F .: W c= V )
A49: 0 < r0 / (|.fx.| + r0) by A6, XREAL_1:139;
then 1 - (r0 / (|.fx.| + r0)) < 1 - 0 by XREAL_1:15;
then i in X1 by A43, XXREAL_1:2;
hence p in W by A4, A44, ZFMISC_1:87; :: thesis: ( W is open & F .: W c= V )
B is open by GOBOARD6:3;
hence W is open by A48, BORSUK_1:6; :: thesis: F .: W c= V
F .: W c= Ball (ep,r0)
proof
let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in F .: W or m in Ball (ep,r0) )
assume m in F .: W ; :: thesis: m in Ball (ep,r0)
then consider z being object such that
A50: z in dom F and
A51: z in W and
A52: F . z = m by FUNCT_1:def 6;
reconsider z = z as Point of [:(TOP-REAL n),I[01]:] by A50;
consider y being Point of (TOP-REAL n), j being Point of I[01] such that
A53: z = [y,j] by BORSUK_1:10;
reconsider ez = F . z, ey = y as Point of (Euclid n) by TOPREAL3:8;
reconsider fp = ep, fz = ez, fy = y as Element of REAL n by EUCLID:22;
fy in B by A51, A53, ZFMISC_1:87;
then A54: dist (lx,ey) < r0 by METRIC_1:11;
A55: ez = F . (y,j) by A53
.= (1 - j) * y by A1 ;
fp = (1 - i) * x by A5
.= 0. (TOP-REAL n) by A43, RLVECT_1:10 ;
then A56: fz - fp = (F . z) - (0. (TOP-REAL n))
.= fz by RLVECT_1:13 ;
A57: |.fy.| - |.fx.| <= |.(fy - fx).| by EUCLID:15;
( dist (lx,ey) = |.(fx - fy).| & |.(fx - fy).| = |.(fy - fx).| ) by EUCLID:18, SPPOL_1:5;
then |.fy.| - |.fx.| < r0 by A54, A57, XXREAL_0:2;
then A58: |.fy.| < |.fx.| + r0 by XREAL_1:19;
A59: now :: thesis: (1 - j) * |.fy.| < r0
per cases ( j < 1 or j >= 1 ) ;
suppose j < 1 ; :: thesis: (1 - j) * |.fy.| < r0
then A60: j - j < 1 - j by XREAL_1:14;
j in X1 by A51, A53, ZFMISC_1:87;
then 1 - (r0 / (|.fx.| + r0)) < j by XXREAL_1:2;
then (1 - (r0 / (|.fx.| + r0))) + (r0 / (|.fx.| + r0)) < j + (r0 / (|.fx.| + r0)) by XREAL_1:8;
then 1 - j < (j + (r0 / (|.fx.| + r0))) - j by XREAL_1:14;
then r0 / (1 - j) > r0 / (r0 / (|.fx.| + r0)) by A6, A60, XREAL_1:76;
then |.fx.| + r0 < r0 / (1 - j) by A49, XCMPLX_1:54;
then |.fy.| < r0 / (1 - j) by A58, XXREAL_0:2;
then (1 - j) * |.fy.| < (1 - j) * (r0 / (1 - j)) by A60, XREAL_1:68;
hence (1 - j) * |.fy.| < r0 by A60, XCMPLX_1:87; :: thesis: verum
end;
suppose A61: j >= 1 ; :: thesis: (1 - j) * |.fy.| < r0
j <= 1 by BORSUK_1:43;
then j = 1 by A61, XXREAL_0:1;
hence (1 - j) * |.fy.| < r0 by A6; :: thesis: verum
end;
end;
end;
1 - j is Point of I[01] by JORDAN5B:4;
then A62: 0 <= 1 - j by BORSUK_1:43;
dist (ep,ez) = |.(fz - fp).| by SPPOL_1:5
.= |.fz.| by A56
.= |.((1 - j) * fy).| by A55
.= |.(1 - j).| * |.fy.| by EUCLID:11
.= (1 - j) * |.fy.| by A62, ABSVALUE:def 1 ;
hence m in Ball (ep,r0) by A52, A59, METRIC_1:11; :: thesis: verum
end;
hence F .: W c= V by A7; :: thesis: verum
end;
end;
end;
hence F is continuous by JGRAPH_2:10; :: thesis: verum