:: UNIFORM1 semantic presentation
begin
theorem Th1: :: UNIFORM1:1
for r being Real st r > 0 holds
ex n being Element of NAT st
( n > 0 & 1 / n < r )
proof
let r be Real; ::_thesis: ( r > 0 implies ex n being Element of NAT st
( n > 0 & 1 / n < r ) )
assume A1: r > 0 ; ::_thesis: ex n being Element of NAT st
( n > 0 & 1 / n < r )
A2: 1 / r > 0 by A1;
consider n being Element of NAT such that
A3: 1 / r < n by SEQ_4:3;
(1 / r) * r < n * r by A1, A3, XREAL_1:68;
then 1 < n * r by A1, XCMPLX_1:87;
then 1 / n < r by A3, A2, XREAL_1:83;
hence ex n being Element of NAT st
( n > 0 & 1 / n < r ) by A3, A2; ::_thesis: verum
end;
definition
let X, Y be non empty MetrStruct ;
let f be Function of X,Y;
attrf is uniformly_continuous means :Def1: :: UNIFORM1:def 1
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for u1, u2 being Element of X st dist (u1,u2) < s holds
dist ((f /. u1),(f /. u2)) < r ) );
end;
:: deftheorem Def1 defines uniformly_continuous UNIFORM1:def_1_:_
for X, Y being non empty MetrStruct
for f being Function of X,Y holds
( f is uniformly_continuous iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for u1, u2 being Element of X st dist (u1,u2) < s holds
dist ((f /. u1),(f /. u2)) < r ) ) );
theorem Th2: :: UNIFORM1:2
for X being non empty TopSpace
for M being non empty MetrSpace
for f being Function of X,(TopSpaceMetr M) st f is continuous holds
for r being Real
for u being Element of M
for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds
f " P is open
proof
let X be non empty TopSpace; ::_thesis: for M being non empty MetrSpace
for f being Function of X,(TopSpaceMetr M) st f is continuous holds
for r being Real
for u being Element of M
for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds
f " P is open
let M be non empty MetrSpace; ::_thesis: for f being Function of X,(TopSpaceMetr M) st f is continuous holds
for r being Real
for u being Element of M
for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds
f " P is open
let f be Function of X,(TopSpaceMetr M); ::_thesis: ( f is continuous implies for r being Real
for u being Element of M
for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds
f " P is open )
assume A1: f is continuous ; ::_thesis: for r being Real
for u being Element of M
for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds
f " P is open
thus for r being Real
for u being Element of M
for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds
f " P is open ::_thesis: verum
proof
let r be Real; ::_thesis: for u being Element of M
for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds
f " P is open
let u be Element of M; ::_thesis: for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds
f " P is open
let P be Subset of (TopSpaceMetr M); ::_thesis: ( P = Ball (u,r) implies f " P is open )
reconsider P9 = P as Subset of (TopSpaceMetr M) ;
assume P = Ball (u,r) ; ::_thesis: f " P is open
then ( [#] (TopSpaceMetr M) <> {} & P9 is open ) by TOPMETR:14;
hence f " P is open by A1, TOPS_2:43; ::_thesis: verum
end;
end;
theorem Th3: :: UNIFORM1:3
for N, M being non empty MetrSpace
for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st ( for r being real number
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) ) holds
f is continuous
proof
let N, M be non empty MetrSpace; ::_thesis: for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st ( for r being real number
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) ) holds
f is continuous
let f be Function of (TopSpaceMetr N),(TopSpaceMetr M); ::_thesis: ( ( for r being real number
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) ) implies f is continuous )
dom f = the carrier of (TopSpaceMetr N) by FUNCT_2:def_1;
then A1: dom f = the carrier of N by TOPMETR:12;
now__::_thesis:_(_(_for_r_being_real_number_
for_u_being_Element_of_N
for_u1_being_Element_of_M_st_r_>_0_&_u1_=_f_._u_holds_
ex_s_being_real_number_st_
(_s_>_0_&_(_for_w_being_Element_of_N
for_w1_being_Element_of_M_st_w1_=_f_._w_&_dist_(u,w)_<_s_holds_
dist_(u1,w1)_<_r_)_)_)_implies_f_is_continuous_)
assume A2: for r being real number
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) ; ::_thesis: f is continuous
for r being real number
for u being Element of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds
f " P is open
proof
let r be real number ; ::_thesis: for u being Element of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds
f " P is open
let u be Element of M; ::_thesis: for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds
f " P is open
let P be Subset of (TopSpaceMetr M); ::_thesis: ( r > 0 & P = Ball (u,r) implies f " P is open )
reconsider P9 = P as Subset of (TopSpaceMetr M) ;
assume that
r > 0 and
A3: P = Ball (u,r) ; ::_thesis: f " P is open
for p being Point of N st p in f " P holds
ex s being real number st
( s > 0 & Ball (p,s) c= f " P )
proof
let p be Point of N; ::_thesis: ( p in f " P implies ex s being real number st
( s > 0 & Ball (p,s) c= f " P ) )
assume p in f " P ; ::_thesis: ex s being real number st
( s > 0 & Ball (p,s) c= f " P )
then A4: f . p in Ball (u,r) by A3, FUNCT_1:def_7;
then reconsider wf = f . p as Element of M ;
P9 is open by A3, TOPMETR:14;
then consider r1 being real number such that
A5: r1 > 0 and
A6: Ball (wf,r1) c= P by A3, A4, TOPMETR:15;
reconsider r1 = r1 as Real by XREAL_0:def_1;
consider s being real number such that
A7: s > 0 and
A8: for w being Element of N
for w1 being Element of M st w1 = f . w & dist (p,w) < s holds
dist (wf,w1) < r1 by A2, A5;
reconsider s = s as Real by XREAL_0:def_1;
Ball (p,s) c= f " P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ball (p,s) or x in f " P )
assume A9: x in Ball (p,s) ; ::_thesis: x in f " P
then reconsider wx = x as Element of N ;
f . wx in rng f by A1, FUNCT_1:def_3;
then reconsider wfx = f . wx as Element of M by TOPMETR:12;
dist (p,wx) < s by A9, METRIC_1:11;
then dist (wf,wfx) < r1 by A8;
then wfx in Ball (wf,r1) by METRIC_1:11;
hence x in f " P by A1, A6, FUNCT_1:def_7; ::_thesis: verum
end;
hence ex s being real number st
( s > 0 & Ball (p,s) c= f " P ) by A7; ::_thesis: verum
end;
hence f " P is open by TOPMETR:15; ::_thesis: verum
end;
hence f is continuous by JORDAN2B:16; ::_thesis: verum
end;
hence ( ( for r being real number
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) ) implies f is continuous ) ; ::_thesis: verum
end;
theorem Th4: :: UNIFORM1:4
for N, M being non empty MetrSpace
for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f is continuous holds
for r being Real
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
proof
let N, M be non empty MetrSpace; ::_thesis: for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f is continuous holds
for r being Real
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
let f be Function of (TopSpaceMetr N),(TopSpaceMetr M); ::_thesis: ( f is continuous implies for r being Real
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) )
assume A1: f is continuous ; ::_thesis: for r being Real
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
let r be Real; ::_thesis: for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
let u be Element of N; ::_thesis: for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
let u1 be Element of M; ::_thesis: ( r > 0 & u1 = f . u implies ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) )
reconsider P = Ball (u1,r) as Subset of (TopSpaceMetr M) by TOPMETR:12;
A2: ( the carrier of N = the carrier of (TopSpaceMetr N) & dom f = the carrier of (TopSpaceMetr N) ) by FUNCT_2:def_1, TOPMETR:12;
assume ( r > 0 & u1 = f . u ) ; ::_thesis: ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
then f . u in P by GOBOARD6:1;
then A3: u in f " P by A2, FUNCT_1:def_7;
f " P is open by A1, Th2;
then consider s1 being real number such that
A4: s1 > 0 and
A5: Ball (u,s1) c= f " P by A3, TOPMETR:15;
reconsider s1 = s1 as Real by XREAL_0:def_1;
for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s1 holds
dist (u1,w1) < r
proof
let w be Element of N; ::_thesis: for w1 being Element of M st w1 = f . w & dist (u,w) < s1 holds
dist (u1,w1) < r
let w1 be Element of M; ::_thesis: ( w1 = f . w & dist (u,w) < s1 implies dist (u1,w1) < r )
assume that
A6: w1 = f . w and
A7: dist (u,w) < s1 ; ::_thesis: dist (u1,w1) < r
w in Ball (u,s1) by A7, METRIC_1:11;
then f . w in P by A5, FUNCT_1:def_7;
hence dist (u1,w1) < r by A6, METRIC_1:11; ::_thesis: verum
end;
hence ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) by A4; ::_thesis: verum
end;
theorem :: UNIFORM1:5
for N, M being non empty MetrSpace
for f being Function of N,M
for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f = g & f is uniformly_continuous holds
g is continuous
proof
let N, M be non empty MetrSpace; ::_thesis: for f being Function of N,M
for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f = g & f is uniformly_continuous holds
g is continuous
let f be Function of N,M; ::_thesis: for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f = g & f is uniformly_continuous holds
g is continuous
let g be Function of (TopSpaceMetr N),(TopSpaceMetr M); ::_thesis: ( f = g & f is uniformly_continuous implies g is continuous )
assume that
A1: f = g and
A2: f is uniformly_continuous ; ::_thesis: g is continuous
for r being real number
for u being Element of N
for u1 being Element of M st r > 0 & u1 = g . u holds
ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
proof
let r be real number ; ::_thesis: for u being Element of N
for u1 being Element of M st r > 0 & u1 = g . u holds
ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
let u be Element of N; ::_thesis: for u1 being Element of M st r > 0 & u1 = g . u holds
ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
let u1 be Element of M; ::_thesis: ( r > 0 & u1 = g . u implies ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) )
reconsider r9 = r as Real by XREAL_0:def_1;
assume that
A3: r > 0 and
A4: u1 = g . u ; ::_thesis: ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
consider s being Real such that
A5: 0 < s and
A6: for wu1, wu2 being Element of N st dist (wu1,wu2) < s holds
dist ((f /. wu1),(f /. wu2)) < r9 by A2, A3, Def1;
for w being Element of N
for w1 being Element of M st w1 = g . w & dist (u,w) < s holds
dist (u1,w1) < r
proof
let w be Element of N; ::_thesis: for w1 being Element of M st w1 = g . w & dist (u,w) < s holds
dist (u1,w1) < r
let w1 be Element of M; ::_thesis: ( w1 = g . w & dist (u,w) < s implies dist (u1,w1) < r )
assume that
A7: w1 = g . w and
A8: dist (u,w) < s ; ::_thesis: dist (u1,w1) < r
A9: u1 = f /. u by A1, A4;
w1 = f /. w by A1, A7;
hence dist (u1,w1) < r by A6, A8, A9; ::_thesis: verum
end;
hence ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) by A5; ::_thesis: verum
end;
hence g is continuous by Th3; ::_thesis: verum
end;
theorem Th6: :: UNIFORM1:6
for N being non empty MetrSpace
for G being Subset-Family of (TopSpaceMetr N) st G is Cover of (TopSpaceMetr N) & G is open & TopSpaceMetr N is compact holds
ex r being Real st
( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds
ex Ga being Subset of (TopSpaceMetr N) st
( w1 in Ga & w2 in Ga & Ga in G ) ) )
proof
let N be non empty MetrSpace; ::_thesis: for G being Subset-Family of (TopSpaceMetr N) st G is Cover of (TopSpaceMetr N) & G is open & TopSpaceMetr N is compact holds
ex r being Real st
( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds
ex Ga being Subset of (TopSpaceMetr N) st
( w1 in Ga & w2 in Ga & Ga in G ) ) )
let G be Subset-Family of (TopSpaceMetr N); ::_thesis: ( G is Cover of (TopSpaceMetr N) & G is open & TopSpaceMetr N is compact implies ex r being Real st
( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds
ex Ga being Subset of (TopSpaceMetr N) st
( w1 in Ga & w2 in Ga & Ga in G ) ) ) )
assume that
A1: G is Cover of (TopSpaceMetr N) and
A2: G is open and
A3: TopSpaceMetr N is compact ; ::_thesis: ex r being Real st
( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds
ex Ga being Subset of (TopSpaceMetr N) st
( w1 in Ga & w2 in Ga & Ga in G ) ) )
now__::_thesis:_ex_r_being_Real_st_
(_r_>_0_&_(_for_w1,_w2_being_Element_of_N_st_dist_(w1,w2)_<_r_holds_
ex_Ga_being_Subset_of_(TopSpaceMetr_N)_st_
(_w1_in_Ga_&_w2_in_Ga_&_Ga_in_G_)_)_)
set TM = TopSpaceMetr N;
defpred S1[ set , set ] means for n being Element of NAT
for w1 being Element of N st n = $1 & w1 = $2 holds
ex w2 being Element of N st
( dist (w1,w2) < 1 / (n + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds
( not w1 in Ga or not w2 in Ga or not Ga in G ) ) );
A4: TopSpaceMetr N = TopStruct(# the carrier of N,(Family_open_set N) #) by PCOMPS_1:def_5;
assume A5: for r being Real holds
( not r > 0 or ex w1, w2 being Element of N st
( dist (w1,w2) < r & ( for Ga being Subset of (TopSpaceMetr N) holds
( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) ) ; ::_thesis: contradiction
A6: for e being set st e in NAT holds
ex u being set st
( u in the carrier of N & S1[e,u] )
proof
let e be set ; ::_thesis: ( e in NAT implies ex u being set st
( u in the carrier of N & S1[e,u] ) )
assume e in NAT ; ::_thesis: ex u being set st
( u in the carrier of N & S1[e,u] )
then reconsider m = e as Element of NAT ;
set r = 1 / (m + 1);
consider w1, w2 being Element of N such that
A7: ( dist (w1,w2) < 1 / (m + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds
( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) by A5;
for n being Element of NAT
for w4 being Element of N st n = e & w4 = w1 holds
ex w5 being Element of N st
( dist (w4,w5) < 1 / (n + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds
( not w4 in Ga or not w5 in Ga or not Ga in G ) ) ) by A7;
hence ex u being set st
( u in the carrier of N & S1[e,u] ) ; ::_thesis: verum
end;
ex f being Function of NAT, the carrier of N st
for e being set st e in NAT holds
S1[e,f . e] from FUNCT_2:sch_1(A6);
then consider f being Function of NAT, the carrier of N such that
A8: for e being set st e in NAT holds
for n being Element of NAT
for w1 being Element of N st n = e & w1 = f . e holds
ex w2 being Element of N st
( dist (w1,w2) < 1 / (n + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds
( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) ;
defpred S2[ Subset of (TopSpaceMetr N)] means ex p being Element of NAT st $1 = { x where x is Point of N : ex n being Element of NAT st
( p <= n & x = f . n ) } ;
consider F being Subset-Family of (TopSpaceMetr N) such that
A9: for B being Subset of (TopSpaceMetr N) holds
( B in F iff S2[B] ) from SUBSET_1:sch_3();
defpred S3[ set ] means ex n being Element of NAT st
( 0 <= n & $1 = f . n );
set B0 = { x where x is Point of N : S3[x] } ;
A10: { x where x is Point of N : S3[x] } is Subset of N from DOMAIN_1:sch_7();
then A11: { x where x is Point of N : S3[x] } in F by A4, A9;
A12: for p being Element of NAT holds { x where x is Point of N : ex n being Element of NAT st
( p <= n & x = f . n ) } <> {}
proof
let p be Element of NAT ; ::_thesis: { x where x is Point of N : ex n being Element of NAT st
( p <= n & x = f . n ) } <> {}
f . p in { x where x is Point of N : ex n being Element of NAT st
( p <= n & x = f . n ) } ;
hence { x where x is Point of N : ex n being Element of NAT st
( p <= n & x = f . n ) } <> {} ; ::_thesis: verum
end;
reconsider B0 = { x where x is Point of N : S3[x] } as Subset of (TopSpaceMetr N) by A4, A10;
reconsider F = F as Subset-Family of (TopSpaceMetr N) ;
set G1 = clf F;
A13: Cl B0 in clf F by A11, PCOMPS_1:def_2;
( clf F <> {} & ( for Gd being set st Gd <> {} & Gd c= clf F & Gd is finite holds
meet Gd <> {} ) )
proof
thus clf F <> {} by A13; ::_thesis: for Gd being set st Gd <> {} & Gd c= clf F & Gd is finite holds
meet Gd <> {}
let H be set ; ::_thesis: ( H <> {} & H c= clf F & H is finite implies meet H <> {} )
assume that
A14: H <> {} and
A15: H c= clf F and
A16: H is finite ; ::_thesis: meet H <> {}
reconsider H = H as Subset-Family of (TopSpaceMetr N) by A15, TOPS_2:2;
H is c=-linear
proof
let B, C be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not B in H or not C in H or B,C are_c=-comparable )
assume that
A17: B in H and
A18: C in H ; ::_thesis: B,C are_c=-comparable
reconsider B = B as Subset of (TopSpaceMetr N) by A17;
consider V being Subset of (TopSpaceMetr N) such that
A19: B = Cl V and
A20: V in F by A15, A17, PCOMPS_1:def_2;
consider p being Element of NAT such that
A21: V = { x where x is Point of N : ex n being Element of NAT st
( p <= n & x = f . n ) } by A9, A20;
reconsider C = C as Subset of (TopSpaceMetr N) by A18;
consider W being Subset of (TopSpaceMetr N) such that
A22: C = Cl W and
A23: W in F by A15, A18, PCOMPS_1:def_2;
consider q being Element of NAT such that
A24: W = { x where x is Point of N : ex n being Element of NAT st
( q <= n & x = f . n ) } by A9, A23;
now__::_thesis:_(_(_q_<=_p_&_V_c=_W_)_or_(_p_<=_q_&_W_c=_V_)_)
percases ( q <= p or p <= q ) ;
caseA25: q <= p ; ::_thesis: V c= W
thus V c= W ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in V or y in W )
assume y in V ; ::_thesis: y in W
then consider x being Point of N such that
A26: y = x and
A27: ex n being Element of NAT st
( p <= n & x = f . n ) by A21;
consider n being Element of NAT such that
A28: p <= n and
A29: x = f . n by A27;
q <= n by A25, A28, XXREAL_0:2;
hence y in W by A24, A26, A29; ::_thesis: verum
end;
end;
caseA30: p <= q ; ::_thesis: W c= V
thus W c= V ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in W or y in V )
assume y in W ; ::_thesis: y in V
then consider x being Point of N such that
A31: y = x and
A32: ex n being Element of NAT st
( q <= n & x = f . n ) by A24;
consider n being Element of NAT such that
A33: q <= n and
A34: x = f . n by A32;
p <= n by A30, A33, XXREAL_0:2;
hence y in V by A21, A31, A34; ::_thesis: verum
end;
end;
end;
end;
then ( B c= C or C c= B ) by A19, A22, PRE_TOPC:19;
hence B,C are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;
then consider m being set such that
A35: m in H and
A36: for C being set st C in H holds
m c= C by A14, A16, FINSET_1:11;
A37: m c= meet H by A14, A36, SETFAM_1:5;
reconsider m = m as Subset of (TopSpaceMetr N) by A35;
consider A being Subset of (TopSpaceMetr N) such that
A38: m = Cl A and
A39: A in F by A15, A35, PCOMPS_1:def_2;
A <> {} by A9, A12, A39;
then m <> {} by A38, PRE_TOPC:18, XBOOLE_1:3;
hence meet H <> {} by A37; ::_thesis: verum
end;
then ( clf F is closed & clf F is centered ) by FINSET_1:def_3, PCOMPS_1:11;
then meet (clf F) <> {} by A3, COMPTS_1:4;
then consider c being Point of (TopSpaceMetr N) such that
A40: c in meet (clf F) by SUBSET_1:4;
reconsider c = c as Point of N by A4;
consider Ge being Subset of (TopSpaceMetr N) such that
A41: c in Ge and
A42: Ge in G by A1, PCOMPS_1:3;
reconsider Ge = Ge as Subset of (TopSpaceMetr N) ;
Ge is open by A2, A42, TOPS_2:def_1;
then consider r being real number such that
A43: r > 0 and
A44: Ball (c,r) c= Ge by A41, TOPMETR:15;
reconsider r = r as Real by XREAL_0:def_1;
consider n being Element of NAT such that
A45: n > 0 and
A46: 1 / n < r / 2 by A43, Th1, XREAL_1:215;
reconsider Q1 = Ball (c,(r / 2)) as Subset of (TopSpaceMetr N) by TOPMETR:12;
A47: Q1 is open by TOPMETR:14;
defpred S4[ set ] means ex n2 being Element of NAT st
( n <= n2 & $1 = f . n2 );
reconsider B2 = { x where x is Point of (TopSpaceMetr N) : S4[x] } as Subset of (TopSpaceMetr N) from DOMAIN_1:sch_7();
A48: the carrier of (TopSpaceMetr N) = the carrier of N by TOPMETR:12;
then B2 in F by A9;
then Cl B2 in clf F by PCOMPS_1:def_2;
then A49: c in Cl B2 by A40, SETFAM_1:def_1;
c in Q1 by A43, GOBOARD6:1, XREAL_1:215;
then B2 meets Q1 by A49, A47, TOPS_1:12;
then consider x being set such that
A50: x in B2 and
A51: x in Q1 by XBOOLE_0:3;
consider y being Point of N such that
A52: x = y and
A53: ex n2 being Element of NAT st
( n <= n2 & y = f . n2 ) by A48, A50;
A54: dist (c,y) < r / 2 by A51, A52, METRIC_1:11;
1 / n >= 1 / (n + 1) by A45, NAT_1:11, XREAL_1:85;
then A55: 1 / (n + 1) < r / 2 by A46, XXREAL_0:2;
consider n2 being Element of NAT such that
A56: n <= n2 and
A57: y = f . n2 by A53;
consider w2 being Element of N such that
A58: dist (y,w2) < 1 / (n2 + 1) and
A59: for Ga being Subset of (TopSpaceMetr N) holds
( not y in Ga or not w2 in Ga or not Ga in G ) by A8, A57;
n + 1 <= n2 + 1 by A56, XREAL_1:7;
then 1 / (n + 1) >= 1 / (n2 + 1) by XREAL_1:118;
then dist (y,w2) < 1 / (n + 1) by A58, XXREAL_0:2;
then dist (y,w2) < r / 2 by A55, XXREAL_0:2;
then A60: (r / 2) + (dist (y,w2)) < (r / 2) + (r / 2) by XREAL_1:6;
r / 1 > r / 2 by A43, XREAL_1:76;
then dist (c,y) < r by A54, XXREAL_0:2;
then A61: y in Ball (c,r) by METRIC_1:11;
( dist (c,w2) <= (dist (c,y)) + (dist (y,w2)) & (dist (c,y)) + (dist (y,w2)) < (r / 2) + (dist (y,w2)) ) by A54, METRIC_1:4, XREAL_1:6;
then dist (c,w2) < (r / 2) + (dist (y,w2)) by XXREAL_0:2;
then dist (c,w2) < (r / 2) + (r / 2) by A60, XXREAL_0:2;
then w2 in Ball (c,r) by METRIC_1:11;
hence contradiction by A42, A44, A61, A59; ::_thesis: verum
end;
hence ex r being Real st
( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds
ex Ga being Subset of (TopSpaceMetr N) st
( w1 in Ga & w2 in Ga & Ga in G ) ) ) ; ::_thesis: verum
end;
begin
theorem Th7: :: UNIFORM1:7
for N, M being non empty MetrSpace
for f being Function of N,M
for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st g = f & TopSpaceMetr N is compact & g is continuous holds
f is uniformly_continuous
proof
let N, M be non empty MetrSpace; ::_thesis: for f being Function of N,M
for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st g = f & TopSpaceMetr N is compact & g is continuous holds
f is uniformly_continuous
let f be Function of N,M; ::_thesis: for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st g = f & TopSpaceMetr N is compact & g is continuous holds
f is uniformly_continuous
let g be Function of (TopSpaceMetr N),(TopSpaceMetr M); ::_thesis: ( g = f & TopSpaceMetr N is compact & g is continuous implies f is uniformly_continuous )
assume that
A1: g = f and
A2: TopSpaceMetr N is compact and
A3: g is continuous ; ::_thesis: f is uniformly_continuous
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for u1, u2 being Element of N st dist (u1,u2) < s holds
dist ((f /. u1),(f /. u2)) < r ) )
proof
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for u1, u2 being Element of N st dist (u1,u2) < s holds
dist ((f /. u1),(f /. u2)) < r ) ) )
set G = { P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st
( P = Ball (w,s) & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds
dist (w2,w3) < r / 2 ) ) } ;
A4: the carrier of (TopSpaceMetr N) = the carrier of N by TOPMETR:12;
{ P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st
( P = Ball (w,s) & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds
dist (w2,w3) < r / 2 ) ) } c= bool the carrier of N
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st
( P = Ball (w,s) & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds
dist (w2,w3) < r / 2 ) ) } or x in bool the carrier of N )
assume x in { P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st
( P = Ball (w,s) & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds
dist (w2,w3) < r / 2 ) ) } ; ::_thesis: x in bool the carrier of N
then ex P being Subset of (TopSpaceMetr N) st
( x = P & ex w being Element of N ex s being Real st
( P = Ball (w,s) & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds
dist (w2,w3) < r / 2 ) ) ) ;
hence x in bool the carrier of N ; ::_thesis: verum
end;
then reconsider G1 = { P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st
( P = Ball (w,s) & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds
dist (w2,w3) < r / 2 ) ) } as Subset-Family of (TopSpaceMetr N) by TOPMETR:12;
for P3 being Subset of (TopSpaceMetr N) st P3 in G1 holds
P3 is open
proof
let P3 be Subset of (TopSpaceMetr N); ::_thesis: ( P3 in G1 implies P3 is open )
assume P3 in G1 ; ::_thesis: P3 is open
then ex P being Subset of (TopSpaceMetr N) st
( P3 = P & ex w being Element of N ex s being Real st
( P = Ball (w,s) & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds
dist (w2,w3) < r / 2 ) ) ) ;
hence P3 is open by TOPMETR:14; ::_thesis: verum
end;
then A5: G1 is open by TOPS_2:def_1;
assume 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for u1, u2 being Element of N st dist (u1,u2) < s holds
dist ((f /. u1),(f /. u2)) < r ) )
then A6: 0 < r / 2 by XREAL_1:215;
A7: the carrier of N c= union G1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of N or x in union G1 )
assume x in the carrier of N ; ::_thesis: x in union G1
then reconsider w0 = x as Element of N ;
g . w0 = f /. w0 by A1;
then reconsider w4 = g . w0 as Element of M ;
consider s4 being Real such that
A8: s4 > 0 and
A9: for u5 being Element of N
for w5 being Element of M st w5 = g . u5 & dist (w0,u5) < s4 holds
dist (w4,w5) < r / 2 by A3, A6, Th4;
reconsider P2 = Ball (w0,s4) as Subset of (TopSpaceMetr N) by TOPMETR:12;
for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w0 & w3 = f . w1 & dist (w0,w1) < s4 holds
dist (w2,w3) < r / 2 by A1, A9;
then ex w being Element of N ex s being Real st
( P2 = Ball (w,s) & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds
dist (w2,w3) < r / 2 ) ) ;
then A10: Ball (w0,s4) in G1 ;
x in Ball (w0,s4) by A8, GOBOARD6:1;
hence x in union G1 by A10, TARSKI:def_4; ::_thesis: verum
end;
the carrier of (TopSpaceMetr N) = the carrier of N by TOPMETR:12;
then the carrier of N = union G1 by A7, XBOOLE_0:def_10;
then G1 is Cover of (TopSpaceMetr N) by A4, SETFAM_1:45;
then consider s1 being Real such that
A11: s1 > 0 and
A12: for w1, w2 being Element of N st dist (w1,w2) < s1 holds
ex Ga being Subset of (TopSpaceMetr N) st
( w1 in Ga & w2 in Ga & Ga in G1 ) by A2, A5, Th6;
for u1, u2 being Element of N st dist (u1,u2) < s1 holds
dist ((f /. u1),(f /. u2)) < r
proof
let u1, u2 be Element of N; ::_thesis: ( dist (u1,u2) < s1 implies dist ((f /. u1),(f /. u2)) < r )
assume dist (u1,u2) < s1 ; ::_thesis: dist ((f /. u1),(f /. u2)) < r
then consider Ga being Subset of (TopSpaceMetr N) such that
A13: u1 in Ga and
A14: u2 in Ga and
A15: Ga in G1 by A12;
consider P being Subset of (TopSpaceMetr N) such that
A16: Ga = P and
A17: ex w being Element of N ex s2 being Real st
( P = Ball (w,s2) & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s2 holds
dist (w2,w3) < r / 2 ) ) by A15;
consider w being Element of N, s2 being Real such that
A18: P = Ball (w,s2) and
A19: for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s2 holds
dist (w2,w3) < r / 2 by A17;
dist (w,u2) < s2 by A14, A16, A18, METRIC_1:11;
then A20: dist ((f /. w),(f /. u2)) < r / 2 by A19;
dist (w,u1) < s2 by A13, A16, A18, METRIC_1:11;
then dist ((f /. w),(f /. u1)) < r / 2 by A19;
then ( dist ((f /. u1),(f /. u2)) <= (dist ((f /. u1),(f /. w))) + (dist ((f /. w),(f /. u2))) & (dist ((f /. w),(f /. u1))) + (dist ((f /. w),(f /. u2))) < (r / 2) + (r / 2) ) by A20, METRIC_1:4, XREAL_1:8;
hence dist ((f /. u1),(f /. u2)) < r by XXREAL_0:2; ::_thesis: verum
end;
hence ex s being Real st
( 0 < s & ( for u1, u2 being Element of N st dist (u1,u2) < s holds
dist ((f /. u1),(f /. u2)) < r ) ) by A11; ::_thesis: verum
end;
hence f is uniformly_continuous by Def1; ::_thesis: verum
end;
Lm1: Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1))
by TOPMETR:def_7;
Lm2: I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1))
by TOPMETR:20, TOPMETR:def_7;
Lm3: the carrier of I[01] = the carrier of (Closed-Interval-MSpace (0,1))
by Lm1, TOPMETR:12, TOPMETR:20;
theorem :: UNIFORM1:8
for n being Element of NAT
for g being Function of I[01],(TOP-REAL n)
for f being Function of (Closed-Interval-MSpace (0,1)),(Euclid n) st g is continuous & f = g holds
f is uniformly_continuous
proof
let n be Element of NAT ; ::_thesis: for g being Function of I[01],(TOP-REAL n)
for f being Function of (Closed-Interval-MSpace (0,1)),(Euclid n) st g is continuous & f = g holds
f is uniformly_continuous
let g be Function of I[01],(TOP-REAL n); ::_thesis: for f being Function of (Closed-Interval-MSpace (0,1)),(Euclid n) st g is continuous & f = g holds
f is uniformly_continuous
let f be Function of (Closed-Interval-MSpace (0,1)),(Euclid n); ::_thesis: ( g is continuous & f = g implies f is uniformly_continuous )
assume that
A1: g is continuous and
A2: f = g ; ::_thesis: f is uniformly_continuous
A3: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider h = g as Function of I[01],(TopSpaceMetr (Euclid n)) ;
h is continuous by A1, A3, PRE_TOPC:33;
hence f is uniformly_continuous by A2, Lm1, Th7, TOPMETR:20; ::_thesis: verum
end;
theorem :: UNIFORM1:9
for n being Element of NAT
for P being Subset of (TOP-REAL n)
for Q being non empty Subset of (Euclid n)
for g being Function of I[01],((TOP-REAL n) | P)
for f being Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous
proof
let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n)
for Q being non empty Subset of (Euclid n)
for g being Function of I[01],((TOP-REAL n) | P)
for f being Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous
let P be Subset of (TOP-REAL n); ::_thesis: for Q being non empty Subset of (Euclid n)
for g being Function of I[01],((TOP-REAL n) | P)
for f being Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous
let Q be non empty Subset of (Euclid n); ::_thesis: for g being Function of I[01],((TOP-REAL n) | P)
for f being Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous
let g be Function of I[01],((TOP-REAL n) | P); ::_thesis: for f being Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous
let f be Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q); ::_thesis: ( P = Q & g is continuous & f = g implies f is uniformly_continuous )
assume that
A1: P = Q and
A2: ( g is continuous & f = g ) ; ::_thesis: f is uniformly_continuous
(TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q) by A1, EUCLID:63;
hence f is uniformly_continuous by A2, Lm1, Th7, TOPMETR:20; ::_thesis: verum
end;
begin
theorem :: UNIFORM1:10
for n being Element of NAT
for g being Function of I[01],(TOP-REAL n) holds g is Function of (Closed-Interval-MSpace (0,1)),(Euclid n) by Lm3, EUCLID:67;
Lm4: for x being set
for f being FinSequence holds
( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x )
proof
let x be set ; ::_thesis: for f being FinSequence holds
( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x )
let f be FinSequence; ::_thesis: ( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x )
A1: len (<*x*> ^ f) = (len <*x*>) + (len f) by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39 ;
1 <= len <*x*> by FINSEQ_1:39;
then A2: 1 in dom <*x*> by FINSEQ_3:25;
then A3: (<*x*> ^ f) . 1 = <*x*> . 1 by FINSEQ_1:def_7
.= x by FINSEQ_1:def_8 ;
(f ^ <*x*>) . ((len f) + 1) = <*x*> . 1 by A2, FINSEQ_1:def_7
.= x by FINSEQ_1:def_8 ;
hence ( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x ) by A1, A3, FINSEQ_2:16; ::_thesis: verum
end;
Lm5: for x being set
for f being FinSequence st 1 <= len f holds
( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) )
proof
let x be set ; ::_thesis: for f being FinSequence st 1 <= len f holds
( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) )
let f be FinSequence; ::_thesis: ( 1 <= len f implies ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) ) )
assume A1: 1 <= len f ; ::_thesis: ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) )
then A2: len f in dom f by FINSEQ_3:25;
A3: (<*x*> ^ f) . ((len f) + 1) = (<*x*> ^ f) . ((len <*x*>) + (len f)) by FINSEQ_1:39
.= f . (len f) by A2, FINSEQ_1:def_7 ;
1 in dom f by A1, FINSEQ_3:25;
hence ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) ) by A3, FINSEQ_1:def_7; ::_thesis: verum
end;
theorem Th11: :: UNIFORM1:11
for r, s being real number holds abs (r - s) = abs (s - r)
proof
let r, s be real number ; ::_thesis: abs (r - s) = abs (s - r)
percases ( r > s or r = s or r < s ) by XXREAL_0:1;
suppose r > s ; ::_thesis: abs (r - s) = abs (s - r)
then s - r < 0 by XREAL_1:49;
then abs (s - r) = - (s - r) by ABSVALUE:def_1
.= r - s ;
hence abs (r - s) = abs (s - r) ; ::_thesis: verum
end;
suppose r = s ; ::_thesis: abs (r - s) = abs (s - r)
hence abs (r - s) = abs (s - r) ; ::_thesis: verum
end;
suppose r < s ; ::_thesis: abs (r - s) = abs (s - r)
then r - s < 0 by XREAL_1:49;
then abs (r - s) = - (r - s) by ABSVALUE:def_1
.= s - r ;
hence abs (r - s) = abs (s - r) ; ::_thesis: verum
end;
end;
end;
Lm6: for r, s1, s2 being Real holds
( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) )
proof
let r, s1, s2 be Real; ::_thesis: ( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) )
A1: now__::_thesis:_(_r_in_[.s1,s2.]_implies_(_s1_<=_r_&_r_<=_s2_)_)
assume r in [.s1,s2.] ; ::_thesis: ( s1 <= r & r <= s2 )
then r in { r1 where r1 is Real : ( s1 <= r1 & r1 <= s2 ) } by RCOMP_1:def_1;
then ex r1 being Real st
( r1 = r & s1 <= r1 & r1 <= s2 ) ;
hence ( s1 <= r & r <= s2 ) ; ::_thesis: verum
end;
now__::_thesis:_(_s1_<=_r_&_r_<=_s2_implies_r_in_[.s1,s2.]_)
assume ( s1 <= r & r <= s2 ) ; ::_thesis: r in [.s1,s2.]
then r in { r1 where r1 is Real : ( s1 <= r1 & r1 <= s2 ) } ;
hence r in [.s1,s2.] by RCOMP_1:def_1; ::_thesis: verum
end;
hence ( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) ) by A1; ::_thesis: verum
end;
theorem Th12: :: UNIFORM1:12
for r1, r2, s1, s2 being Real st r1 in [.s1,s2.] & r2 in [.s1,s2.] holds
abs (r1 - r2) <= s2 - s1
proof
let r1, r2, s1, s2 be Real; ::_thesis: ( r1 in [.s1,s2.] & r2 in [.s1,s2.] implies abs (r1 - r2) <= s2 - s1 )
assume A1: ( r1 in [.s1,s2.] & r2 in [.s1,s2.] ) ; ::_thesis: abs (r1 - r2) <= s2 - s1
then A2: ( r1 <= s2 & s1 <= r2 ) by Lm6;
A3: ( s1 <= r1 & r2 <= s2 ) by A1, Lm6;
percases ( r1 <= r2 or r1 > r2 ) ;
supposeA4: r1 <= r2 ; ::_thesis: abs (r1 - r2) <= s2 - s1
A5: r2 - r1 <= s2 - s1 by A3, XREAL_1:13;
r2 - r1 >= 0 by A4, XREAL_1:48;
then abs (r2 - r1) <= s2 - s1 by A5, ABSVALUE:def_1;
hence abs (r1 - r2) <= s2 - s1 by Th11; ::_thesis: verum
end;
suppose r1 > r2 ; ::_thesis: abs (r1 - r2) <= s2 - s1
then A6: r1 - r2 >= 0 by XREAL_1:48;
r1 - r2 <= s2 - s1 by A2, XREAL_1:13;
hence abs (r1 - r2) <= s2 - s1 by A6, ABSVALUE:def_1; ::_thesis: verum
end;
end;
end;
definition
let IT be FinSequence of REAL ;
attrIT is decreasing means :Def2: :: UNIFORM1:def 2
for n, m being Element of NAT st n in dom IT & m in dom IT & n < m holds
IT . n > IT . m;
end;
:: deftheorem Def2 defines decreasing UNIFORM1:def_2_:_
for IT being FinSequence of REAL holds
( IT is decreasing iff for n, m being Element of NAT st n in dom IT & m in dom IT & n < m holds
IT . n > IT . m );
Lm7: for f being FinSequence of REAL st ( for k being Element of NAT st 1 <= k & k < len f holds
f /. k < f /. (k + 1) ) holds
f is increasing
proof
let f be FinSequence of REAL ; ::_thesis: ( ( for k being Element of NAT st 1 <= k & k < len f holds
f /. k < f /. (k + 1) ) implies f is increasing )
assume A1: for k being Element of NAT st 1 <= k & k < len f holds
f /. k < f /. (k + 1) ; ::_thesis: f is increasing
now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_f_&_j_in_dom_f_&_i_<_j_holds_
f_._i_<_f_._j
let i, j be Element of NAT ; ::_thesis: ( i in dom f & j in dom f & i < j implies f . i < f . j )
now__::_thesis:_(_i_in_dom_f_&_j_in_dom_f_&_i_<_j_implies_f_._i_<_f_._j_)
defpred S1[ Element of NAT ] means ( i + (1 + $1) <= len f implies f /. i < f /. (i + (1 + $1)) );
assume that
A2: i in dom f and
A3: j in dom f and
A4: i < j ; ::_thesis: f . i < f . j
A5: 1 <= i by A2, FINSEQ_3:25;
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A7: ( i + (1 + k) <= len f implies f /. i < f /. (i + (1 + k)) ) ; ::_thesis: S1[k + 1]
now__::_thesis:_(_i_+_(1_+_(k_+_1))_<=_len_f_implies_f_/._i_<_f_/._(i_+_(1_+_(k_+_1)))_)
( 1 <= i + 1 & i + 1 <= (i + 1) + k ) by NAT_1:11;
then A8: 1 <= (i + 1) + k by XXREAL_0:2;
A9: i + (1 + (k + 1)) = (i + (1 + k)) + 1 ;
1 + k < 1 + (k + 1) by NAT_1:13;
then A10: i + (1 + k) < i + (1 + (k + 1)) by XREAL_1:6;
assume A11: i + (1 + (k + 1)) <= len f ; ::_thesis: f /. i < f /. (i + (1 + (k + 1)))
then i + (1 + k) < len f by A10, XXREAL_0:2;
then f /. (i + (1 + k)) < f /. (i + (1 + (k + 1))) by A1, A8, A9;
hence f /. i < f /. (i + (1 + (k + 1))) by A7, A11, A10, XXREAL_0:2; ::_thesis: verum
end;
hence S1[k + 1] ; ::_thesis: verum
end;
i + 1 <= j by A4, NAT_1:13;
then j -' (i + 1) = j - (i + 1) by XREAL_1:233;
then A12: i + (1 + (j -' (i + 1))) = j ;
A13: f /. i = f . i by A2, PARTFUN1:def_6;
A14: j <= len f by A3, FINSEQ_3:25;
then i < len f by A4, XXREAL_0:2;
then A15: S1[ 0 ] by A1, A5;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A15, A6);
then f /. i < f /. j by A14, A12;
hence f . i < f . j by A3, A13, PARTFUN1:def_6; ::_thesis: verum
end;
hence ( i in dom f & j in dom f & i < j implies f . i < f . j ) ; ::_thesis: verum
end;
hence f is increasing by SEQM_3:def_1; ::_thesis: verum
end;
Lm8: for f being FinSequence of REAL st ( for k being Element of NAT st 1 <= k & k < len f holds
f /. k > f /. (k + 1) ) holds
f is decreasing
proof
let f be FinSequence of REAL ; ::_thesis: ( ( for k being Element of NAT st 1 <= k & k < len f holds
f /. k > f /. (k + 1) ) implies f is decreasing )
assume A1: for k being Element of NAT st 1 <= k & k < len f holds
f /. k > f /. (k + 1) ; ::_thesis: f is decreasing
now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_f_&_j_in_dom_f_&_i_<_j_holds_
f_._i_>_f_._j
let i, j be Element of NAT ; ::_thesis: ( i in dom f & j in dom f & i < j implies f . i > f . j )
now__::_thesis:_(_i_in_dom_f_&_j_in_dom_f_&_i_<_j_implies_f_._i_>_f_._j_)
defpred S1[ Element of NAT ] means ( i + (1 + $1) <= len f implies f /. i > f /. (i + (1 + $1)) );
assume that
A2: i in dom f and
A3: j in dom f and
A4: i < j ; ::_thesis: f . i > f . j
A5: 1 <= i by A2, FINSEQ_3:25;
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A7: ( i + (1 + k) <= len f implies f /. i > f /. (i + (1 + k)) ) ; ::_thesis: S1[k + 1]
now__::_thesis:_(_i_+_(1_+_(k_+_1))_<=_len_f_implies_f_/._i_>_f_/._(i_+_(1_+_(k_+_1)))_)
( 1 <= i + 1 & i + 1 <= (i + 1) + k ) by NAT_1:11;
then A8: 1 <= (i + 1) + k by XXREAL_0:2;
A9: i + (1 + (k + 1)) = (i + (1 + k)) + 1 ;
1 + k < 1 + (k + 1) by NAT_1:13;
then A10: i + (1 + k) < i + (1 + (k + 1)) by XREAL_1:6;
assume A11: i + (1 + (k + 1)) <= len f ; ::_thesis: f /. i > f /. (i + (1 + (k + 1)))
then i + (1 + k) < len f by A10, XXREAL_0:2;
then f /. (i + (1 + k)) > f /. (i + (1 + (k + 1))) by A1, A8, A9;
hence f /. i > f /. (i + (1 + (k + 1))) by A7, A11, A10, XXREAL_0:2; ::_thesis: verum
end;
hence S1[k + 1] ; ::_thesis: verum
end;
i + 1 <= j by A4, NAT_1:13;
then j -' (i + 1) = j - (i + 1) by XREAL_1:233;
then A12: i + (1 + (j -' (i + 1))) = j ;
A13: f /. i = f . i by A2, PARTFUN1:def_6;
A14: j <= len f by A3, FINSEQ_3:25;
then i < len f by A4, XXREAL_0:2;
then A15: S1[ 0 ] by A1, A5;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A15, A6);
then f /. i > f /. j by A14, A12;
hence f . i > f . j by A3, A13, PARTFUN1:def_6; ::_thesis: verum
end;
hence ( i in dom f & j in dom f & i < j implies f . i > f . j ) ; ::_thesis: verum
end;
hence f is decreasing by Def2; ::_thesis: verum
end;
theorem :: UNIFORM1:13
for n being Element of NAT
for e being Real
for g being Function of I[01],(TOP-REAL n)
for p1, p2 being Element of (TOP-REAL n) st e > 0 & g is continuous holds
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 Element of 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 ) )
proof
let n be Element of NAT ; ::_thesis: for e being Real
for g being Function of I[01],(TOP-REAL n)
for p1, p2 being Element of (TOP-REAL n) st e > 0 & g is continuous holds
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 Element of 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.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {1} or x in [.0,1.] )
assume x in {1} ; ::_thesis: x in [.0,1.]
hence x in [.0,1.] by A1, TARSKI:def_1; ::_thesis: verum
end;
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 Real; ::_thesis: for g being Function of I[01],(TOP-REAL n)
for p1, p2 being Element of (TOP-REAL n) st e > 0 & g is continuous holds
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 Element of 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 Function of I[01],(TOP-REAL n); ::_thesis: for p1, p2 being Element of (TOP-REAL n) st e > 0 & g is continuous holds
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 Element of 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 p1, p2 be Element of (TOP-REAL n); ::_thesis: ( e > 0 & g is continuous implies 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 Element of 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 ) ) )
assume that
A4: e > 0 and
A5: g is continuous ; ::_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 Element of 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 ) )
A6: e / 2 > 0 by A4, XREAL_1:215;
A7: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider h = g as Function of I[01],(TopSpaceMetr (Euclid n)) ;
reconsider f = h as Function of (Closed-Interval-MSpace (0,1)),(Euclid n) by Lm3, EUCLID:67;
A8: dom g = the carrier of I[01] by FUNCT_2:def_1;
h is continuous by A5, A7, PRE_TOPC:33;
then f is uniformly_continuous by Lm1, Th7, TOPMETR:20;
then consider s1 being Real such that
A9: 0 < s1 and
A10: 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, Def1;
set s = min (s1,(1 / 2));
defpred S1[ Nat, set ] means $2 = ((min (s1,(1 / 2))) / 2) * ($1 - 1);
A11: 0 <= min (s1,(1 / 2)) by A9, XXREAL_0:20;
then reconsider j = [/(2 / (min (s1,(1 / 2))))\] as Element of NAT by INT_1:53;
A12: 2 / (min (s1,(1 / 2))) <= j by INT_1:def_7;
A13: min (s1,(1 / 2)) <= s1 by XXREAL_0:17;
A14: 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 A13, XXREAL_0:2;
hence dist ((f /. u1),(f /. u2)) < e / 2 by A10; ::_thesis: verum
end;
A15: 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 A16: ((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - j)) <= ((min (s1,(1 / 2))) / 2) * 1 by A11, XREAL_1:64;
A17: for k being Nat st k in Seg j holds
ex x being set st S1[k,x] ;
consider p being FinSequence such that
A18: ( dom p = Seg j & ( for k being Nat st k in Seg j holds
S1[k,p . k] ) ) from FINSEQ_1:sch_1(A17);
A19: Seg (len p) = Seg j by A18, FINSEQ_1:def_3;
rng (p ^ <*1*>) c= REAL
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (p ^ <*1*>) or y in REAL )
A20: len (p ^ <*1*>) = (len p) + (len <*1*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
assume y in rng (p ^ <*1*>) ; ::_thesis: y in REAL
then consider x being set such that
A21: x in dom (p ^ <*1*>) and
A22: y = (p ^ <*1*>) . x by FUNCT_1:def_3;
reconsider nx = x as Element of NAT by A21;
A23: dom (p ^ <*1*>) = Seg (len (p ^ <*1*>)) by FINSEQ_1:def_3;
then A24: nx <= len (p ^ <*1*>) by A21, FINSEQ_1:1;
A25: 1 <= nx by A21, A23, FINSEQ_1:1;
A26: 1 <= nx by A21, A23, FINSEQ_1:1;
now__::_thesis:_(_(_nx_<_(len_p)_+_1_&_y_in_REAL_)_or_(_nx_>=_(len_p)_+_1_&_y_in_REAL_)_)
percases ( nx < (len p) + 1 or nx >= (len p) + 1 ) ;
case nx < (len p) + 1 ; ::_thesis: y in REAL
then A27: nx <= len p by NAT_1:13;
then nx in Seg j by A19, A25, FINSEQ_1:1;
then A28: p . nx = ((min (s1,(1 / 2))) / 2) * (nx - 1) by A18;
y = p . nx by A22, A26, A27, FINSEQ_1:64;
hence y in REAL by A28; ::_thesis: verum
end;
case nx >= (len p) + 1 ; ::_thesis: y in REAL
then nx = (len p) + 1 by A24, A20, XXREAL_0:1;
then y = 1 by A22, Lm4;
hence y in REAL ; ::_thesis: verum
end;
end;
end;
hence y in REAL ; ::_thesis: verum
end;
then reconsider h1 = p ^ <*1*> as FinSequence of REAL by FINSEQ_1:def_4;
A29: len h1 = (len p) + (len <*1*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
A30: len p = j by A18, FINSEQ_1:def_3;
A31: min (s1,(1 / 2)) <> 0 by A9, XXREAL_0:15;
then 2 / (min (s1,(1 / 2))) >= 2 / (1 / 2) by A11, XREAL_1:118, XXREAL_0:17;
then 4 <= j by A12, XXREAL_0:2;
then A32: 4 + 1 <= (len p) + 1 by A30, XREAL_1:6;
A33: (min (s1,(1 / 2))) / 2 > 0 by A11, A31, XREAL_1:215;
A34: for i being Element of 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 Element of 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
A35: ( 1 <= i & i < len p ) and
A36: r1 = p . i and
A37: r2 = p . (i + 1) ; ::_thesis: ( r1 < r2 & r2 - r1 = (min (s1,(1 / 2))) / 2 )
( 1 < i + 1 & i + 1 <= len p ) by A35, NAT_1:13;
then i + 1 in Seg j by A19, FINSEQ_1:1;
then A38: r2 = ((min (s1,(1 / 2))) / 2) * ((i + 1) - 1) by A18, A37;
i < i + 1 by NAT_1:13;
then A39: i - 1 < (i + 1) - 1 by XREAL_1:9;
A40: i in Seg j by A19, A35, FINSEQ_1:1;
then r1 = ((min (s1,(1 / 2))) / 2) * (i - 1) by A18, A36;
hence r1 < r2 by A33, A38, A39, 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 A18, A36, A40, A38
.= (min (s1,(1 / 2))) / 2 ;
hence r2 - r1 = (min (s1,(1 / 2))) / 2 ; ::_thesis: verum
end;
0 < min (s1,(1 / 2)) by A9, XXREAL_0:15;
then 0 < j by A15, XREAL_1:139;
then A41: 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 A18
.= 0 ;
then A42: h1 . 1 = 0 by A41, A30, Lm5;
2 * (min (s1,(1 / 2))) <> 0 by A9, XXREAL_0:15;
then A43: ( ((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 A44: 1 - (((min (s1,(1 / 2))) / 2) * (j - 1)) = ((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - [/(2 / (min (s1,(1 / 2))))\])) ;
A45: for r1 being Real st r1 = p . (len p) holds
1 - r1 <= (min (s1,(1 / 2))) / 2
proof
let r1 be Real; ::_thesis: ( r1 = p . (len p) implies 1 - r1 <= (min (s1,(1 / 2))) / 2 )
assume A46: r1 = p . (len p) ; ::_thesis: 1 - r1 <= (min (s1,(1 / 2))) / 2
len p in Seg j by A41, A30, FINSEQ_1:1;
hence 1 - r1 <= (min (s1,(1 / 2))) / 2 by A16, A18, A30, A44, A46; ::_thesis: verum
end;
A47: for i being Element of NAT st 1 <= i & i < len h1 holds
(h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len h1 implies (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 )
assume that
A48: 1 <= i and
A49: i < len h1 ; ::_thesis: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2
A50: i + 1 <= len h1 by A49, NAT_1:13;
A51: 1 < i + 1 by A48, NAT_1:13;
A52: i <= len p by A29, A49, NAT_1:13;
now__::_thesis:_(_(_i_<_len_p_&_(h1_/._(i_+_1))_-_(h1_/._i)_<=_(min_(s1,(1_/_2)))_/_2_)_or_(_i_>=_len_p_&_(h1_/._(i_+_1))_-_(h1_/._i)_<=_(min_(s1,(1_/_2)))_/_2_)_)
percases ( i < len p or i >= len p ) ;
caseA53: i < len p ; ::_thesis: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2
then i + 1 <= len p by NAT_1:13;
then A54: h1 . (i + 1) = p . (i + 1) by A51, FINSEQ_1:64;
A55: h1 . i = p . i by A48, A53, FINSEQ_1:64;
( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A48, A49, A50, A51, FINSEQ_4:15;
hence (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 by A34, A48, A53, A55, A54; ::_thesis: verum
end;
case i >= len p ; ::_thesis: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2
then A56: i = len p by A52, XXREAL_0:1;
A57: h1 /. i = h1 . i by A48, A49, FINSEQ_4:15
.= p . i by A48, A52, FINSEQ_1:64 ;
h1 /. (i + 1) = h1 . (i + 1) by A50, A51, FINSEQ_4:15
.= 1 by A56, Lm4 ;
hence (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 by A45, A56, A57; ::_thesis: verum
end;
end;
end;
hence (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 ; ::_thesis: verum
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 A58: ((min (s1,(1 / 2))) / 2) * (j - 1) < ((min (s1,(1 / 2))) / 2) * (2 / (min (s1,(1 / 2)))) by A33, XREAL_1:68;
A59: for i being Element of NAT
for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds
r1 < 1
proof
let i be Element of 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
A60: 1 <= i and
A61: i <= len p and
A62: r1 = p . i ; ::_thesis: r1 < 1
i - 1 <= j - 1 by A30, A61, XREAL_1:9;
then A63: ((min (s1,(1 / 2))) / 2) * (i - 1) <= ((min (s1,(1 / 2))) / 2) * (j - 1) by A11, XREAL_1:64;
i in Seg j by A19, A60, A61, FINSEQ_1:1;
then r1 = ((min (s1,(1 / 2))) / 2) * (i - 1) by A18, A62;
hence r1 < 1 by A58, A43, A63, XXREAL_0:2; ::_thesis: verum
end;
A64: for i being Element of NAT st 1 <= i & i < len h1 holds
h1 /. i < h1 /. (i + 1)
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len h1 implies h1 /. i < h1 /. (i + 1) )
assume that
A65: 1 <= i and
A66: i < len h1 ; ::_thesis: h1 /. i < h1 /. (i + 1)
A67: 1 < i + 1 by A65, NAT_1:13;
A68: i <= len p by A29, A66, NAT_1:13;
A69: i + 1 <= len h1 by A66, NAT_1:13;
now__::_thesis:_(_(_i_<_len_p_&_h1_/._i_<_h1_/._(i_+_1)_)_or_(_i_>=_len_p_&_h1_/._i_<_h1_/._(i_+_1)_)_)
percases ( i < len p or i >= len p ) ;
caseA70: i < len p ; ::_thesis: h1 /. i < h1 /. (i + 1)
then i + 1 <= len p by NAT_1:13;
then A71: h1 . (i + 1) = p . (i + 1) by A67, FINSEQ_1:64;
A72: h1 . i = p . i by A65, A70, FINSEQ_1:64;
( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A65, A66, A69, A67, FINSEQ_4:15;
hence h1 /. i < h1 /. (i + 1) by A34, A65, A70, A72, A71; ::_thesis: verum
end;
case i >= len p ; ::_thesis: h1 /. i < h1 /. (i + 1)
then A73: i = len p by A68, XXREAL_0:1;
A74: h1 /. i = h1 . i by A65, A66, FINSEQ_4:15
.= p . i by A65, A68, FINSEQ_1:64 ;
h1 /. (i + 1) = h1 . (i + 1) by A69, A67, FINSEQ_4:15
.= 1 by A73, Lm4 ;
hence h1 /. i < h1 /. (i + 1) by A59, A65, A68, A74; ::_thesis: verum
end;
end;
end;
hence h1 /. i < h1 /. (i + 1) ; ::_thesis: verum
end;
A75: e / 2 < e by A4, XREAL_1:216;
A76: for i being Element of 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 Element of 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
A77: ( 1 <= i & i < len h1 ) and
A78: Q = [.(h1 /. i),(h1 /. (i + 1)).] and
A79: W = g .: Q ; ::_thesis: diameter W < e
h1 /. i < h1 /. (i + 1) by A64, A77;
then A80: Q <> {} by A78, XXREAL_1:1;
A81: 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
A82: x in W and
A83: y in W ; ::_thesis: dist (x,y) <= e / 2
consider x3 being set such that
A84: x3 in dom g and
A85: x3 in Q and
A86: x = g . x3 by A79, A82, FUNCT_1:def_6;
reconsider x3 = x3 as Element of (Closed-Interval-MSpace (0,1)) by A84, Lm2, TOPMETR:12;
reconsider r3 = x3 as Real by A78, A85;
A87: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 by A47, A77;
consider y3 being set such that
A88: y3 in dom g and
A89: y3 in Q and
A90: y = g . y3 by A79, A83, FUNCT_1:def_6;
reconsider y3 = y3 as Element of (Closed-Interval-MSpace (0,1)) by A88, Lm2, TOPMETR:12;
reconsider s3 = y3 as Real by A78, A89;
A91: ( f . x3 = f /. x3 & f . y3 = f /. y3 ) ;
abs (r3 - s3) <= (h1 /. (i + 1)) - (h1 /. i) by A78, A85, A89, Th12;
then abs (r3 - s3) <= (min (s1,(1 / 2))) / 2 by A87, XXREAL_0:2;
then A92: dist (x3,y3) <= (min (s1,(1 / 2))) / 2 by HEINE:1;
(min (s1,(1 / 2))) / 2 < min (s1,(1 / 2)) by A11, A31, XREAL_1:216;
then dist (x3,y3) < min (s1,(1 / 2)) by A92, XXREAL_0:2;
hence dist (x,y) <= e / 2 by A14, A86, A90, A91; ::_thesis: verum
end;
then W is bounded by A6, TBSP_1:def_7;
then diameter W <= e / 2 by A8, A79, A80, A81, TBSP_1:def_8;
hence diameter W < e by A75, XXREAL_0:2; ::_thesis: verum
end;
A93: rng p c= [.0,1.]
proof
let y be set ; :: 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 set such that
A94: x in dom p and
A95: y = p . x by FUNCT_1:def_3;
reconsider nx = x as Element of NAT by A94;
A96: p . nx = ((min (s1,(1 / 2))) / 2) * (nx - 1) by A18, A94;
then reconsider ry = p . nx as Real ;
A97: x in Seg (len p) by A94, FINSEQ_1:def_3;
then A98: 1 <= nx by FINSEQ_1:1;
then A99: nx - 1 >= 1 - 1 by XREAL_1:9;
nx <= len p by A97, FINSEQ_1:1;
then ry < 1 by A59, A98;
then y in { rs where rs is Real : ( 0 <= rs & rs <= 1 ) } by A11, A95, A96, A99;
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 A100: rng h1 c= [.0,1.] \/ {1} by A93, XBOOLE_1:13;
h1 . (len h1) = 1 by A29, Lm4;
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 Element of 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 A29, A32, A42, A2, A100, A3, A64, A76, Lm7; ::_thesis: verum
end;
theorem :: UNIFORM1:14
for n being Element of NAT
for e being Real
for g being Function of I[01],(TOP-REAL n)
for p1, p2 being Element of (TOP-REAL n) st e > 0 & g is continuous holds
ex h being FinSequence of REAL st
( h . 1 = 1 & h . (len h) = 0 & 5 <= len h & rng h c= the carrier of I[01] & h is decreasing & ( for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. (i + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) )
proof
let n be Element of NAT ; ::_thesis: for e being Real
for g being Function of I[01],(TOP-REAL n)
for p1, p2 being Element of (TOP-REAL n) st e > 0 & g is continuous holds
ex h being FinSequence of REAL st
( h . 1 = 1 & h . (len h) = 0 & 5 <= len h & rng h c= the carrier of I[01] & h is decreasing & ( for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. (i + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) )
let e be Real; ::_thesis: for g being Function of I[01],(TOP-REAL n)
for p1, p2 being Element of (TOP-REAL n) st e > 0 & g is continuous holds
ex h being FinSequence of REAL st
( h . 1 = 1 & h . (len h) = 0 & 5 <= len h & rng h c= the carrier of I[01] & h is decreasing & ( for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. (i + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) )
let g be Function of I[01],(TOP-REAL n); ::_thesis: for p1, p2 being Element of (TOP-REAL n) st e > 0 & g is continuous holds
ex h being FinSequence of REAL st
( h . 1 = 1 & h . (len h) = 0 & 5 <= len h & rng h c= the carrier of I[01] & h is decreasing & ( for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. (i + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) )
let p1, p2 be Element of (TOP-REAL n); ::_thesis: ( e > 0 & g is continuous implies ex h being FinSequence of REAL st
( h . 1 = 1 & h . (len h) = 0 & 5 <= len h & rng h c= the carrier of I[01] & h is decreasing & ( for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. (i + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) ) )
A1: dom g = the carrier of I[01] by FUNCT_2:def_1;
A2: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider h = g as Function of I[01],(TopSpaceMetr (Euclid n)) ;
reconsider f = g as Function of (Closed-Interval-MSpace (0,1)),(Euclid n) by Lm3, EUCLID:67;
assume that
A3: e > 0 and
A4: g is continuous ; ::_thesis: ex h being FinSequence of REAL st
( h . 1 = 1 & h . (len h) = 0 & 5 <= len h & rng h c= the carrier of I[01] & h is decreasing & ( for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. (i + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) )
A5: e / 2 > 0 by A3, XREAL_1:215;
h is continuous by A4, A2, PRE_TOPC:33;
then f is uniformly_continuous by Lm1, Th7, TOPMETR:20;
then consider s1 being Real such that
A6: 0 < s1 and
A7: 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 A5, Def1;
set s = min (s1,(1 / 2));
defpred S1[ Nat, set ] means $2 = 1 - (((min (s1,(1 / 2))) / 2) * ($1 - 1));
A8: 0 <= min (s1,(1 / 2)) by A6, XXREAL_0:20;
then reconsider j = [/(2 / (min (s1,(1 / 2))))\] as Element of NAT by INT_1:53;
A9: 2 / (min (s1,(1 / 2))) <= j by INT_1:def_7;
A10: min (s1,(1 / 2)) <= s1 by XXREAL_0:17;
A11: 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 A10, XXREAL_0:2;
hence dist ((f /. u1),(f /. u2)) < e / 2 by A7; ::_thesis: verum
end;
A12: 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 A13: ((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - j)) <= ((min (s1,(1 / 2))) / 2) * 1 by A8, XREAL_1:64;
A14: for k being Nat st k in Seg j holds
ex x being set st S1[k,x] ;
consider p being FinSequence such that
A15: ( dom p = Seg j & ( for k being Nat st k in Seg j holds
S1[k,p . k] ) ) from FINSEQ_1:sch_1(A14);
A16: Seg (len p) = Seg j by A15, FINSEQ_1:def_3;
rng (p ^ <*0*>) c= REAL
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (p ^ <*0*>) or y in REAL )
A17: len (p ^ <*0*>) = (len p) + (len <*0*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
assume y in rng (p ^ <*0*>) ; ::_thesis: y in REAL
then consider x being set such that
A18: x in dom (p ^ <*0*>) and
A19: y = (p ^ <*0*>) . x by FUNCT_1:def_3;
reconsider nx = x as Element of NAT by A18;
A20: dom (p ^ <*0*>) = Seg (len (p ^ <*0*>)) by FINSEQ_1:def_3;
then A21: nx <= len (p ^ <*0*>) by A18, FINSEQ_1:1;
A22: 1 <= nx by A18, A20, FINSEQ_1:1;
A23: 1 <= nx by A18, A20, FINSEQ_1:1;
now__::_thesis:_(_(_nx_<_(len_p)_+_1_&_y_in_REAL_)_or_(_nx_>=_(len_p)_+_1_&_y_in_REAL_)_)
percases ( nx < (len p) + 1 or nx >= (len p) + 1 ) ;
case nx < (len p) + 1 ; ::_thesis: y in REAL
then A24: nx <= len p by NAT_1:13;
then nx in Seg j by A16, A22, FINSEQ_1:1;
then A25: p . nx = 1 - (((min (s1,(1 / 2))) / 2) * (nx - 1)) by A15;
y = p . nx by A19, A23, A24, FINSEQ_1:64;
hence y in REAL by A25; ::_thesis: verum
end;
case nx >= (len p) + 1 ; ::_thesis: y in REAL
then nx = (len p) + 1 by A21, A17, XXREAL_0:1;
then y = 0 by A19, Lm4;
hence y in REAL ; ::_thesis: verum
end;
end;
end;
hence y in REAL ; ::_thesis: verum
end;
then reconsider h1 = p ^ <*0*> as FinSequence of REAL by FINSEQ_1:def_4;
A26: len h1 = (len p) + (len <*0*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
A27: len p = j by A15, FINSEQ_1:def_3;
A28: min (s1,(1 / 2)) <> 0 by A6, XXREAL_0:15;
then 2 / (min (s1,(1 / 2))) >= 2 / (1 / 2) by A8, XREAL_1:118, XXREAL_0:17;
then 4 <= j by A9, XXREAL_0:2;
then A29: 4 + 1 <= (len p) + 1 by A27, XREAL_1:6;
A30: (min (s1,(1 / 2))) / 2 > 0 by A8, A28, XREAL_1:215;
A31: for i being Element of NAT
for r1, r2 being Real st 1 <= i & i < len p & r1 = p . i & r2 = p . (i + 1) holds
( r1 > r2 & r1 - r2 = (min (s1,(1 / 2))) / 2 )
proof
let i be Element of NAT ; ::_thesis: for r1, r2 being Real st 1 <= i & i < len p & r1 = p . i & r2 = p . (i + 1) holds
( r1 > r2 & r1 - r2 = (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 & r1 - r2 = (min (s1,(1 / 2))) / 2 ) )
assume that
A32: ( 1 <= i & i < len p ) and
A33: r1 = p . i and
A34: r2 = p . (i + 1) ; ::_thesis: ( r1 > r2 & r1 - r2 = (min (s1,(1 / 2))) / 2 )
i in Seg j by A16, A32, FINSEQ_1:1;
then A35: r1 = 1 - (((min (s1,(1 / 2))) / 2) * (i - 1)) by A15, A33;
( 1 < i + 1 & i + 1 <= len p ) by A32, NAT_1:13;
then i + 1 in Seg j by A16, FINSEQ_1:1;
then A36: r2 = 1 - (((min (s1,(1 / 2))) / 2) * ((i + 1) - 1)) by A15, A34;
i < i + 1 by NAT_1:13;
then i - 1 < (i + 1) - 1 by XREAL_1:9;
then ((min (s1,(1 / 2))) / 2) * (i - 1) < ((min (s1,(1 / 2))) / 2) * ((i + 1) - 1) by A30, XREAL_1:68;
hence r1 > r2 by A35, A36, XREAL_1:15; ::_thesis: r1 - r2 = (min (s1,(1 / 2))) / 2
thus r1 - r2 = (min (s1,(1 / 2))) / 2 by A35, A36; ::_thesis: verum
end;
0 < min (s1,(1 / 2)) by A6, XXREAL_0:15;
then 0 < j by A12, XREAL_1:139;
then A37: 0 + 1 <= j by NAT_1:13;
then 1 in Seg j by FINSEQ_1:1;
then p . 1 = 1 - (((min (s1,(1 / 2))) / 2) * (1 - 1)) by A15
.= 1 ;
then A38: h1 . 1 = 1 by A37, A27, Lm5;
2 * (min (s1,(1 / 2))) <> 0 by A6, XXREAL_0:15;
then A39: ( ((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 A40: 1 - (((min (s1,(1 / 2))) / 2) * (j - 1)) = ((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - [/(2 / (min (s1,(1 / 2))))\])) ;
A41: for r1 being Real st r1 = p . (len p) holds
r1 - 0 <= (min (s1,(1 / 2))) / 2
proof
let r1 be Real; ::_thesis: ( r1 = p . (len p) implies r1 - 0 <= (min (s1,(1 / 2))) / 2 )
assume A42: r1 = p . (len p) ; ::_thesis: r1 - 0 <= (min (s1,(1 / 2))) / 2
len p in Seg j by A37, A27, FINSEQ_1:1;
then r1 = 1 - (((min (s1,(1 / 2))) / 2) * ((len p) - 1)) by A15, A42;
hence r1 - 0 <= (min (s1,(1 / 2))) / 2 by A13, A15, A40, FINSEQ_1:def_3; ::_thesis: verum
end;
A43: for i being Element of NAT st 1 <= i & i < len h1 holds
(h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len h1 implies (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 )
assume that
A44: 1 <= i and
A45: i < len h1 ; ::_thesis: (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2
A46: i + 1 <= len h1 by A45, NAT_1:13;
A47: 1 < i + 1 by A44, NAT_1:13;
A48: i <= len p by A26, A45, NAT_1:13;
now__::_thesis:_(_(_i_<_len_p_&_(h1_/._i)_-_(h1_/._(i_+_1))_<=_(min_(s1,(1_/_2)))_/_2_)_or_(_i_>=_len_p_&_(h1_/._i)_-_(h1_/._(i_+_1))_<=_(min_(s1,(1_/_2)))_/_2_)_)
percases ( i < len p or i >= len p ) ;
caseA49: i < len p ; ::_thesis: (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2
then i + 1 <= len p by NAT_1:13;
then A50: h1 . (i + 1) = p . (i + 1) by A47, FINSEQ_1:64;
A51: h1 . i = p . i by A44, A49, FINSEQ_1:64;
( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A44, A45, A46, A47, FINSEQ_4:15;
hence (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 by A31, A44, A49, A51, A50; ::_thesis: verum
end;
case i >= len p ; ::_thesis: (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2
then A52: i = len p by A48, XXREAL_0:1;
A53: h1 /. i = h1 . i by A44, A45, FINSEQ_4:15
.= p . i by A44, A48, FINSEQ_1:64 ;
h1 /. (i + 1) = h1 . (i + 1) by A46, A47, FINSEQ_4:15
.= 0 by A52, Lm4 ;
hence (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 by A41, A52, A53; ::_thesis: verum
end;
end;
end;
hence (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 ; ::_thesis: verum
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 A54: ((min (s1,(1 / 2))) / 2) * (j - 1) < ((min (s1,(1 / 2))) / 2) * (2 / (min (s1,(1 / 2)))) by A30, XREAL_1:68;
A55: for i being Element of NAT
for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds
0 < r1
proof
let i be Element of NAT ; ::_thesis: for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds
0 < r1
let r1 be Real; ::_thesis: ( 1 <= i & i <= len p & r1 = p . i implies 0 < r1 )
assume that
A56: 1 <= i and
A57: i <= len p and
A58: r1 = p . i ; ::_thesis: 0 < r1
i - 1 <= j - 1 by A27, A57, XREAL_1:9;
then ((min (s1,(1 / 2))) / 2) * (i - 1) <= ((min (s1,(1 / 2))) / 2) * (j - 1) by A8, XREAL_1:64;
then ((min (s1,(1 / 2))) / 2) * (i - 1) < 1 by A54, A39, XXREAL_0:2;
then A59: 1 - (((min (s1,(1 / 2))) / 2) * (i - 1)) > 1 - 1 by XREAL_1:10;
i in Seg j by A16, A56, A57, FINSEQ_1:1;
hence 0 < r1 by A15, A58, A59; ::_thesis: verum
end;
A60: for i being Element of NAT st 1 <= i & i < len h1 holds
h1 /. i > h1 /. (i + 1)
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len h1 implies h1 /. i > h1 /. (i + 1) )
assume that
A61: 1 <= i and
A62: i < len h1 ; ::_thesis: h1 /. i > h1 /. (i + 1)
A63: 1 < i + 1 by A61, NAT_1:13;
A64: i <= len p by A26, A62, NAT_1:13;
A65: i + 1 <= len h1 by A62, NAT_1:13;
now__::_thesis:_(_(_i_<_len_p_&_h1_/._i_>_h1_/._(i_+_1)_)_or_(_i_>=_len_p_&_h1_/._i_>_h1_/._(i_+_1)_)_)
percases ( i < len p or i >= len p ) ;
caseA66: i < len p ; ::_thesis: h1 /. i > h1 /. (i + 1)
then i + 1 <= len p by NAT_1:13;
then A67: h1 . (i + 1) = p . (i + 1) by A63, FINSEQ_1:64;
A68: h1 . i = p . i by A61, A66, FINSEQ_1:64;
( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A61, A62, A65, A63, FINSEQ_4:15;
hence h1 /. i > h1 /. (i + 1) by A31, A61, A66, A68, A67; ::_thesis: verum
end;
case i >= len p ; ::_thesis: h1 /. i > h1 /. (i + 1)
then A69: i = len p by A64, XXREAL_0:1;
A70: h1 /. i = h1 . i by A61, A62, FINSEQ_4:15
.= p . i by A61, A64, FINSEQ_1:64 ;
h1 /. (i + 1) = h1 . (i + 1) by A65, A63, FINSEQ_4:15
.= 0 by A69, Lm4 ;
hence h1 /. i > h1 /. (i + 1) by A55, A61, A64, A70; ::_thesis: verum
end;
end;
end;
hence h1 /. i > h1 /. (i + 1) ; ::_thesis: verum
end;
A71: e / 2 < e by A3, XREAL_1:216;
A72: for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h1 & Q = [.(h1 /. (i + 1)),(h1 /. i).] & W = g .: Q holds
diameter W < e
proof
let i be Element of 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 + 1)),(h1 /. i).] & 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 + 1)),(h1 /. i).] & W = g .: Q holds
diameter W < e
let W be Subset of (Euclid n); ::_thesis: ( 1 <= i & i < len h1 & Q = [.(h1 /. (i + 1)),(h1 /. i).] & W = g .: Q implies diameter W < e )
assume that
A73: ( 1 <= i & i < len h1 ) and
A74: Q = [.(h1 /. (i + 1)),(h1 /. i).] and
A75: W = g .: Q ; ::_thesis: diameter W < e
h1 /. i > h1 /. (i + 1) by A60, A73;
then A76: Q <> {} by A74, XXREAL_1:1;
A77: 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
A78: x in W and
A79: y in W ; ::_thesis: dist (x,y) <= e / 2
consider x3 being set such that
A80: x3 in dom g and
A81: x3 in Q and
A82: x = g . x3 by A75, A78, FUNCT_1:def_6;
reconsider x3 = x3 as Element of (Closed-Interval-MSpace (0,1)) by A80, Lm2, TOPMETR:12;
reconsider r3 = x3 as Real by A74, A81;
A83: x = f /. x3 by A82;
consider y3 being set such that
A84: y3 in dom g and
A85: y3 in Q and
A86: y = g . y3 by A75, A79, FUNCT_1:def_6;
reconsider y3 = y3 as Element of (Closed-Interval-MSpace (0,1)) by A84, Lm2, TOPMETR:12;
reconsider s3 = y3 as Real by A74, A85;
A87: (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 by A43, A73;
abs (r3 - s3) <= (h1 /. i) - (h1 /. (i + 1)) by A74, A81, A85, Th12;
then A88: abs (r3 - s3) <= (min (s1,(1 / 2))) / 2 by A87, XXREAL_0:2;
( dist (x3,y3) = abs (r3 - s3) & (min (s1,(1 / 2))) / 2 < min (s1,(1 / 2)) ) by A8, A28, HEINE:1, XREAL_1:216;
then ( f . y3 = f /. y3 & dist (x3,y3) < min (s1,(1 / 2)) ) by A88, XXREAL_0:2;
hence dist (x,y) <= e / 2 by A11, A86, A83; ::_thesis: verum
end;
then W is bounded by A5, TBSP_1:def_7;
then diameter W <= e / 2 by A1, A75, A76, A77, TBSP_1:def_8;
hence diameter W < e by A71, XXREAL_0:2; ::_thesis: verum
end;
0 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then A89: 0 in [.0,1.] by RCOMP_1:def_1;
{0} c= [.0,1.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {0} or x in [.0,1.] )
assume x in {0} ; ::_thesis: x in [.0,1.]
hence x in [.0,1.] by A89, TARSKI:def_1; ::_thesis: verum
end;
then A90: [.0,1.] \/ {0} = [.0,1.] by XBOOLE_1:12;
Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:def_7;
then A91: the carrier of I[01] = the carrier of (Closed-Interval-MSpace (0,1)) by TOPMETR:12, TOPMETR:20
.= [.0,1.] by TOPMETR:10 ;
A92: rng p c= [.0,1.]
proof
let y be set ; :: 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 set such that
A93: x in dom p and
A94: y = p . x by FUNCT_1:def_3;
reconsider nx = x as Element of NAT by A93;
A95: p . nx = 1 - (((min (s1,(1 / 2))) / 2) * (nx - 1)) by A15, A93;
then reconsider ry = p . nx as Real ;
A96: x in Seg (len p) by A93, FINSEQ_1:def_3;
then A97: 1 <= nx by FINSEQ_1:1;
then nx - 1 >= 1 - 1 by XREAL_1:9;
then A98: 1 - (((min (s1,(1 / 2))) / 2) * (nx - 1)) <= 1 - 0 by A8, XREAL_1:6;
nx <= len p by A96, FINSEQ_1:1;
then 0 < ry by A55, A97;
then y in { rs where rs is Real : ( 0 <= rs & rs <= 1 ) } by A94, A95, A98;
hence y in [.0,1.] by RCOMP_1:def_1; ::_thesis: verum
end;
rng <*0*> = {0} by FINSEQ_1:38;
then rng h1 = (rng p) \/ {0} by FINSEQ_1:31;
then A99: rng h1 c= [.0,1.] \/ {0} by A92, XBOOLE_1:13;
h1 . (len h1) = 0 by A26, Lm4;
hence ex h being FinSequence of REAL st
( h . 1 = 1 & h . (len h) = 0 & 5 <= len h & rng h c= the carrier of I[01] & h is decreasing & ( for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. (i + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) ) by A26, A29, A38, A90, A99, A91, A60, A72, Lm8; ::_thesis: verum
end;