:: NORMSP_2 semantic presentation
begin
theorem :: NORMSP_2:1
for X being non empty MetrSpace
for Y being SetSequence of X st X is complete & union (rng Y) = the carrier of X & ( for n being Element of NAT holds (Y . n) ` in Family_open_set X ) holds
ex n0 being Element of NAT ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
proof
let X be non empty MetrSpace; ::_thesis: for Y being SetSequence of X st X is complete & union (rng Y) = the carrier of X & ( for n being Element of NAT holds (Y . n) ` in Family_open_set X ) holds
ex n0 being Element of NAT ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
let Y be SetSequence of X; ::_thesis: ( X is complete & union (rng Y) = the carrier of X & ( for n being Element of NAT holds (Y . n) ` in Family_open_set X ) implies ex n0 being Element of NAT ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 ) )
assume that
A1: X is complete and
A2: union (rng Y) = the carrier of X and
A3: for n being Element of NAT holds (Y . n) ` in Family_open_set X ; ::_thesis: ex n0 being Element of NAT ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
defpred S1[ Element of NAT , Point of X, Real, Point of X, Real] means ( 0 < $3 & $3 < 1 / (2 |^ $1) & (Ball ($2,$3)) /\ (Y . $1) = {} implies ( 0 < $5 & $5 < 1 / (2 |^ ($1 + 1)) & Ball ($4,$5) c= Ball ($2,($3 / 2)) & (Ball ($4,$5)) /\ (Y . ($1 + 1)) = {} ) );
assume A4: for n0 being Element of NAT
for r being Real
for x0 being Point of X holds
( not 0 < r or not Ball (x0,r) c= Y . n0 ) ; ::_thesis: contradiction
now__::_thesis:_not_(Y_._0)_`_=_{}
set x0 = the Point of X;
A5: ( ((Y . 0) `) ` = the carrier of X \ ((Y . 0) `) & Ball ( the Point of X,1) c= the carrier of X ) ;
assume (Y . 0) ` = {} ; ::_thesis: contradiction
hence contradiction by A4, A5; ::_thesis: verum
end;
then consider z0 being set such that
A6: z0 in (Y . 0) ` by XBOOLE_0:def_1;
reconsider z0 = z0 as Element of X by A6;
(Y . 0) ` in Family_open_set X by A3;
then consider t01 being Real such that
A7: 0 < t01 and
A8: Ball (z0,t01) c= (Y . 0) ` by A6, PCOMPS_1:def_4;
reconsider t0 = min (t01,(1 / 2)) as Real ;
t0 <= 1 / 2 by XXREAL_0:17;
then t0 < 1 / 1 by XXREAL_0:2;
then A9: t0 < 1 / (2 |^ 0) by NEWTON:4;
Ball (z0,t0) c= Ball (z0,t01) by PCOMPS_1:1, XXREAL_0:17;
then Ball (z0,t0) c= (Y . 0) ` by A8, XBOOLE_1:1;
then Ball (z0,t0) misses Y . 0 by SUBSET_1:23;
then A10: (Ball (z0,t0)) /\ (Y . 0) = {} by XBOOLE_0:def_7;
A11: for n being Element of NAT
for x being Point of X
for r being Real ex x1 being Point of X ex r1 being Real st
( 0 < r & r < 1 / (2 |^ n) & (Ball (x,r)) /\ (Y . n) = {} implies ( 0 < r1 & r1 < 1 / (2 |^ (n + 1)) & Ball (x1,r1) c= Ball (x,(r / 2)) & (Ball (x1,r1)) /\ (Y . (n + 1)) = {} ) )
proof
let n be Element of NAT ; ::_thesis: for x being Point of X
for r being Real ex x1 being Point of X ex r1 being Real st
( 0 < r & r < 1 / (2 |^ n) & (Ball (x,r)) /\ (Y . n) = {} implies ( 0 < r1 & r1 < 1 / (2 |^ (n + 1)) & Ball (x1,r1) c= Ball (x,(r / 2)) & (Ball (x1,r1)) /\ (Y . (n + 1)) = {} ) )
let x be Point of X; ::_thesis: for r being Real ex x1 being Point of X ex r1 being Real st
( 0 < r & r < 1 / (2 |^ n) & (Ball (x,r)) /\ (Y . n) = {} implies ( 0 < r1 & r1 < 1 / (2 |^ (n + 1)) & Ball (x1,r1) c= Ball (x,(r / 2)) & (Ball (x1,r1)) /\ (Y . (n + 1)) = {} ) )
let r be Real; ::_thesis: ex x1 being Point of X ex r1 being Real st
( 0 < r & r < 1 / (2 |^ n) & (Ball (x,r)) /\ (Y . n) = {} implies ( 0 < r1 & r1 < 1 / (2 |^ (n + 1)) & Ball (x1,r1) c= Ball (x,(r / 2)) & (Ball (x1,r1)) /\ (Y . (n + 1)) = {} ) )
now__::_thesis:_(_0_<_r_&_r_<_1_/_(2_|^_n)_&_(Ball_(x,r))_/\_(Y_._n)_=_{}_implies_ex_x1_being_Point_of_X_ex_r1_being_Real_st_S1[n,x,r,x1,r1]_)
0 < 2 |^ (n + 2) by NEWTON:83;
then A12: 0 < 1 / (2 |^ (n + 2)) by XREAL_1:139;
0 < 2 |^ (n + 1) by NEWTON:83;
then A13: (1 / (2 |^ (n + 1))) / 2 < 1 / (2 |^ (n + 1)) by XREAL_1:139, XREAL_1:216;
2 |^ (n + 2) = 2 |^ ((n + 1) + 1)
.= (2 |^ (n + 1)) * 2 by NEWTON:6 ;
then A14: 1 / (2 |^ (n + 2)) = (1 / (2 |^ (n + 1))) / 2 by XCMPLX_1:78;
assume that
A15: 0 < r and
r < 1 / (2 |^ n) and
(Ball (x,r)) /\ (Y . n) = {} ; ::_thesis: ex x1 being Point of X ex r1 being Real st S1[n,x,r,x1,r1]
not Ball (x,(r / 2)) c= Y . (n + 1) by A4, A15, XREAL_1:215;
then Ball (x,(r / 2)) meets (Y . (n + 1)) ` by SUBSET_1:24;
then consider z0 being set such that
A16: z0 in (Ball (x,(r / 2))) /\ ((Y . (n + 1)) `) by XBOOLE_0:4;
reconsider x1 = z0 as Point of X by A16;
A17: (Y . (n + 1)) ` in Family_open_set X by A3;
( Ball (x,(r / 2)) in Family_open_set X & (Y . (n + 1)) ` in Family_open_set X ) by A3, PCOMPS_1:29;
then (Ball (x,(r / 2))) /\ ((Y . (n + 1)) `) in Family_open_set X by PCOMPS_1:31;
then consider t02 being Real such that
A18: 0 < t02 and
A19: Ball (x1,t02) c= (Ball (x,(r / 2))) /\ ((Y . (n + 1)) `) by A16, PCOMPS_1:def_4;
A20: Ball (x1,t02) c= Ball (x,(r / 2)) by A19, XBOOLE_1:18;
x1 in (Y . (n + 1)) ` by A16, XBOOLE_0:def_4;
then consider t01 being Real such that
A21: 0 < t01 and
A22: Ball (x1,t01) c= (Y . (n + 1)) ` by A17, PCOMPS_1:def_4;
reconsider r1 = min ((min (t01,t02)),(1 / (2 |^ (n + 2)))) as Real ;
A23: r1 <= min (t01,t02) by XXREAL_0:17;
min (t01,t02) <= t02 by XXREAL_0:17;
then A24: Ball (x1,r1) c= Ball (x1,t02) by A23, PCOMPS_1:1, XXREAL_0:2;
min (t01,t02) <= t01 by XXREAL_0:17;
then Ball (x1,r1) c= Ball (x1,t01) by A23, PCOMPS_1:1, XXREAL_0:2;
then Ball (x1,r1) c= (Y . (n + 1)) ` by A22, XBOOLE_1:1;
then A25: Ball (x1,r1) misses Y . (n + 1) by SUBSET_1:23;
take x1 = x1; ::_thesis: ex r1 being Real st S1[n,x,r,x1,r1]
take r1 = r1; ::_thesis: S1[n,x,r,x1,r1]
A26: r1 <= 1 / (2 |^ (n + 2)) by XXREAL_0:17;
0 < min (t01,t02) by A21, A18, XXREAL_0:15;
hence S1[n,x,r,x1,r1] by A20, A14, A12, A13, A24, A25, A26, XBOOLE_0:def_7, XBOOLE_1:1, XXREAL_0:2, XXREAL_0:15; ::_thesis: verum
end;
hence ex x1 being Point of X ex r1 being Real st
( 0 < r & r < 1 / (2 |^ n) & (Ball (x,r)) /\ (Y . n) = {} implies ( 0 < r1 & r1 < 1 / (2 |^ (n + 1)) & Ball (x1,r1) c= Ball (x,(r / 2)) & (Ball (x1,r1)) /\ (Y . (n + 1)) = {} ) ) ; ::_thesis: verum
end;
ex x0 being sequence of X ex r0 being Real_Sequence st
( x0 . 0 = z0 & r0 . 0 = t0 & ( for n being Element of NAT st 0 < r0 . n & r0 . n < 1 / (2 |^ n) & (Ball ((x0 . n),(r0 . n))) /\ (Y . n) = {} holds
( 0 < r0 . (n + 1) & r0 . (n + 1) < 1 / (2 |^ (n + 1)) & Ball ((x0 . (n + 1)),(r0 . (n + 1))) c= Ball ((x0 . n),((r0 . n) / 2)) & (Ball ((x0 . (n + 1)),(r0 . (n + 1)))) /\ (Y . (n + 1)) = {} ) ) )
proof
defpred S2[ Element of NAT , Element of [: the carrier of X,REAL:], Element of [: the carrier of X,REAL:]] means ( 0 < $2 `2 & $2 `2 < 1 / (2 |^ $1) & (Ball (($2 `1),($2 `2))) /\ (Y . $1) = {} implies ( 0 < $3 `2 & $3 `2 < 1 / (2 |^ ($1 + 1)) & Ball (($3 `1),($3 `2)) c= Ball (($2 `1),(($2 `2) / 2)) & (Ball (($3 `1),($3 `2))) /\ (Y . ($1 + 1)) = {} ) );
A27: for n being Element of NAT
for u being Element of [: the carrier of X,REAL:] ex v being Element of [: the carrier of X,REAL:] st S2[n,u,v]
proof
let n be Element of NAT ; ::_thesis: for u being Element of [: the carrier of X,REAL:] ex v being Element of [: the carrier of X,REAL:] st S2[n,u,v]
let u be Element of [: the carrier of X,REAL:]; ::_thesis: ex v being Element of [: the carrier of X,REAL:] st S2[n,u,v]
consider v1 being Element of X, v2 being Element of REAL such that
A28: S1[n,u `1 ,u `2 ,v1,v2] by A11;
take [v1,v2] ; ::_thesis: S2[n,u,[v1,v2]]
[v1,v2] `1 = v1 by MCART_1:7;
hence S2[n,u,[v1,v2]] by A28, MCART_1:7; ::_thesis: verum
end;
consider f being Function of NAT,[: the carrier of X,REAL:] such that
A29: ( f . 0 = [z0,t0] & ( for n being Element of NAT holds S2[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A27);
take pr1 f ; ::_thesis: ex r0 being Real_Sequence st
( (pr1 f) . 0 = z0 & r0 . 0 = t0 & ( for n being Element of NAT st 0 < r0 . n & r0 . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),(r0 . n))) /\ (Y . n) = {} holds
( 0 < r0 . (n + 1) & r0 . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),(r0 . (n + 1))) c= Ball (((pr1 f) . n),((r0 . n) / 2)) & (Ball (((pr1 f) . (n + 1)),(r0 . (n + 1)))) /\ (Y . (n + 1)) = {} ) ) )
take pr2 f ; ::_thesis: ( (pr1 f) . 0 = z0 & (pr2 f) . 0 = t0 & ( for n being Element of NAT st 0 < (pr2 f) . n & (pr2 f) . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),((pr2 f) . n))) /\ (Y . n) = {} holds
( 0 < (pr2 f) . (n + 1) & (pr2 f) . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1))) c= Ball (((pr1 f) . n),(((pr2 f) . n) / 2)) & (Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1)))) /\ (Y . (n + 1)) = {} ) ) )
thus (pr1 f) . 0 = (f . 0) `1 by FUNCT_2:def_5
.= z0 by A29, MCART_1:7 ; ::_thesis: ( (pr2 f) . 0 = t0 & ( for n being Element of NAT st 0 < (pr2 f) . n & (pr2 f) . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),((pr2 f) . n))) /\ (Y . n) = {} holds
( 0 < (pr2 f) . (n + 1) & (pr2 f) . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1))) c= Ball (((pr1 f) . n),(((pr2 f) . n) / 2)) & (Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1)))) /\ (Y . (n + 1)) = {} ) ) )
thus (pr2 f) . 0 = (f . 0) `2 by FUNCT_2:def_6
.= t0 by A29, MCART_1:7 ; ::_thesis: for n being Element of NAT st 0 < (pr2 f) . n & (pr2 f) . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),((pr2 f) . n))) /\ (Y . n) = {} holds
( 0 < (pr2 f) . (n + 1) & (pr2 f) . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1))) c= Ball (((pr1 f) . n),(((pr2 f) . n) / 2)) & (Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1)))) /\ (Y . (n + 1)) = {} )
hereby ::_thesis: verum
let i be Element of NAT ; ::_thesis: S1[i,(pr1 f) . i,(pr2 f) . i,(pr1 f) . (i + 1),(pr2 f) . (i + 1)]
A30: ( (f . (i + 1)) `1 = (pr1 f) . (i + 1) & (f . (i + 1)) `2 = (pr2 f) . (i + 1) ) by FUNCT_2:def_5, FUNCT_2:def_6;
( (f . i) `1 = (pr1 f) . i & (f . i) `2 = (pr2 f) . i ) by FUNCT_2:def_5, FUNCT_2:def_6;
hence S1[i,(pr1 f) . i,(pr2 f) . i,(pr1 f) . (i + 1),(pr2 f) . (i + 1)] by A29, A30; ::_thesis: verum
end;
end;
then consider x0 being sequence of X, r0 being Real_Sequence such that
A31: ( x0 . 0 = z0 & r0 . 0 = t0 ) and
A32: for n being Element of NAT st 0 < r0 . n & r0 . n < 1 / (2 |^ n) & (Ball ((x0 . n),(r0 . n))) /\ (Y . n) = {} holds
( 0 < r0 . (n + 1) & r0 . (n + 1) < 1 / (2 |^ (n + 1)) & Ball ((x0 . (n + 1)),(r0 . (n + 1))) c= Ball ((x0 . n),((r0 . n) / 2)) & (Ball ((x0 . (n + 1)),(r0 . (n + 1)))) /\ (Y . (n + 1)) = {} ) ;
0 < 1 / 2 ;
then A33: 0 < t0 by A7, XXREAL_0:15;
A34: for n being Element of NAT holds
( 0 < r0 . n & r0 . n < 1 / (2 |^ n) & Ball ((x0 . (n + 1)),(r0 . (n + 1))) c= Ball ((x0 . n),((r0 . n) / 2)) & (Ball ((x0 . n),(r0 . n))) /\ (Y . n) = {} )
proof
defpred S2[ Element of NAT ] means ( 0 < r0 . $1 & r0 . $1 < 1 / (2 |^ $1) & Ball ((x0 . ($1 + 1)),(r0 . ($1 + 1))) c= Ball ((x0 . $1),((r0 . $1) / 2)) & (Ball ((x0 . $1),(r0 . $1))) /\ (Y . $1) = {} );
A35: now__::_thesis:_for_n_being_Element_of_NAT_st_S2[n]_holds_
S2[n_+_1]
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A36: S2[n] ; ::_thesis: S2[n + 1]
then A37: (Ball ((x0 . (n + 1)),(r0 . (n + 1)))) /\ (Y . (n + 1)) = {} by A32;
( 0 < r0 . (n + 1) & r0 . (n + 1) < 1 / (2 |^ (n + 1)) ) by A32, A36;
hence S2[n + 1] by A32, A37; ::_thesis: verum
end;
A38: S2[ 0 ] by A33, A9, A10, A31, A32;
thus for n being Element of NAT holds S2[n] from NAT_1:sch_1(A38, A35); ::_thesis: verum
end;
A39: for m, k being Element of NAT holds dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))
proof
let m be Element of NAT ; ::_thesis: for k being Element of NAT holds dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))
defpred S2[ Element of NAT ] means dist ((x0 . (m + $1)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ $1)));
A40: now__::_thesis:_for_k_being_Element_of_NAT_st_S2[k]_holds_
S2[k_+_1]
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume S2[k] ; ::_thesis: S2[k + 1]
then A41: (dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) + (dist ((x0 . (m + k)),(x0 . m))) <= (dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) by XREAL_1:6;
( 0 < r0 . ((m + k) + 1) & dist ((x0 . ((m + k) + 1)),(x0 . ((m + k) + 1))) = 0 ) by A34, METRIC_1:1;
then A42: x0 . ((m + k) + 1) in Ball ((x0 . ((m + k) + 1)),(r0 . ((m + k) + 1))) by METRIC_1:11;
r0 . (m + k) < 1 / (2 |^ (m + k)) by A34;
then (r0 . (m + k)) / 2 < (1 / (2 |^ (m + k))) / 2 by XREAL_1:74;
then (r0 . (m + k)) / 2 < 1 / ((2 |^ (m + k)) * 2) by XCMPLX_1:78;
then A43: (r0 . (m + k)) / 2 < 1 / (2 |^ ((m + k) + 1)) by NEWTON:6;
Ball ((x0 . ((m + k) + 1)),(r0 . ((m + k) + 1))) c= Ball ((x0 . (m + k)),((r0 . (m + k)) / 2)) by A34;
then dist ((x0 . ((m + k) + 1)),(x0 . (m + k))) < (r0 . (m + k)) / 2 by A42, METRIC_1:11;
then dist ((x0 . ((m + k) + 1)),(x0 . (m + k))) <= 1 / (2 |^ ((m + k) + 1)) by A43, XXREAL_0:2;
then A44: (dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) <= (1 / (2 |^ ((m + k) + 1))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) by XREAL_1:6;
2 |^ (m + (k + 1)) = (2 |^ m) * (2 |^ (k + 1)) by NEWTON:8;
then 1 / (2 |^ ((m + k) + 1)) = (1 / (2 |^ m)) / ((2 |^ (k + 1)) / 1) by XCMPLX_1:78
.= (1 / (2 |^ m)) * (1 / (2 |^ (k + 1))) by XCMPLX_1:79 ;
then A45: (1 / (2 |^ ((m + k) + 1))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) = (1 / (2 |^ m)) * (1 + ((1 / (2 |^ (k + 1))) - (1 / (2 |^ k))))
.= (1 / (2 |^ m)) * (1 + ((1 / ((2 |^ k) * 2)) - (1 / (2 |^ k)))) by NEWTON:6
.= (1 / (2 |^ m)) * (1 + (((1 / (2 |^ k)) / 2) - (1 / (2 |^ k)))) by XCMPLX_1:78
.= (1 / (2 |^ m)) * (1 - ((1 / (2 |^ k)) / 2))
.= (1 / (2 |^ m)) * (1 - (1 / ((2 |^ k) * 2))) by XCMPLX_1:78 ;
dist ((x0 . ((m + k) + 1)),(x0 . m)) <= (dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) + (dist ((x0 . (m + k)),(x0 . m))) by METRIC_1:4;
then dist ((x0 . (m + (k + 1))),(x0 . m)) <= (dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) by A41, XXREAL_0:2;
then dist ((x0 . (m + (k + 1))),(x0 . m)) <= (1 / (2 |^ ((m + k) + 1))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) by A44, XXREAL_0:2;
hence S2[k + 1] by A45, NEWTON:6; ::_thesis: verum
end;
2 |^ 0 = 1 by NEWTON:4;
then A46: S2[ 0 ] by METRIC_1:1;
for k being Element of NAT holds S2[k] from NAT_1:sch_1(A46, A40);
hence for k being Element of NAT holds dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k))) ; ::_thesis: verum
end;
A47: now__::_thesis:_for_m,_k_being_Element_of_NAT_holds_dist_((x0_._(m_+_k)),(x0_._m))_<_1_/_(2_|^_m)
let m be Element of NAT ; ::_thesis: for k being Element of NAT holds dist ((x0 . (m + k)),(x0 . m)) < 1 / (2 |^ m)
hereby ::_thesis: verum
let k be Element of NAT ; ::_thesis: dist ((x0 . (m + k)),(x0 . m)) < 1 / (2 |^ m)
A48: dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k))) by A39;
0 < 2 |^ k by NEWTON:83;
then 0 < 1 / (2 |^ k) by XREAL_1:139;
then A49: 1 - (1 / (2 |^ k)) < 1 - 0 by XREAL_1:10;
0 < 2 |^ m by NEWTON:83;
then 0 < 1 / (2 |^ m) by XREAL_1:139;
then (1 / (2 |^ m)) * (1 - (1 / (2 |^ k))) < (1 / (2 |^ m)) * 1 by A49, XREAL_1:68;
hence dist ((x0 . (m + k)),(x0 . m)) < 1 / (2 |^ m) by A48, XXREAL_0:2; ::_thesis: verum
end;
end;
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_p_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_p_&_m_>=_p_holds_
dist_((x0_._n),(x0_._m))_<_r
let r be Real; ::_thesis: ( 0 < r implies ex p being Element of NAT st
for n, m being Element of NAT st n >= p & m >= p holds
dist ((x0 . n),(x0 . m)) < r )
assume 0 < r ; ::_thesis: ex p being Element of NAT st
for n, m being Element of NAT st n >= p & m >= p holds
dist ((x0 . n),(x0 . m)) < r
then consider p1 being Element of NAT such that
A50: 1 / (2 |^ p1) <= r by PREPOWER:92;
take p = p1 + 1; ::_thesis: for n, m being Element of NAT st n >= p & m >= p holds
dist ((x0 . n),(x0 . m)) < r
hereby ::_thesis: verum
let n, m be Element of NAT ; ::_thesis: ( n >= p & m >= p implies dist ((x0 . n),(x0 . m)) < r )
assume that
A51: n >= p and
A52: m >= p ; ::_thesis: dist ((x0 . n),(x0 . m)) < r
consider k1 being Nat such that
A53: n = p + k1 by A51, NAT_1:10;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def_12;
n = p + k1 by A53;
then A54: dist ((x0 . n),(x0 . p)) < 1 / (2 |^ p) by A47;
consider k2 being Nat such that
A55: m = p + k2 by A52, NAT_1:10;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def_12;
A56: 1 / (2 |^ p) = 1 / ((2 |^ p1) * 2) by NEWTON:6
.= (1 / (2 |^ p1)) / 2 by XCMPLX_1:78 ;
m = p + k2 by A55;
then A57: (dist ((x0 . n),(x0 . p))) + (dist ((x0 . p),(x0 . m))) < (1 / (2 |^ p)) + (1 / (2 |^ p)) by A47, A54, XREAL_1:8;
dist ((x0 . n),(x0 . m)) <= (dist ((x0 . n),(x0 . p))) + (dist ((x0 . p),(x0 . m))) by METRIC_1:4;
then dist ((x0 . n),(x0 . m)) < 1 / (2 |^ p1) by A57, A56, XXREAL_0:2;
hence dist ((x0 . n),(x0 . m)) < r by A50, XXREAL_0:2; ::_thesis: verum
end;
end;
then x0 is Cauchy by TBSP_1:def_4;
then A58: x0 is convergent by A1, TBSP_1:def_5;
A59: for m, k being Element of NAT holds Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k))) c= Ball ((x0 . m),((r0 . m) / 2))
proof
let m be Element of NAT ; ::_thesis: for k being Element of NAT holds Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k))) c= Ball ((x0 . m),((r0 . m) / 2))
defpred S2[ Element of NAT ] means Ball ((x0 . ((m + 1) + $1)),(r0 . ((m + 1) + $1))) c= Ball ((x0 . m),((r0 . m) / 2));
A60: now__::_thesis:_for_k_being_Element_of_NAT_st_S2[k]_holds_
S2[k_+_1]
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A61: S2[k] ; ::_thesis: S2[k + 1]
0 < r0 . ((m + 1) + k) by A34;
then (r0 . ((m + 1) + k)) / 2 < r0 . ((m + 1) + k) by XREAL_1:216;
then A62: Ball ((x0 . ((m + 1) + k)),((r0 . ((m + 1) + k)) / 2)) c= Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k))) by PCOMPS_1:1;
Ball ((x0 . ((m + 1) + (k + 1))),(r0 . ((m + 1) + (k + 1)))) = Ball ((x0 . (((m + 1) + k) + 1)),(r0 . (((m + 1) + k) + 1))) ;
then Ball ((x0 . ((m + 1) + (k + 1))),(r0 . ((m + 1) + (k + 1)))) c= Ball ((x0 . ((m + 1) + k)),((r0 . ((m + 1) + k)) / 2)) by A34;
then Ball ((x0 . ((m + 1) + (k + 1))),(r0 . ((m + 1) + (k + 1)))) c= Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k))) by A62, XBOOLE_1:1;
hence S2[k + 1] by A61, XBOOLE_1:1; ::_thesis: verum
end;
A63: S2[ 0 ] by A34;
thus for k being Element of NAT holds S2[k] from NAT_1:sch_1(A63, A60); ::_thesis: verum
end;
A64: now__::_thesis:_for_m_being_Element_of_NAT_holds_lim_x0_in_Ball_((x0_._m),(r0_._m))
let m be Element of NAT ; ::_thesis: lim x0 in Ball ((x0 . m),(r0 . m))
set m1 = m + 1;
0 < r0 . m by A34;
then 0 < (r0 . m) / 2 by XREAL_1:215;
then consider n1 being Element of NAT such that
A65: for l being Element of NAT st n1 <= l holds
dist ((x0 . l),(lim x0)) < (r0 . m) / 2 by A58, TBSP_1:def_3;
reconsider n = max (n1,(m + 1)) as Element of NAT by XXREAL_0:16;
A66: dist ((x0 . n),(lim x0)) < (r0 . m) / 2 by A65, XXREAL_0:25;
consider k being Nat such that
A67: n = (m + 1) + k by NAT_1:10, XXREAL_0:25;
( dist ((x0 . n),(x0 . n)) = 0 & 0 < r0 . n ) by A34, METRIC_1:1;
then A68: x0 . n in Ball ((x0 . n),(r0 . n)) by METRIC_1:11;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
n = (m + 1) + k by A67;
then Ball ((x0 . n),(r0 . n)) c= Ball ((x0 . m),((r0 . m) / 2)) by A59;
then dist ((x0 . n),(x0 . m)) < (r0 . m) / 2 by A68, METRIC_1:11;
then A69: (dist ((lim x0),(x0 . n))) + (dist ((x0 . n),(x0 . m))) < ((r0 . m) / 2) + ((r0 . m) / 2) by A66, XREAL_1:8;
dist ((lim x0),(x0 . m)) <= (dist ((lim x0),(x0 . n))) + (dist ((x0 . n),(x0 . m))) by METRIC_1:4;
then dist ((lim x0),(x0 . m)) < ((r0 . m) / 2) + ((r0 . m) / 2) by A69, XXREAL_0:2;
hence lim x0 in Ball ((x0 . m),(r0 . m)) by METRIC_1:11; ::_thesis: verum
end;
A70: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_lim_x0_in_Y_._n
let n be Element of NAT ; ::_thesis: not lim x0 in Y . n
thus not lim x0 in Y . n ::_thesis: verum
proof
assume A71: lim x0 in Y . n ; ::_thesis: contradiction
lim x0 in Ball ((x0 . n),(r0 . n)) by A64;
then lim x0 in (Ball ((x0 . n),(r0 . n))) /\ (Y . n) by A71, XBOOLE_0:def_4;
hence contradiction by A34; ::_thesis: verum
end;
end;
not lim x0 in union (rng Y)
proof
assume lim x0 in union (rng Y) ; ::_thesis: contradiction
then consider A being set such that
A72: lim x0 in A and
A73: A in rng Y by TARSKI:def_4;
ex k being set st
( k in dom Y & A = Y . k ) by A73, FUNCT_1:def_3;
hence contradiction by A70, A72; ::_thesis: verum
end;
hence contradiction by A2; ::_thesis: verum
end;
begin
definition
let X be RealNormSpace;
func distance_by_norm_of X -> Function of [: the carrier of X, the carrier of X:],REAL means :Def1: :: NORMSP_2:def 1
for x, y being Point of X holds it . (x,y) = ||.(x - y).||;
existence
ex b1 being Function of [: the carrier of X, the carrier of X:],REAL st
for x, y being Point of X holds b1 . (x,y) = ||.(x - y).||
proof
set CX = the carrier of X;
deffunc H1( Element of the carrier of X, Element of the carrier of X) -> Element of REAL = ||.($1 - $2).||;
ex f being Function of [: the carrier of X, the carrier of X:],REAL st
for x, y being Element of the carrier of X holds f . (x,y) = H1(x,y) from BINOP_1:sch_4();
hence ex b1 being Function of [: the carrier of X, the carrier of X:],REAL st
for x, y being Point of X holds b1 . (x,y) = ||.(x - y).|| ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of [: the carrier of X, the carrier of X:],REAL st ( for x, y being Point of X holds b1 . (x,y) = ||.(x - y).|| ) & ( for x, y being Point of X holds b2 . (x,y) = ||.(x - y).|| ) holds
b1 = b2
proof
let dist1, dist2 be Function of [: the carrier of X, the carrier of X:],REAL; ::_thesis: ( ( for x, y being Point of X holds dist1 . (x,y) = ||.(x - y).|| ) & ( for x, y being Point of X holds dist2 . (x,y) = ||.(x - y).|| ) implies dist1 = dist2 )
assume that
A1: for x, y being Point of X holds dist1 . (x,y) = ||.(x - y).|| and
A2: for x, y being Point of X holds dist2 . (x,y) = ||.(x - y).|| ; ::_thesis: dist1 = dist2
now__::_thesis:_for_x,_y_being_Point_of_X_holds_dist1_._(x,y)_=_dist2_._(x,y)
let x, y be Point of X; ::_thesis: dist1 . (x,y) = dist2 . (x,y)
dist1 . (x,y) = ||.(x - y).|| by A1;
hence dist1 . (x,y) = dist2 . (x,y) by A2; ::_thesis: verum
end;
hence dist1 = dist2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines distance_by_norm_of NORMSP_2:def_1_:_
for X being RealNormSpace
for b2 being Function of [: the carrier of X, the carrier of X:],REAL holds
( b2 = distance_by_norm_of X iff for x, y being Point of X holds b2 . (x,y) = ||.(x - y).|| );
Lm1: for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is Reflexive
proof
let X be RealNormSpace; ::_thesis: the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is Reflexive
now__::_thesis:_for_a_being_Element_of_X_holds_(distance_by_norm_of_X)_._(a,a)_=_0
let a be Element of X; ::_thesis: (distance_by_norm_of X) . (a,a) = 0
thus (distance_by_norm_of X) . (a,a) = ||.(a - a).|| by Def1
.= 0 by NORMSP_1:6 ; ::_thesis: verum
end;
hence the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is Reflexive by METRIC_1:def_2; ::_thesis: verum
end;
Lm2: for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is discerning
proof
let X be RealNormSpace; ::_thesis: the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is discerning
now__::_thesis:_for_a,_b_being_Element_of_X_st_(distance_by_norm_of_X)_._(a,b)_=_0_holds_
a_=_b
let a, b be Element of X; ::_thesis: ( (distance_by_norm_of X) . (a,b) = 0 implies a = b )
assume A1: (distance_by_norm_of X) . (a,b) = 0 ; ::_thesis: a = b
(distance_by_norm_of X) . (a,b) = ||.(a - b).|| by Def1;
hence a = b by A1, NORMSP_1:6; ::_thesis: verum
end;
hence the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is discerning by METRIC_1:def_3; ::_thesis: verum
end;
Lm3: for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is symmetric
proof
let X be RealNormSpace; ::_thesis: the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is symmetric
now__::_thesis:_for_a,_b_being_Element_of_X_holds_(distance_by_norm_of_X)_._(a,b)_=_(distance_by_norm_of_X)_._(b,a)
let a, b be Element of X; ::_thesis: (distance_by_norm_of X) . (a,b) = (distance_by_norm_of X) . (b,a)
thus (distance_by_norm_of X) . (a,b) = ||.(a - b).|| by Def1
.= ||.(b - a).|| by NORMSP_1:7
.= (distance_by_norm_of X) . (b,a) by Def1 ; ::_thesis: verum
end;
hence the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is symmetric by METRIC_1:def_4; ::_thesis: verum
end;
Lm4: for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is triangle
proof
let X be RealNormSpace; ::_thesis: the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is triangle
now__::_thesis:_for_a,_b,_c_being_Element_of_X_holds_(distance_by_norm_of_X)_._(a,c)_<=_((distance_by_norm_of_X)_._(a,b))_+_((distance_by_norm_of_X)_._(b,c))
let a, b, c be Element of X; ::_thesis: (distance_by_norm_of X) . (a,c) <= ((distance_by_norm_of X) . (a,b)) + ((distance_by_norm_of X) . (b,c))
A1: ||.(a - c).|| <= ||.(a - b).|| + ||.(b - c).|| by NORMSP_1:10;
||.(a - b).|| + ||.(b - c).|| = ||.(a - b).|| + ((distance_by_norm_of X) . (b,c)) by Def1
.= ((distance_by_norm_of X) . (a,b)) + ((distance_by_norm_of X) . (b,c)) by Def1 ;
hence (distance_by_norm_of X) . (a,c) <= ((distance_by_norm_of X) . (a,b)) + ((distance_by_norm_of X) . (b,c)) by A1, Def1; ::_thesis: verum
end;
hence the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is triangle by METRIC_1:def_5; ::_thesis: verum
end;
definition
let X be RealNormSpace;
func MetricSpaceNorm X -> non empty MetrSpace equals :: NORMSP_2:def 2
MetrStruct(# the carrier of X,(distance_by_norm_of X) #);
coherence
MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is non empty MetrSpace
proof
( the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is Reflexive & the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is discerning & the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is symmetric & the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is triangle ) by Lm1, Lm2, Lm3, Lm4;
hence MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is non empty MetrSpace by METRIC_1:def_6, METRIC_1:def_7, METRIC_1:def_8, METRIC_1:def_9; ::_thesis: verum
end;
end;
:: deftheorem defines MetricSpaceNorm NORMSP_2:def_2_:_
for X being RealNormSpace holds MetricSpaceNorm X = MetrStruct(# the carrier of X,(distance_by_norm_of X) #);
theorem Th2: :: NORMSP_2:2
for X being RealNormSpace
for z being Element of (MetricSpaceNorm X)
for r being real number ex x being Point of X st
( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } )
proof
let X be RealNormSpace; ::_thesis: for z being Element of (MetricSpaceNorm X)
for r being real number ex x being Point of X st
( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } )
let z be Element of (MetricSpaceNorm X); ::_thesis: for r being real number ex x being Point of X st
( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } )
let r be real number ; ::_thesis: ex x being Point of X st
( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } )
set M = MetricSpaceNorm X;
reconsider x = z as Point of X ;
A1: Ball (z,r) = { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } by METRIC_1:def_14;
now__::_thesis:_for_a_being_set_st_a_in__{__y_where_y_is_Point_of_X_:_||.(x_-_y).||_<_r__}__holds_
a_in__{__q_where_q_is_Element_of_(MetricSpaceNorm_X)_:_dist_(z,q)_<_r__}_
let a be set ; ::_thesis: ( a in { y where y is Point of X : ||.(x - y).|| < r } implies a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } )
assume a in { y where y is Point of X : ||.(x - y).|| < r } ; ::_thesis: a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r }
then consider y being Point of X such that
A2: ( a = y & ||.(x - y).|| < r ) ;
reconsider t = y as Element of (MetricSpaceNorm X) ;
||.(x - y).|| = dist (z,t) by Def1;
hence a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } by A2; ::_thesis: verum
end;
then A3: { y where y is Point of X : ||.(x - y).|| < r } c= { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } by TARSKI:def_3;
now__::_thesis:_for_a_being_set_st_a_in__{__q_where_q_is_Element_of_(MetricSpaceNorm_X)_:_dist_(z,q)_<_r__}__holds_
a_in__{__y_where_y_is_Point_of_X_:_||.(x_-_y).||_<_r__}_
let a be set ; ::_thesis: ( a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } implies a in { y where y is Point of X : ||.(x - y).|| < r } )
assume a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } ; ::_thesis: a in { y where y is Point of X : ||.(x - y).|| < r }
then consider q being Element of (MetricSpaceNorm X) such that
A4: ( a = q & dist (z,q) < r ) ;
reconsider t = q as Point of X ;
||.(x - t).|| = dist (z,q) by Def1;
hence a in { y where y is Point of X : ||.(x - y).|| < r } by A4; ::_thesis: verum
end;
then { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } c= { y where y is Point of X : ||.(x - y).|| < r } by TARSKI:def_3;
then { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } = { y where y is Point of X : ||.(x - y).|| < r } by A3, XBOOLE_0:def_10;
hence ex x being Point of X st
( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } ) by A1; ::_thesis: verum
end;
theorem Th3: :: NORMSP_2:3
for X being RealNormSpace
for z being Element of (MetricSpaceNorm X)
for r being real number ex x being Point of X st
( x = z & cl_Ball (z,r) = { y where y is Point of X : ||.(x - y).|| <= r } )
proof
let X be RealNormSpace; ::_thesis: for z being Element of (MetricSpaceNorm X)
for r being real number ex x being Point of X st
( x = z & cl_Ball (z,r) = { y where y is Point of X : ||.(x - y).|| <= r } )
let z be Element of (MetricSpaceNorm X); ::_thesis: for r being real number ex x being Point of X st
( x = z & cl_Ball (z,r) = { y where y is Point of X : ||.(x - y).|| <= r } )
let r be real number ; ::_thesis: ex x being Point of X st
( x = z & cl_Ball (z,r) = { y where y is Point of X : ||.(x - y).|| <= r } )
reconsider x = z as Point of X ;
set M = MetricSpaceNorm X;
A1: cl_Ball (z,r) = { q where q is Element of (MetricSpaceNorm X) : dist (z,q) <= r } by METRIC_1:def_15;
now__::_thesis:_for_a_being_set_st_a_in__{__y_where_y_is_Point_of_X_:_||.(x_-_y).||_<=_r__}__holds_
a_in__{__q_where_q_is_Element_of_(MetricSpaceNorm_X)_:_dist_(z,q)_<=_r__}_
let a be set ; ::_thesis: ( a in { y where y is Point of X : ||.(x - y).|| <= r } implies a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) <= r } )
assume a in { y where y is Point of X : ||.(x - y).|| <= r } ; ::_thesis: a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) <= r }
then consider y being Point of X such that
A2: ( a = y & ||.(x - y).|| <= r ) ;
reconsider t = y as Element of (MetricSpaceNorm X) ;
||.(x - y).|| = dist (z,t) by Def1;
hence a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) <= r } by A2; ::_thesis: verum
end;
then A3: { y where y is Point of X : ||.(x - y).|| <= r } c= { q where q is Element of (MetricSpaceNorm X) : dist (z,q) <= r } by TARSKI:def_3;
now__::_thesis:_for_a_being_set_st_a_in__{__q_where_q_is_Element_of_(MetricSpaceNorm_X)_:_dist_(z,q)_<=_r__}__holds_
a_in__{__y_where_y_is_Point_of_X_:_||.(x_-_y).||_<=_r__}_
let a be set ; ::_thesis: ( a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) <= r } implies a in { y where y is Point of X : ||.(x - y).|| <= r } )
assume a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) <= r } ; ::_thesis: a in { y where y is Point of X : ||.(x - y).|| <= r }
then consider q being Element of (MetricSpaceNorm X) such that
A4: ( a = q & dist (z,q) <= r ) ;
reconsider t = q as Point of X ;
||.(x - t).|| = dist (z,q) by Def1;
hence a in { y where y is Point of X : ||.(x - y).|| <= r } by A4; ::_thesis: verum
end;
then { q where q is Element of (MetricSpaceNorm X) : dist (z,q) <= r } c= { y where y is Point of X : ||.(x - y).|| <= r } by TARSKI:def_3;
then { q where q is Element of (MetricSpaceNorm X) : dist (z,q) <= r } = { y where y is Point of X : ||.(x - y).|| <= r } by A3, XBOOLE_0:def_10;
hence ex x being Point of X st
( x = z & cl_Ball (z,r) = { y where y is Point of X : ||.(x - y).|| <= r } ) by A1; ::_thesis: verum
end;
theorem Th4: :: NORMSP_2:4
for X being RealNormSpace
for S being sequence of X
for St being sequence of (MetricSpaceNorm X)
for x being Point of X
for xt being Point of (MetricSpaceNorm X) st S = St & x = xt holds
( St is_convergent_in_metrspace_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
proof
let X be RealNormSpace; ::_thesis: for S being sequence of X
for St being sequence of (MetricSpaceNorm X)
for x being Point of X
for xt being Point of (MetricSpaceNorm X) st S = St & x = xt holds
( St is_convergent_in_metrspace_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
let S be sequence of X; ::_thesis: for St being sequence of (MetricSpaceNorm X)
for x being Point of X
for xt being Point of (MetricSpaceNorm X) st S = St & x = xt holds
( St is_convergent_in_metrspace_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
let St be sequence of (MetricSpaceNorm X); ::_thesis: for x being Point of X
for xt being Point of (MetricSpaceNorm X) st S = St & x = xt holds
( St is_convergent_in_metrspace_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
let x be Point of X; ::_thesis: for xt being Point of (MetricSpaceNorm X) st S = St & x = xt holds
( St is_convergent_in_metrspace_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
let xt be Point of (MetricSpaceNorm X); ::_thesis: ( S = St & x = xt implies ( St is_convergent_in_metrspace_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r ) )
assume A1: ( S = St & x = xt ) ; ::_thesis: ( St is_convergent_in_metrspace_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
A2: now__::_thesis:_(_(_for_r_being_Real_st_0_<_r_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
||.((S_._n)_-_x).||_<_r_)_implies_St_is_convergent_in_metrspace_to_xt_)
assume A3: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r ; ::_thesis: St is_convergent_in_metrspace_to xt
now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
dist_((St_._n),xt)_<_r
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((St . n),xt) < r )
assume r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((St . n),xt) < r
then consider m being Element of NAT such that
A4: for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r by A3;
take m = m; ::_thesis: for n being Element of NAT st m <= n holds
dist ((St . n),xt) < r
let n be Element of NAT ; ::_thesis: ( m <= n implies dist ((St . n),xt) < r )
assume m <= n ; ::_thesis: dist ((St . n),xt) < r
then ||.((S . n) - x).|| < r by A4;
hence dist ((St . n),xt) < r by A1, Def1; ::_thesis: verum
end;
hence St is_convergent_in_metrspace_to xt by METRIC_6:def_2; ::_thesis: verum
end;
now__::_thesis:_(_St_is_convergent_in_metrspace_to_xt_implies_for_r_being_Real_st_0_<_r_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
||.((S_._n)_-_x).||_<_r_)
assume A5: St is_convergent_in_metrspace_to xt ; ::_thesis: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
assume 0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r
then consider m being Element of NAT such that
A6: for n being Element of NAT st m <= n holds
dist ((St . n),xt) < r by A5, METRIC_6:def_2;
take m = m; ::_thesis: for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r
let n be Element of NAT ; ::_thesis: ( m <= n implies ||.((S . n) - x).|| < r )
assume m <= n ; ::_thesis: ||.((S . n) - x).|| < r
then dist ((St . n),xt) < r by A6;
hence ||.((S . n) - x).|| < r by A1, Def1; ::_thesis: verum
end;
hence ( St is_convergent_in_metrspace_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r ) by A2; ::_thesis: verum
end;
theorem Th5: :: NORMSP_2:5
for X being RealNormSpace
for S being sequence of X
for St being sequence of (MetricSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
proof
let X be RealNormSpace; ::_thesis: for S being sequence of X
for St being sequence of (MetricSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
let S be sequence of X; ::_thesis: for St being sequence of (MetricSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
let St be sequence of (MetricSpaceNorm X); ::_thesis: ( S = St implies ( St is convergent iff S is convergent ) )
assume A1: S = St ; ::_thesis: ( St is convergent iff S is convergent )
A2: now__::_thesis:_(_S_is_convergent_implies_St_is_convergent_)
assume S is convergent ; ::_thesis: St is convergent
then consider x being Point of X such that
A3: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r by NORMSP_1:def_6;
reconsider xt = x as Point of (MetricSpaceNorm X) ;
St is_convergent_in_metrspace_to xt by A1, A3, Th4;
hence St is convergent by METRIC_6:9; ::_thesis: verum
end;
now__::_thesis:_(_St_is_convergent_implies_S_is_convergent_)
assume St is convergent ; ::_thesis: S is convergent
then consider xt being Point of (MetricSpaceNorm X) such that
A4: St is_convergent_in_metrspace_to xt by METRIC_6:10;
reconsider x = xt as Point of X ;
for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r by A1, A4, Th4;
hence S is convergent by NORMSP_1:def_6; ::_thesis: verum
end;
hence ( St is convergent iff S is convergent ) by A2; ::_thesis: verum
end;
theorem Th6: :: NORMSP_2:6
for X being RealNormSpace
for S being sequence of X
for St being sequence of (MetricSpaceNorm X) st S = St & St is convergent holds
lim St = lim S
proof
let X be RealNormSpace; ::_thesis: for S being sequence of X
for St being sequence of (MetricSpaceNorm X) st S = St & St is convergent holds
lim St = lim S
let S be sequence of X; ::_thesis: for St being sequence of (MetricSpaceNorm X) st S = St & St is convergent holds
lim St = lim S
let St be sequence of (MetricSpaceNorm X); ::_thesis: ( S = St & St is convergent implies lim St = lim S )
assume that
A1: S = St and
A2: St is convergent ; ::_thesis: lim St = lim S
reconsider xt = lim S as Point of (MetricSpaceNorm X) ;
S is convergent by A1, A2, Th5;
then for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - (lim S)).|| < r by NORMSP_1:def_7;
then St is_convergent_in_metrspace_to xt by A1, Th4;
hence lim St = lim S by METRIC_6:11; ::_thesis: verum
end;
begin
definition
let X be RealNormSpace;
func TopSpaceNorm X -> non empty TopSpace equals :: NORMSP_2:def 3
TopSpaceMetr (MetricSpaceNorm X);
coherence
TopSpaceMetr (MetricSpaceNorm X) is non empty TopSpace ;
end;
:: deftheorem defines TopSpaceNorm NORMSP_2:def_3_:_
for X being RealNormSpace holds TopSpaceNorm X = TopSpaceMetr (MetricSpaceNorm X);
theorem Th7: :: NORMSP_2:7
for X being RealNormSpace
for V being Subset of (TopSpaceNorm X) holds
( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )
proof
let X be RealNormSpace; ::_thesis: for V being Subset of (TopSpaceNorm X) holds
( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )
let V be Subset of (TopSpaceNorm X); ::_thesis: ( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )
A1: now__::_thesis:_(_(_for_x_being_Point_of_X_st_x_in_V_holds_
ex_r_being_Real_st_
(_r_>_0_&__{__y_where_y_is_Point_of_X_:_||.(x_-_y).||_<_r__}__c=_V_)_)_implies_(_V_in_the_topology_of_(TopSpaceNorm_X)_&_V_is_open_)_)
assume A2: for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) ; ::_thesis: ( V in the topology of (TopSpaceNorm X) & V is open )
now__::_thesis:_for_z_being_Element_of_(MetricSpaceNorm_X)_st_z_in_V_holds_
ex_r_being_Real_st_
(_r_>_0_&_Ball_(z,r)_c=_V_)
let z be Element of (MetricSpaceNorm X); ::_thesis: ( z in V implies ex r being Real st
( r > 0 & Ball (z,r) c= V ) )
reconsider x = z as Point of X ;
assume z in V ; ::_thesis: ex r being Real st
( r > 0 & Ball (z,r) c= V )
then consider r being Real such that
A3: ( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) by A2;
take r = r; ::_thesis: ( r > 0 & Ball (z,r) c= V )
ex t being Point of X st
( t = z & Ball (z,r) = { y where y is Point of X : ||.(t - y).|| < r } ) by Th2;
hence ( r > 0 & Ball (z,r) c= V ) by A3; ::_thesis: verum
end;
hence V in the topology of (TopSpaceNorm X) by PCOMPS_1:def_4; ::_thesis: V is open
hence V is open by PRE_TOPC:def_2; ::_thesis: verum
end;
now__::_thesis:_(_V_is_open_implies_for_x_being_Point_of_X_st_x_in_V_holds_
ex_r_being_Real_st_
(_r_>_0_&__{__y_where_y_is_Point_of_X_:_||.(x_-_y).||_<_r__}__c=_V_)_)
assume A4: V is open ; ::_thesis: for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V )
hereby ::_thesis: verum
let x be Point of X; ::_thesis: ( x in V implies ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )
assume A5: x in V ; ::_thesis: ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V )
reconsider z = x as Element of (MetricSpaceNorm X) ;
V in the topology of (TopSpaceNorm X) by A4, PRE_TOPC:def_2;
then consider r being Real such that
A6: ( r > 0 & Ball (z,r) c= V ) by A5, PCOMPS_1:def_4;
take r = r; ::_thesis: ( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V )
ex t being Point of X st
( t = z & Ball (z,r) = { y where y is Point of X : ||.(t - y).|| < r } ) by Th2;
hence ( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) by A6; ::_thesis: verum
end;
end;
hence ( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) ) by A1; ::_thesis: verum
end;
theorem Th8: :: NORMSP_2:8
for X being RealNormSpace
for x being Point of X
for r being Real holds { y where y is Point of X : ||.(x - y).|| < r } is open Subset of (TopSpaceNorm X)
proof
let X be RealNormSpace; ::_thesis: for x being Point of X
for r being Real holds { y where y is Point of X : ||.(x - y).|| < r } is open Subset of (TopSpaceNorm X)
let x be Point of X; ::_thesis: for r being Real holds { y where y is Point of X : ||.(x - y).|| < r } is open Subset of (TopSpaceNorm X)
let r be Real; ::_thesis: { y where y is Point of X : ||.(x - y).|| < r } is open Subset of (TopSpaceNorm X)
reconsider z = x as Element of (MetricSpaceNorm X) ;
( ex t being Point of X st
( t = x & Ball (z,r) = { y where y is Point of X : ||.(t - y).|| < r } ) & Ball (z,r) in Family_open_set (MetricSpaceNorm X) ) by Th2, PCOMPS_1:29;
hence { y where y is Point of X : ||.(x - y).|| < r } is open Subset of (TopSpaceNorm X) by PRE_TOPC:def_2; ::_thesis: verum
end;
theorem :: NORMSP_2:9
for X being RealNormSpace
for x being Point of X
for r being Real holds { y where y is Point of X : ||.(x - y).|| <= r } is closed Subset of (TopSpaceNorm X)
proof
let X be RealNormSpace; ::_thesis: for x being Point of X
for r being Real holds { y where y is Point of X : ||.(x - y).|| <= r } is closed Subset of (TopSpaceNorm X)
let x be Point of X; ::_thesis: for r being Real holds { y where y is Point of X : ||.(x - y).|| <= r } is closed Subset of (TopSpaceNorm X)
let r be Real; ::_thesis: { y where y is Point of X : ||.(x - y).|| <= r } is closed Subset of (TopSpaceNorm X)
reconsider z = x as Element of (MetricSpaceNorm X) ;
ex t being Point of X st
( t = x & cl_Ball (z,r) = { y where y is Point of X : ||.(t - y).|| <= r } ) by Th3;
hence { y where y is Point of X : ||.(x - y).|| <= r } is closed Subset of (TopSpaceNorm X) by TOPREAL6:57; ::_thesis: verum
end;
theorem :: NORMSP_2:10
for X being non empty Hausdorff TopSpace st X is locally-compact holds
X is Baire
proof
let X be non empty Hausdorff TopSpace; ::_thesis: ( X is locally-compact implies X is Baire )
assume X is locally-compact ; ::_thesis: X is Baire
then ( X is sober & X is locally-compact ) by YELLOW_8:22;
hence X is Baire by WAYBEL12:44; ::_thesis: verum
end;
theorem :: NORMSP_2:11
for X being RealNormSpace holds TopSpaceNorm X is sequential ;
registration
let X be RealNormSpace;
cluster TopSpaceNorm X -> non empty sequential ;
coherence
TopSpaceNorm X is sequential ;
end;
theorem Th12: :: NORMSP_2:12
for X being RealNormSpace
for S being sequence of X
for St being sequence of (TopSpaceNorm X)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
proof
let X be RealNormSpace; ::_thesis: for S being sequence of X
for St being sequence of (TopSpaceNorm X)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
let S be sequence of X; ::_thesis: for St being sequence of (TopSpaceNorm X)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
let St be sequence of (TopSpaceNorm X); ::_thesis: for x being Point of X
for xt being Point of (TopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
let x be Point of X; ::_thesis: for xt being Point of (TopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
let xt be Point of (TopSpaceNorm X); ::_thesis: ( S = St & x = xt implies ( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r ) )
assume that
A1: S = St and
A2: x = xt ; ::_thesis: ( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
reconsider Sm = St as sequence of (MetricSpaceNorm X) ;
reconsider xm = x as Point of (MetricSpaceNorm X) ;
( St is_convergent_to xt iff Sm is_convergent_in_metrspace_to xm ) by A2, FRECHET2:28;
hence ( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r ) by A1, Th4; ::_thesis: verum
end;
theorem Th13: :: NORMSP_2:13
for X being RealNormSpace
for S being sequence of X
for St being sequence of (TopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
proof
let X be RealNormSpace; ::_thesis: for S being sequence of X
for St being sequence of (TopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
let S be sequence of X; ::_thesis: for St being sequence of (TopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
let St be sequence of (TopSpaceNorm X); ::_thesis: ( S = St implies ( St is convergent iff S is convergent ) )
reconsider Sm = St as sequence of (MetricSpaceNorm X) ;
A1: ( St is convergent iff Sm is convergent ) by FRECHET2:29;
assume S = St ; ::_thesis: ( St is convergent iff S is convergent )
hence ( St is convergent iff S is convergent ) by A1, Th5; ::_thesis: verum
end;
theorem Th14: :: NORMSP_2:14
for X being RealNormSpace
for S being sequence of X
for St being sequence of (TopSpaceNorm X) st S = St & St is convergent holds
( Lim St = {(lim S)} & lim St = lim S )
proof
let X be RealNormSpace; ::_thesis: for S being sequence of X
for St being sequence of (TopSpaceNorm X) st S = St & St is convergent holds
( Lim St = {(lim S)} & lim St = lim S )
let S be sequence of X; ::_thesis: for St being sequence of (TopSpaceNorm X) st S = St & St is convergent holds
( Lim St = {(lim S)} & lim St = lim S )
let St be sequence of (TopSpaceNorm X); ::_thesis: ( S = St & St is convergent implies ( Lim St = {(lim S)} & lim St = lim S ) )
assume that
A1: S = St and
A2: St is convergent ; ::_thesis: ( Lim St = {(lim S)} & lim St = lim S )
consider x being Point of (TopSpaceNorm X) such that
A3: Lim St = {x} by A2, FRECHET2:24;
reconsider Sm = St as sequence of (MetricSpaceNorm X) ;
A4: Sm is convergent by A2, FRECHET2:29;
then A5: lim St = lim Sm by FRECHET2:30
.= lim S by A1, A4, Th6 ;
x in Lim St by A3, TARSKI:def_1;
then St is_convergent_to x by FRECHET:def_5;
hence Lim St = {(lim S)} by A5, A3, FRECHET2:25; ::_thesis: lim St = lim S
thus lim St = lim S by A5; ::_thesis: verum
end;
theorem Th15: :: NORMSP_2:15
for X being RealNormSpace
for V being Subset of X
for Vt being Subset of (TopSpaceNorm X) st V = Vt holds
( V is closed iff Vt is closed )
proof
let X be RealNormSpace; ::_thesis: for V being Subset of X
for Vt being Subset of (TopSpaceNorm X) st V = Vt holds
( V is closed iff Vt is closed )
let V be Subset of X; ::_thesis: for Vt being Subset of (TopSpaceNorm X) st V = Vt holds
( V is closed iff Vt is closed )
let Vt be Subset of (TopSpaceNorm X); ::_thesis: ( V = Vt implies ( V is closed iff Vt is closed ) )
assume A1: V = Vt ; ::_thesis: ( V is closed iff Vt is closed )
hereby ::_thesis: ( Vt is closed implies V is closed )
assume A2: V is closed ; ::_thesis: Vt is closed
now__::_thesis:_for_St_being_sequence_of_(TopSpaceNorm_X)_st_St_is_convergent_&_rng_St_c=_Vt_holds_
Lim_St_c=_Vt
let St be sequence of (TopSpaceNorm X); ::_thesis: ( St is convergent & rng St c= Vt implies Lim St c= Vt )
assume that
A3: St is convergent and
A4: rng St c= Vt ; ::_thesis: Lim St c= Vt
reconsider S = St as sequence of X ;
S is convergent by A3, Th13;
then lim S in V by A1, A2, A4, NFCONT_1:def_3;
then {(lim S)} c= V by ZFMISC_1:31;
hence Lim St c= Vt by A1, A3, Th14; ::_thesis: verum
end;
hence Vt is closed by FRECHET:def_7; ::_thesis: verum
end;
assume A5: Vt is closed ; ::_thesis: V is closed
now__::_thesis:_for_S_being_sequence_of_X_st_rng_S_c=_V_&_S_is_convergent_holds_
lim_S_in_V
let S be sequence of X; ::_thesis: ( rng S c= V & S is convergent implies lim S in V )
assume that
A6: rng S c= V and
A7: S is convergent ; ::_thesis: lim S in V
reconsider St = S as sequence of (TopSpaceNorm X) ;
A8: St is convergent by A7, Th13;
then Lim St c= Vt by A1, A5, A6, FRECHET:def_7;
then {(lim S)} c= V by A1, A8, Th14;
hence lim S in V by ZFMISC_1:31; ::_thesis: verum
end;
hence V is closed by NFCONT_1:def_3; ::_thesis: verum
end;
theorem Th16: :: NORMSP_2:16
for X being RealNormSpace
for V being Subset of X
for Vt being Subset of (TopSpaceNorm X) st V = Vt holds
( V is open iff Vt is open )
proof
let X be RealNormSpace; ::_thesis: for V being Subset of X
for Vt being Subset of (TopSpaceNorm X) st V = Vt holds
( V is open iff Vt is open )
let V be Subset of X; ::_thesis: for Vt being Subset of (TopSpaceNorm X) st V = Vt holds
( V is open iff Vt is open )
let Vt be Subset of (TopSpaceNorm X); ::_thesis: ( V = Vt implies ( V is open iff Vt is open ) )
A1: ( V is open iff V ` is closed ) by NFCONT_1:def_4;
assume V = Vt ; ::_thesis: ( V is open iff Vt is open )
then ( V is open iff Vt ` is closed ) by A1, Th15;
hence ( V is open iff Vt is open ) by TOPS_1:4; ::_thesis: verum
end;
Lm5: for X being RealNormSpace
for r being Real
for x being Point of X holds { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r }
proof
let X be RealNormSpace; ::_thesis: for r being Real
for x being Point of X holds { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r }
let r be Real; ::_thesis: for x being Point of X holds { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r }
let x be Point of X; ::_thesis: { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r }
now__::_thesis:_for_s_being_set_st_s_in__{__y_where_y_is_Point_of_X_:_||.(y_-_x).||_<_r__}__holds_
s_in__{__y_where_y_is_Point_of_X_:_||.(x_-_y).||_<_r__}_
let s be set ; ::_thesis: ( s in { y where y is Point of X : ||.(y - x).|| < r } implies s in { y where y is Point of X : ||.(x - y).|| < r } )
assume s in { y where y is Point of X : ||.(y - x).|| < r } ; ::_thesis: s in { y where y is Point of X : ||.(x - y).|| < r }
then consider z being Point of X such that
A1: s = z and
A2: ||.(z - x).|| < r ;
||.(x - z).|| < r by A2, NORMSP_1:7;
hence s in { y where y is Point of X : ||.(x - y).|| < r } by A1; ::_thesis: verum
end;
then A3: { y where y is Point of X : ||.(y - x).|| < r } c= { y where y is Point of X : ||.(x - y).|| < r } by TARSKI:def_3;
now__::_thesis:_for_s_being_set_st_s_in__{__y_where_y_is_Point_of_X_:_||.(x_-_y).||_<_r__}__holds_
s_in__{__y_where_y_is_Point_of_X_:_||.(y_-_x).||_<_r__}_
let s be set ; ::_thesis: ( s in { y where y is Point of X : ||.(x - y).|| < r } implies s in { y where y is Point of X : ||.(y - x).|| < r } )
assume s in { y where y is Point of X : ||.(x - y).|| < r } ; ::_thesis: s in { y where y is Point of X : ||.(y - x).|| < r }
then consider z being Point of X such that
A4: s = z and
A5: ||.(x - z).|| < r ;
||.(z - x).|| < r by A5, NORMSP_1:7;
hence s in { y where y is Point of X : ||.(y - x).|| < r } by A4; ::_thesis: verum
end;
then { y where y is Point of X : ||.(x - y).|| < r } c= { y where y is Point of X : ||.(y - x).|| < r } by TARSKI:def_3;
hence { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r } by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th17: :: NORMSP_2:17
for X being RealNormSpace
for U being Subset of X
for Ut being Subset of (TopSpaceNorm X)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st U = Ut & x = xt holds
( U is Neighbourhood of x iff Ut is a_neighborhood of xt )
proof
let X be RealNormSpace; ::_thesis: for U being Subset of X
for Ut being Subset of (TopSpaceNorm X)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st U = Ut & x = xt holds
( U is Neighbourhood of x iff Ut is a_neighborhood of xt )
let U be Subset of X; ::_thesis: for Ut being Subset of (TopSpaceNorm X)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st U = Ut & x = xt holds
( U is Neighbourhood of x iff Ut is a_neighborhood of xt )
let Ut be Subset of (TopSpaceNorm X); ::_thesis: for x being Point of X
for xt being Point of (TopSpaceNorm X) st U = Ut & x = xt holds
( U is Neighbourhood of x iff Ut is a_neighborhood of xt )
let x be Point of X; ::_thesis: for xt being Point of (TopSpaceNorm X) st U = Ut & x = xt holds
( U is Neighbourhood of x iff Ut is a_neighborhood of xt )
let xt be Point of (TopSpaceNorm X); ::_thesis: ( U = Ut & x = xt implies ( U is Neighbourhood of x iff Ut is a_neighborhood of xt ) )
assume that
A1: U = Ut and
A2: x = xt ; ::_thesis: ( U is Neighbourhood of x iff Ut is a_neighborhood of xt )
A3: now__::_thesis:_(_U_is_Neighbourhood_of_x_implies_Ut_is_a_neighborhood_of_xt_)
assume U is Neighbourhood of x ; ::_thesis: Ut is a_neighborhood of xt
then consider r being Real such that
A4: r > 0 and
A5: { y where y is Point of X : ||.(y - x).|| < r } c= U by NFCONT_1:def_1;
now__::_thesis:_for_s_being_set_st_s_in__{__y_where_y_is_Point_of_X_:_||.(y_-_x).||_<_r__}__holds_
s_in_the_carrier_of_X
let s be set ; ::_thesis: ( s in { y where y is Point of X : ||.(y - x).|| < r } implies s in the carrier of X )
assume s in { y where y is Point of X : ||.(y - x).|| < r } ; ::_thesis: s in the carrier of X
then ex z being Point of X st
( s = z & ||.(z - x).|| < r ) ;
hence s in the carrier of X ; ::_thesis: verum
end;
then reconsider Vt = { y where y is Point of X : ||.(y - x).|| < r } as Subset of (TopSpaceNorm X) by TARSKI:def_3;
Vt = { y where y is Point of X : ||.(x - y).|| < r } by Lm5;
then A6: Vt is open by Th8;
||.(x - x).|| = 0 by NORMSP_1:6;
then xt in Vt by A2, A4;
hence Ut is a_neighborhood of xt by A1, A5, A6, CONNSP_2:6; ::_thesis: verum
end;
now__::_thesis:_(_Ut_is_a_neighborhood_of_xt_implies_U_is_Neighbourhood_of_x_)
assume Ut is a_neighborhood of xt ; ::_thesis: U is Neighbourhood of x
then consider Vt being Subset of (TopSpaceNorm X) such that
A7: Vt is open and
A8: Vt c= Ut and
A9: xt in Vt by CONNSP_2:6;
consider r being Real such that
A10: r > 0 and
A11: { y where y is Point of X : ||.(x - y).|| < r } c= Vt by A2, A7, A9, Th7;
A12: { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r } by Lm5;
{ y where y is Point of X : ||.(x - y).|| < r } c= U by A1, A8, A11, XBOOLE_1:1;
hence U is Neighbourhood of x by A10, A12, NFCONT_1:def_1; ::_thesis: verum
end;
hence ( U is Neighbourhood of x iff Ut is a_neighborhood of xt ) by A3; ::_thesis: verum
end;
theorem Th18: :: NORMSP_2:18
for X, Y being RealNormSpace
for f being PartFunc of X,Y
for ft being Function of (TopSpaceNorm X),(TopSpaceNorm Y)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_in x iff ft is_continuous_at xt )
proof
let X, Y be RealNormSpace; ::_thesis: for f being PartFunc of X,Y
for ft being Function of (TopSpaceNorm X),(TopSpaceNorm Y)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_in x iff ft is_continuous_at xt )
let f be PartFunc of X,Y; ::_thesis: for ft being Function of (TopSpaceNorm X),(TopSpaceNorm Y)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_in x iff ft is_continuous_at xt )
let ft be Function of (TopSpaceNorm X),(TopSpaceNorm Y); ::_thesis: for x being Point of X
for xt being Point of (TopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_in x iff ft is_continuous_at xt )
let x be Point of X; ::_thesis: for xt being Point of (TopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_in x iff ft is_continuous_at xt )
let xt be Point of (TopSpaceNorm X); ::_thesis: ( f = ft & x = xt implies ( f is_continuous_in x iff ft is_continuous_at xt ) )
assume that
A1: f = ft and
A2: x = xt ; ::_thesis: ( f is_continuous_in x iff ft is_continuous_at xt )
A3: dom f = the carrier of X by A1, FUNCT_2:def_1;
then A4: ft . xt = f /. x by A1, A2, PARTFUN1:def_6;
hereby ::_thesis: ( ft is_continuous_at xt implies f is_continuous_in x )
assume A5: f is_continuous_in x ; ::_thesis: ft is_continuous_at xt
now__::_thesis:_for_G_being_a_neighborhood_of_ft_._xt_ex_H_being_a_neighborhood_of_xt_st_ft_.:_H_c=_G
let G be a_neighborhood of ft . xt; ::_thesis: ex H being a_neighborhood of xt st ft .: H c= G
reconsider N1 = G as Subset of Y ;
N1 is Neighbourhood of f /. x by A4, Th17;
then consider N being Neighbourhood of x such that
A6: f .: N c= N1 by A5, NFCONT_1:10;
reconsider H = N as a_neighborhood of xt by A2, Th17;
take H = H; ::_thesis: ft .: H c= G
thus ft .: H c= G by A1, A6; ::_thesis: verum
end;
hence ft is_continuous_at xt by TMAP_1:def_2; ::_thesis: verum
end;
assume A7: ft is_continuous_at xt ; ::_thesis: f is_continuous_in x
now__::_thesis:_for_N1_being_Neighbourhood_of_f_/._x_ex_N_being_Neighbourhood_of_x_st_f_.:_N_c=_N1
let N1 be Neighbourhood of f /. x; ::_thesis: ex N being Neighbourhood of x st f .: N c= N1
reconsider G = N1 as Subset of Y ;
G is a_neighborhood of ft . xt by A4, Th17;
then consider H being a_neighborhood of xt such that
A8: ft .: H c= G by A7, TMAP_1:def_2;
reconsider N = H as Subset of X ;
reconsider N = N as Neighbourhood of x by A2, Th17;
take N = N; ::_thesis: f .: N c= N1
thus f .: N c= N1 by A1, A8; ::_thesis: verum
end;
hence f is_continuous_in x by A3, NFCONT_1:10; ::_thesis: verum
end;
theorem :: NORMSP_2:19
for X, Y being RealNormSpace
for f being PartFunc of X,Y
for ft being Function of (TopSpaceNorm X),(TopSpaceNorm Y) st f = ft holds
( f is_continuous_on the carrier of X iff ft is continuous )
proof
let X, Y be RealNormSpace; ::_thesis: for f being PartFunc of X,Y
for ft being Function of (TopSpaceNorm X),(TopSpaceNorm Y) st f = ft holds
( f is_continuous_on the carrier of X iff ft is continuous )
let f be PartFunc of X,Y; ::_thesis: for ft being Function of (TopSpaceNorm X),(TopSpaceNorm Y) st f = ft holds
( f is_continuous_on the carrier of X iff ft is continuous )
let ft be Function of (TopSpaceNorm X),(TopSpaceNorm Y); ::_thesis: ( f = ft implies ( f is_continuous_on the carrier of X iff ft is continuous ) )
assume A1: f = ft ; ::_thesis: ( f is_continuous_on the carrier of X iff ft is continuous )
A2: f | the carrier of X = f by RELSET_1:19;
hereby ::_thesis: ( ft is continuous implies f is_continuous_on the carrier of X )
assume A3: f is_continuous_on the carrier of X ; ::_thesis: ft is continuous
now__::_thesis:_for_xt_being_Point_of_(TopSpaceNorm_X)_holds_ft_is_continuous_at_xt
let xt be Point of (TopSpaceNorm X); ::_thesis: ft is_continuous_at xt
reconsider x = xt as Point of X ;
f | the carrier of X is_continuous_in x by A3, NFCONT_1:def_7;
hence ft is_continuous_at xt by A1, A2, Th18; ::_thesis: verum
end;
hence ft is continuous by TMAP_1:44; ::_thesis: verum
end;
assume A4: ft is continuous ; ::_thesis: f is_continuous_on the carrier of X
A5: now__::_thesis:_for_x_being_Point_of_X_st_x_in_the_carrier_of_X_holds_
f_|_the_carrier_of_X_is_continuous_in_x
let x be Point of X; ::_thesis: ( x in the carrier of X implies f | the carrier of X is_continuous_in x )
assume x in the carrier of X ; ::_thesis: f | the carrier of X is_continuous_in x
reconsider xt = x as Point of (TopSpaceNorm X) ;
ft is_continuous_at xt by A4, TMAP_1:44;
hence f | the carrier of X is_continuous_in x by A1, A2, Th18; ::_thesis: verum
end;
dom f = the carrier of X by A1, FUNCT_2:def_1;
hence f is_continuous_on the carrier of X by A5, NFCONT_1:def_7; ::_thesis: verum
end;
begin
definition
let X be RealNormSpace;
func LinearTopSpaceNorm X -> non empty strict RLTopStruct means :Def4: :: NORMSP_2:def 4
( the carrier of it = the carrier of X & 0. it = 0. X & the addF of it = the addF of X & the Mult of it = the Mult of X & the topology of it = the topology of (TopSpaceNorm X) );
existence
ex b1 being non empty strict RLTopStruct st
( the carrier of b1 = the carrier of X & 0. b1 = 0. X & the addF of b1 = the addF of X & the Mult of b1 = the Mult of X & the topology of b1 = the topology of (TopSpaceNorm X) )
proof
reconsider TP = the topology of (TopSpaceNorm X) as Subset-Family of X ;
take RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) ; ::_thesis: ( the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the carrier of X & 0. RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = 0. X & the addF of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the addF of X & the Mult of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the Mult of X & the topology of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the topology of (TopSpaceNorm X) )
thus ( the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the carrier of X & 0. RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = 0. X & the addF of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the addF of X & the Mult of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the Mult of X & the topology of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the topology of (TopSpaceNorm X) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict RLTopStruct st the carrier of b1 = the carrier of X & 0. b1 = 0. X & the addF of b1 = the addF of X & the Mult of b1 = the Mult of X & the topology of b1 = the topology of (TopSpaceNorm X) & the carrier of b2 = the carrier of X & 0. b2 = 0. X & the addF of b2 = the addF of X & the Mult of b2 = the Mult of X & the topology of b2 = the topology of (TopSpaceNorm X) holds
b1 = b2 ;
end;
:: deftheorem Def4 defines LinearTopSpaceNorm NORMSP_2:def_4_:_
for X being RealNormSpace
for b2 being non empty strict RLTopStruct holds
( b2 = LinearTopSpaceNorm X iff ( the carrier of b2 = the carrier of X & 0. b2 = 0. X & the addF of b2 = the addF of X & the Mult of b2 = the Mult of X & the topology of b2 = the topology of (TopSpaceNorm X) ) );
registration
let X be RealNormSpace;
cluster LinearTopSpaceNorm X -> non empty TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous ;
correctness
coherence
( LinearTopSpaceNorm X is add-continuous & LinearTopSpaceNorm X is Mult-continuous & LinearTopSpaceNorm X is TopSpace-like & LinearTopSpaceNorm X is Abelian & LinearTopSpaceNorm X is add-associative & LinearTopSpaceNorm X is right_zeroed & LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital );
proof
thus LinearTopSpaceNorm X is add-continuous ::_thesis: ( LinearTopSpaceNorm X is Mult-continuous & LinearTopSpaceNorm X is TopSpace-like & LinearTopSpaceNorm X is Abelian & LinearTopSpaceNorm X is add-associative & LinearTopSpaceNorm X is right_zeroed & LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital )
proof
let x1, x2 be Point of (LinearTopSpaceNorm X); :: according to RLTOPSP1:def_8 ::_thesis: for b1 being Element of bool the carrier of (LinearTopSpaceNorm X) holds
( not b1 is open or not x1 + x2 in b1 or ex b2, b3 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b2 is open & b3 is open & x1 in b2 & x2 in b3 & b2 + b3 c= b1 ) )
reconsider z2 = x2 as Element of (MetricSpaceNorm X) by Def4;
reconsider z1 = x1 as Element of (MetricSpaceNorm X) by Def4;
reconsider z12 = x1 + x2 as Element of (MetricSpaceNorm X) by Def4;
let V be Subset of (LinearTopSpaceNorm X); ::_thesis: ( not V is open or not x1 + x2 in V or ex b1, b2 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b1 is open & b2 is open & x1 in b1 & x2 in b2 & b1 + b2 c= V ) )
assume that
A1: V is open and
A2: x1 + x2 in V ; ::_thesis: ex b1, b2 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b1 is open & b2 is open & x1 in b1 & x2 in b2 & b1 + b2 c= V )
V in the topology of (LinearTopSpaceNorm X) by A1, PRE_TOPC:def_2;
then V in the topology of (TopSpaceNorm X) by Def4;
then consider r being Real such that
A3: r > 0 and
A4: Ball (z12,r) c= V by A2, PCOMPS_1:def_4;
set r2 = r / 2;
A5: 0 < r / 2 by A3, XREAL_1:215;
reconsider V1 = Ball (z1,(r / 2)), V2 = Ball (z2,(r / 2)) as Subset of (LinearTopSpaceNorm X) by Def4;
A6: V1 + V2 c= V
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in V1 + V2 or w in V )
assume w in V1 + V2 ; ::_thesis: w in V
then consider v, u being VECTOR of (LinearTopSpaceNorm X) such that
A7: w = v + u and
A8: ( v in V1 & u in V2 ) ;
reconsider v1 = v, u1 = u as Element of (MetricSpaceNorm X) by Def4;
reconsider w1 = w as Element of (MetricSpaceNorm X) by A7, Def4;
reconsider zz12 = x1 + x2, zz1 = x1, zz2 = x2, vv1 = v, uu1 = u as Point of X by Def4;
A9: ( ||.((zz1 - vv1) + (zz2 - uu1)).|| <= ||.(zz1 - vv1).|| + ||.(zz2 - uu1).|| & ||.(zz1 - vv1).|| = dist (z1,v1) ) by Def1, NORMSP_1:def_1;
( dist (z1,v1) < r / 2 & dist (z2,u1) < r / 2 ) by A8, METRIC_1:11;
then A10: (dist (z1,v1)) + (dist (z2,u1)) < (r / 2) + (r / 2) by XREAL_1:8;
reconsider ww1 = w as Point of X by A7, Def4;
A11: ||.(zz2 - uu1).|| = dist (z2,u1) by Def1;
dist (z12,w1) = ||.(zz12 - ww1).|| by Def1
.= ||.((zz1 + zz2) - ww1).|| by Def4
.= ||.((zz1 + zz2) - (vv1 + uu1)).|| by A7, Def4
.= ||.((zz1 + zz2) + ((- uu1) + (- vv1))).|| by RLVECT_1:31
.= ||.(((zz1 + zz2) + (- vv1)) + (- uu1)).|| by RLVECT_1:def_3
.= ||.(((zz1 + (- vv1)) + zz2) + (- uu1)).|| by RLVECT_1:def_3
.= ||.((zz1 + (- vv1)) + (zz2 + (- uu1))).|| by RLVECT_1:def_3 ;
then dist (z12,w1) < r by A9, A11, A10, XXREAL_0:2;
then w1 in Ball (z12,r) by METRIC_1:11;
hence w in V by A4; ::_thesis: verum
end;
dist (z2,z2) = 0 by METRIC_1:1;
then A12: x2 in V2 by A5, METRIC_1:11;
Ball (z2,(r / 2)) in the topology of (TopSpaceNorm X) by PCOMPS_1:29;
then Ball (z2,(r / 2)) in the topology of (LinearTopSpaceNorm X) by Def4;
then A13: V2 is open by PRE_TOPC:def_2;
Ball (z1,(r / 2)) in the topology of (TopSpaceNorm X) by PCOMPS_1:29;
then Ball (z1,(r / 2)) in the topology of (LinearTopSpaceNorm X) by Def4;
then A14: V1 is open by PRE_TOPC:def_2;
dist (z1,z1) = 0 by METRIC_1:1;
then x1 in V1 by A5, METRIC_1:11;
hence ex b1, b2 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b1 is open & b2 is open & x1 in b1 & x2 in b2 & b1 + b2 c= V ) by A14, A13, A12, A6; ::_thesis: verum
end;
A15: now__::_thesis:_for_a,_b_being_real_number_
for_v_being_VECTOR_of_(LinearTopSpaceNorm_X)_holds_(a_+_b)_*_v_=_(a_*_v)_+_(b_*_v)
let a, b be real number ; ::_thesis: for v being VECTOR of (LinearTopSpaceNorm X) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of (LinearTopSpaceNorm X); ::_thesis: (a + b) * v = (a * v) + (b * v)
reconsider v1 = v as VECTOR of X by Def4;
( a * v = a * v1 & b * v = b * v1 ) by Def4;
then A16: (a * v1) + (b * v1) = (a * v) + (b * v) by Def4;
(a + b) * v = (a + b) * v1 by Def4;
hence (a + b) * v = (a * v) + (b * v) by A16, RLVECT_1:def_6; ::_thesis: verum
end;
thus LinearTopSpaceNorm X is Mult-continuous ::_thesis: ( LinearTopSpaceNorm X is TopSpace-like & LinearTopSpaceNorm X is Abelian & LinearTopSpaceNorm X is add-associative & LinearTopSpaceNorm X is right_zeroed & LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital )
proof
let a be Real; :: according to RLTOPSP1:def_9 ::_thesis: for b1 being Element of the carrier of (LinearTopSpaceNorm X)
for b2 being Element of bool the carrier of (LinearTopSpaceNorm X) holds
( not b2 is open or not a * b1 in b2 or ex b3 being Element of REAL ex b4 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b4 is open & b1 in b4 & ( for b5 being Element of REAL holds
( b3 <= abs (b5 - a) or b5 * b4 c= b2 ) ) ) )
let x be Point of (LinearTopSpaceNorm X); ::_thesis: for b1 being Element of bool the carrier of (LinearTopSpaceNorm X) holds
( not b1 is open or not a * x in b1 or ex b2 being Element of REAL ex b3 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b3 is open & x in b3 & ( for b4 being Element of REAL holds
( b2 <= abs (b4 - a) or b4 * b3 c= b1 ) ) ) )
let V be Subset of (LinearTopSpaceNorm X); ::_thesis: ( not V is open or not a * x in V or ex b1 being Element of REAL ex b2 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b2 is open & x in b2 & ( for b3 being Element of REAL holds
( b1 <= abs (b3 - a) or b3 * b2 c= V ) ) ) )
assume that
A17: V is open and
A18: a * x in V ; ::_thesis: ex b1 being Element of REAL ex b2 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b2 is open & x in b2 & ( for b3 being Element of REAL holds
( b1 <= abs (b3 - a) or b3 * b2 c= V ) ) )
reconsider z = x, az = a * x as Element of (MetricSpaceNorm X) by Def4;
V in the topology of (LinearTopSpaceNorm X) by A17, PRE_TOPC:def_2;
then V in the topology of (TopSpaceNorm X) by Def4;
then consider r0 being Real such that
A19: r0 > 0 and
A20: Ball (az,r0) c= V by A18, PCOMPS_1:def_4;
set r = r0 / 2;
r0 / 2 > 0 by A19, XREAL_1:215;
then A21: 0 < (r0 / 2) / 2 by XREAL_1:215;
reconsider z1 = z as Point of X ;
set r2 = min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1);
reconsider W = Ball (z,(min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1))) as Subset of (LinearTopSpaceNorm X) by Def4;
A22: r0 / 2 < r0 / 1 by A19, XREAL_1:76;
A23: for s being Real st abs (s - a) < min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) holds
s * W c= V
proof
let s be Real; ::_thesis: ( abs (s - a) < min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) implies s * W c= V )
assume abs (s - a) < min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) ; ::_thesis: s * W c= V
then A24: abs (a - s) <= min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) by COMPLEX1:60;
thus s * W c= V ::_thesis: verum
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in s * W or w in V )
assume w in s * W ; ::_thesis: w in V
then consider v being VECTOR of (LinearTopSpaceNorm X) such that
A25: w = s * v and
A26: v in W ;
reconsider v1 = v as Element of (MetricSpaceNorm X) by Def4;
A27: dist (z,v1) < min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) by A26, METRIC_1:11;
reconsider w1 = w as Element of (MetricSpaceNorm X) by A25, Def4;
reconsider zza = a * x, zz = x, vv1 = v as Point of X by Def4;
A28: ||.(zz - vv1).|| = dist (z,v1) by Def1;
min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) <= 1 by XXREAL_0:17;
then ||.(zz - vv1).|| <= 1 by A28, A27, XXREAL_0:2;
then ||.(vv1 - zz).|| <= 1 by NORMSP_1:7;
then A29: ||.zz.|| + ||.(vv1 - zz).|| <= ||.zz.|| + 1 by XREAL_1:6;
zz + (vv1 - zz) = vv1 - (zz - zz) by RLVECT_1:29
.= vv1 - (0. X) by RLVECT_1:15
.= vv1 by RLVECT_1:13 ;
then ||.vv1.|| <= ||.zz.|| + ||.(vv1 - zz).|| by NORMSP_1:def_1;
then A30: ||.vv1.|| <= ||.zz.|| + 1 by A29, XXREAL_0:2;
A31: 0 <= 1 + ||.z1.|| by NORMSP_1:4, XREAL_1:39;
then A32: (min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1)) * (||.zz.|| + 1) <= (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))) * (||.zz.|| + 1) by XREAL_1:64, XXREAL_0:17;
( 0 <= abs (a - s) & 0 <= ||.vv1.|| ) by COMPLEX1:46, NORMSP_1:4;
then (abs (a - s)) * ||.vv1.|| <= (min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1)) * (||.zz.|| + 1) by A24, A30, XREAL_1:66;
then (abs (a - s)) * ||.vv1.|| <= (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))) * (||.z1.|| + 1) by A32, XXREAL_0:2;
then A33: (abs (a - s)) * ||.vv1.|| <= ((||.z1.|| + 1) / ((1 + ||.z1.||) + (abs a))) * ((r0 / 2) / 2) by XCMPLX_1:75;
0 <= abs a by COMPLEX1:46;
then 0 + (1 + ||.z1.||) <= (abs a) + (1 + ||.z1.||) by XREAL_1:6;
then (||.z1.|| + 1) / ((1 + ||.z1.||) + (abs a)) <= 1 by A31, XREAL_1:183;
then ((||.z1.|| + 1) / ((1 + ||.z1.||) + (abs a))) * ((r0 / 2) / 2) <= 1 * ((r0 / 2) / 2) by A19, XREAL_1:64;
then A34: (abs (a - s)) * ||.vv1.|| <= (r0 / 2) / 2 by A33, XXREAL_0:2;
reconsider ww1 = w as Point of X by A25, Def4;
(a * (zz - vv1)) - ((s - a) * vv1) = ((a * zz) - (a * vv1)) - ((s - a) * vv1) by RLVECT_1:34
.= ((a * zz) - (a * vv1)) - ((s * vv1) - (a * vv1)) by RLVECT_1:35
.= (a * zz) - (((s * vv1) - (a * vv1)) + (a * vv1)) by RLVECT_1:27
.= (a * zz) - ((s * vv1) - ((a * vv1) - (a * vv1))) by RLVECT_1:29
.= (a * zz) - ((s * vv1) - (0. X)) by RLVECT_1:15
.= (a * zz) - (s * vv1) by RLVECT_1:13 ;
then ||.((a * zz) - (s * vv1)).|| <= ||.(a * (zz - vv1)).|| + ||.((s - a) * vv1).|| by NORMSP_1:3;
then ||.((a * zz) - (s * vv1)).|| <= ((abs a) * ||.(zz - vv1).||) + ||.((s - a) * vv1).|| by NORMSP_1:def_1;
then ||.((a * zz) - (s * vv1)).|| <= ((abs a) * ||.(zz - vv1).||) + ((abs (s - a)) * ||.vv1.||) by NORMSP_1:def_1;
then A35: ||.((a * zz) - (s * vv1)).|| <= ((abs a) * ||.(zz - vv1).||) + ((abs (a - s)) * ||.vv1.||) by COMPLEX1:60;
A36: 0 <= abs a by COMPLEX1:46;
then A37: (min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1)) * (abs a) <= (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))) * (abs a) by XREAL_1:64, XXREAL_0:17;
0 <= 1 + ||.z1.|| by NORMSP_1:4, XREAL_1:39;
then 0 + (abs a) <= (1 + ||.z1.||) + (abs a) by XREAL_1:6;
then (abs a) / ((1 + ||.z1.||) + (abs a)) <= 1 by A36, XREAL_1:183;
then A38: ((abs a) / ((1 + ||.z1.||) + (abs a))) * ((r0 / 2) / 2) <= 1 * ((r0 / 2) / 2) by A19, XREAL_1:64;
||.(zz - vv1).|| * (abs a) <= (min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1)) * (abs a) by A28, A27, A36, XREAL_1:64;
then (abs a) * ||.(zz - vv1).|| <= (abs a) * (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))) by A37, XXREAL_0:2;
then (abs a) * ||.(zz - vv1).|| <= ((abs a) / ((1 + ||.z1.||) + (abs a))) * ((r0 / 2) / 2) by XCMPLX_1:75;
then (abs a) * ||.(zz - vv1).|| <= (r0 / 2) / 2 by A38, XXREAL_0:2;
then A39: ((abs a) * ||.(zz - vv1).||) + ((abs (a - s)) * ||.vv1.||) <= ((r0 / 2) / 2) + ((r0 / 2) / 2) by A34, XREAL_1:7;
dist (az,w1) = ||.(zza - ww1).|| by Def1
.= ||.((a * zz) - ww1).|| by Def4
.= ||.((a * zz) - (s * vv1)).|| by A25, Def4 ;
then dist (az,w1) <= r0 / 2 by A35, A39, XXREAL_0:2;
then dist (az,w1) < r0 by A22, XXREAL_0:2;
then w1 in Ball (az,r0) by METRIC_1:11;
hence w in V by A20; ::_thesis: verum
end;
end;
( 0 <= ||.z1.|| & 0 <= abs a ) by COMPLEX1:46, NORMSP_1:4;
then 0 / ((1 + ||.z1.||) + (abs a)) < ((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a)) by A21, XREAL_1:74;
then A40: 0 < min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) by XXREAL_0:15;
Ball (z,(min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1))) in the topology of (TopSpaceNorm X) by PCOMPS_1:29;
then Ball (z,(min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1))) in the topology of (LinearTopSpaceNorm X) by Def4;
then A41: W is open by PRE_TOPC:def_2;
dist (z,z) = 0 by METRIC_1:1;
then x in W by A40, METRIC_1:11;
hence ex b1 being Element of REAL ex b2 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b2 is open & x in b2 & ( for b3 being Element of REAL holds
( b1 <= abs (b3 - a) or b3 * b2 c= V ) ) ) by A41, A40, A23; ::_thesis: verum
end;
thus LinearTopSpaceNorm X is TopSpace-like ::_thesis: ( LinearTopSpaceNorm X is Abelian & LinearTopSpaceNorm X is add-associative & LinearTopSpaceNorm X is right_zeroed & LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital )
proof
set LTSN = LinearTopSpaceNorm X;
A42: the topology of (LinearTopSpaceNorm X) = the topology of (TopSpaceNorm X) by Def4;
then A43: for a, b being Subset of (LinearTopSpaceNorm X) st a in the topology of (LinearTopSpaceNorm X) & b in the topology of (LinearTopSpaceNorm X) holds
a /\ b in the topology of (LinearTopSpaceNorm X) by PRE_TOPC:def_1;
the carrier of (LinearTopSpaceNorm X) = the carrier of (TopSpaceNorm X) by Def4;
then ( the carrier of (LinearTopSpaceNorm X) in the topology of (LinearTopSpaceNorm X) & ( for a being Subset-Family of (LinearTopSpaceNorm X) st a c= the topology of (LinearTopSpaceNorm X) holds
union a in the topology of (LinearTopSpaceNorm X) ) ) by A42, PRE_TOPC:def_1;
hence LinearTopSpaceNorm X is TopSpace-like by A43, PRE_TOPC:def_1; ::_thesis: verum
end;
thus LinearTopSpaceNorm X is Abelian ::_thesis: ( LinearTopSpaceNorm X is add-associative & LinearTopSpaceNorm X is right_zeroed & LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital )
proof
let v, w be VECTOR of (LinearTopSpaceNorm X); :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v
reconsider v1 = v, w1 = w as VECTOR of X by Def4;
thus v + w = v1 + w1 by Def4
.= w1 + v1
.= w + v by Def4 ; ::_thesis: verum
end;
thus LinearTopSpaceNorm X is add-associative ::_thesis: ( LinearTopSpaceNorm X is right_zeroed & LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital )
proof
let v, w, x be VECTOR of (LinearTopSpaceNorm X); :: according to RLVECT_1:def_3 ::_thesis: (v + w) + x = v + (w + x)
reconsider v1 = v, w1 = w, x1 = x as VECTOR of X by Def4;
A44: w + x = w1 + x1 by Def4;
v + w = v1 + w1 by Def4;
hence (v + w) + x = (v1 + w1) + x1 by Def4
.= v1 + (w1 + x1) by RLVECT_1:def_3
.= v + (w + x) by A44, Def4 ;
::_thesis: verum
end;
thus LinearTopSpaceNorm X is right_zeroed ::_thesis: ( LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital )
proof
let v be VECTOR of (LinearTopSpaceNorm X); :: according to RLVECT_1:def_4 ::_thesis: v + (0. (LinearTopSpaceNorm X)) = v
reconsider v1 = v as VECTOR of X by Def4;
0. (LinearTopSpaceNorm X) = 0. X by Def4;
hence v + (0. (LinearTopSpaceNorm X)) = v1 + (0. X) by Def4
.= v by RLVECT_1:def_4 ;
::_thesis: verum
end;
thus LinearTopSpaceNorm X is right_complementable ::_thesis: ( LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital )
proof
let v be VECTOR of (LinearTopSpaceNorm X); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider v1 = v as VECTOR of X by Def4;
reconsider w = - v1 as VECTOR of (LinearTopSpaceNorm X) by Def4;
take w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. (LinearTopSpaceNorm X)
thus v + w = v1 - v1 by Def4
.= 0. X by RLVECT_1:15
.= 0. (LinearTopSpaceNorm X) by Def4 ; ::_thesis: verum
end;
A45: now__::_thesis:_for_a,_b_being_real_number_
for_v_being_VECTOR_of_(LinearTopSpaceNorm_X)_holds_(a_*_b)_*_v_=_a_*_(b_*_v)
let a, b be real number ; ::_thesis: for v being VECTOR of (LinearTopSpaceNorm X) holds (a * b) * v = a * (b * v)
let v be VECTOR of (LinearTopSpaceNorm X); ::_thesis: (a * b) * v = a * (b * v)
reconsider v1 = v as VECTOR of X by Def4;
b * v = b * v1 by Def4;
then a * (b * v1) = a * (b * v) by Def4;
then (a * b) * v1 = a * (b * v) by RLVECT_1:def_7;
hence (a * b) * v = a * (b * v) by Def4; ::_thesis: verum
end;
A46: now__::_thesis:_for_a_being_real_number_
for_v,_w_being_VECTOR_of_(LinearTopSpaceNorm_X)_holds_a_*_(v_+_w)_=_(a_*_v)_+_(a_*_w)
let a be real number ; ::_thesis: for v, w being VECTOR of (LinearTopSpaceNorm X) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of (LinearTopSpaceNorm X); ::_thesis: a * (v + w) = (a * v) + (a * w)
reconsider v1 = v, w1 = w as VECTOR of X by Def4;
( a * v = a * v1 & a * w = a * w1 ) by Def4;
then A47: (a * v1) + (a * w1) = (a * v) + (a * w) by Def4;
v + w = v1 + w1 by Def4;
then a * (v + w) = a * (v1 + w1) by Def4;
hence a * (v + w) = (a * v) + (a * w) by A47, RLVECT_1:def_5; ::_thesis: verum
end;
now__::_thesis:_for_v_being_VECTOR_of_(LinearTopSpaceNorm_X)_holds_1_*_v_=_v
let v be VECTOR of (LinearTopSpaceNorm X); ::_thesis: 1 * v = v
reconsider v1 = v as VECTOR of X by Def4;
thus 1 * v = 1 * v1 by Def4
.= v by RLVECT_1:def_8 ; ::_thesis: verum
end;
hence ( LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital ) by A46, A15, A45, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8; ::_thesis: verum
end;
end;
theorem Th20: :: NORMSP_2:20
for X being RealNormSpace
for V being Subset of (TopSpaceNorm X)
for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is open iff Vt is open )
proof
let X be RealNormSpace; ::_thesis: for V being Subset of (TopSpaceNorm X)
for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is open iff Vt is open )
let V be Subset of (TopSpaceNorm X); ::_thesis: for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is open iff Vt is open )
let Vt be Subset of (LinearTopSpaceNorm X); ::_thesis: ( V = Vt implies ( V is open iff Vt is open ) )
( Vt is open iff Vt in the topology of (LinearTopSpaceNorm X) ) by PRE_TOPC:def_2;
then A1: ( Vt is open iff Vt in the topology of (TopSpaceNorm X) ) by Def4;
assume V = Vt ; ::_thesis: ( V is open iff Vt is open )
hence ( V is open iff Vt is open ) by A1, PRE_TOPC:def_2; ::_thesis: verum
end;
theorem Th21: :: NORMSP_2:21
for X being RealNormSpace
for V being Subset of (TopSpaceNorm X)
for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is closed iff Vt is closed )
proof
let X be RealNormSpace; ::_thesis: for V being Subset of (TopSpaceNorm X)
for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is closed iff Vt is closed )
let V be Subset of (TopSpaceNorm X); ::_thesis: for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is closed iff Vt is closed )
let Vt be Subset of (LinearTopSpaceNorm X); ::_thesis: ( V = Vt implies ( V is closed iff Vt is closed ) )
assume V = Vt ; ::_thesis: ( V is closed iff Vt is closed )
then A1: Vt ` = V ` by Def4;
( Vt is closed iff Vt ` is open ) by TOPS_1:3;
then ( Vt is closed iff V ` is open ) by A1, Th20;
hence ( V is closed iff Vt is closed ) by TOPS_1:3; ::_thesis: verum
end;
theorem :: NORMSP_2:22
for X being RealNormSpace
for V being Subset of (LinearTopSpaceNorm X) holds
( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )
proof
let X be RealNormSpace; ::_thesis: for V being Subset of (LinearTopSpaceNorm X) holds
( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )
let V be Subset of (LinearTopSpaceNorm X); ::_thesis: ( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )
reconsider V0 = V as Subset of (TopSpaceNorm X) by Def4;
( V is open iff V0 is open ) by Th20;
hence ( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) ) by Th7; ::_thesis: verum
end;
theorem :: NORMSP_2:23
for X being RealNormSpace
for x being Point of X
for r being Real
for V being Subset of (LinearTopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| < r } holds
V is open
proof
let X be RealNormSpace; ::_thesis: for x being Point of X
for r being Real
for V being Subset of (LinearTopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| < r } holds
V is open
let x be Point of X; ::_thesis: for r being Real
for V being Subset of (LinearTopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| < r } holds
V is open
let r be Real; ::_thesis: for V being Subset of (LinearTopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| < r } holds
V is open
let V be Subset of (LinearTopSpaceNorm X); ::_thesis: ( V = { y where y is Point of X : ||.(x - y).|| < r } implies V is open )
reconsider V0 = V as Subset of (TopSpaceNorm X) by Def4;
assume V = { y where y is Point of X : ||.(x - y).|| < r } ; ::_thesis: V is open
then V0 is open by Th8;
hence V is open by Th20; ::_thesis: verum
end;
theorem :: NORMSP_2:24
for X being RealNormSpace
for x being Point of X
for r being Real
for V being Subset of (TopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| <= r } holds
V is closed
proof
let X be RealNormSpace; ::_thesis: for x being Point of X
for r being Real
for V being Subset of (TopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| <= r } holds
V is closed
let x be Point of X; ::_thesis: for r being Real
for V being Subset of (TopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| <= r } holds
V is closed
let r be Real; ::_thesis: for V being Subset of (TopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| <= r } holds
V is closed
let V be Subset of (TopSpaceNorm X); ::_thesis: ( V = { y where y is Point of X : ||.(x - y).|| <= r } implies V is closed )
assume A1: V = { y where y is Point of X : ||.(x - y).|| <= r } ; ::_thesis: V is closed
reconsider z = x as Element of (MetricSpaceNorm X) ;
ex t being Point of X st
( t = x & cl_Ball (z,r) = { y where y is Point of X : ||.(t - y).|| <= r } ) by Th3;
hence V is closed by A1, TOPREAL6:57; ::_thesis: verum
end;
registration
let X be RealNormSpace;
cluster LinearTopSpaceNorm X -> non empty T_2 strict ;
coherence
LinearTopSpaceNorm X is T_2
proof
let p, q be Point of (LinearTopSpaceNorm X); :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
A1: the topology of (LinearTopSpaceNorm X) = the topology of (TopSpaceNorm X) by Def4;
reconsider p1 = p, q1 = q as Point of (TopSpaceNorm X) by Def4;
assume p <> q ; ::_thesis: ex b1, b2 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
then consider W1, V1 being Subset of (TopSpaceNorm X) such that
A2: W1 is open and
A3: V1 is open and
A4: ( p1 in W1 & q1 in V1 & W1 misses V1 ) by PRE_TOPC:def_10;
reconsider W = W1, V = V1 as Subset of (LinearTopSpaceNorm X) by Def4;
V1 in the topology of (TopSpaceNorm X) by A3, PRE_TOPC:def_2;
then A5: V is open by A1, PRE_TOPC:def_2;
W1 in the topology of (TopSpaceNorm X) by A2, PRE_TOPC:def_2;
then W is open by A1, PRE_TOPC:def_2;
hence ex b1, b2 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) by A4, A5; ::_thesis: verum
end;
cluster LinearTopSpaceNorm X -> non empty sober strict ;
coherence
LinearTopSpaceNorm X is sober by YELLOW_8:22;
end;
theorem Th25: :: NORMSP_2:25
for X being RealNormSpace
for S being Subset-Family of (TopSpaceNorm X)
for St being Subset-Family of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is Basis of iff S is Basis of )
proof
let X be RealNormSpace; ::_thesis: for S being Subset-Family of (TopSpaceNorm X)
for St being Subset-Family of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is Basis of iff S is Basis of )
let S be Subset-Family of (TopSpaceNorm X); ::_thesis: for St being Subset-Family of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is Basis of iff S is Basis of )
let St be Subset-Family of (LinearTopSpaceNorm X); ::_thesis: for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is Basis of iff S is Basis of )
let x be Point of (TopSpaceNorm X); ::_thesis: for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is Basis of iff S is Basis of )
let xt be Point of (LinearTopSpaceNorm X); ::_thesis: ( S = St & x = xt implies ( St is Basis of iff S is Basis of ) )
assume that
A1: S = St and
A2: x = xt ; ::_thesis: ( St is Basis of iff S is Basis of )
A3: Intersect S = Intersect St by A1, Def4;
hereby ::_thesis: ( S is Basis of implies St is Basis of )
assume A4: St is Basis of ; ::_thesis: S is Basis of
then St c= the topology of (LinearTopSpaceNorm X) by TOPS_2:64;
then A5: S c= the topology of (TopSpaceNorm X) by A1, Def4;
A6: now__::_thesis:_for_U_being_Subset_of_(TopSpaceNorm_X)_st_U_is_open_&_x_in_U_holds_
ex_V_being_Subset_of_(TopSpaceNorm_X)_st_
(_V_in_S_&_V_c=_U_)
let U be Subset of (TopSpaceNorm X); ::_thesis: ( U is open & x in U implies ex V being Subset of (TopSpaceNorm X) st
( V in S & V c= U ) )
assume that
A7: U is open and
A8: x in U ; ::_thesis: ex V being Subset of (TopSpaceNorm X) st
( V in S & V c= U )
reconsider Ut = U as open Subset of (LinearTopSpaceNorm X) by A7, Def4, Th20;
consider Vt being Subset of (LinearTopSpaceNorm X) such that
A9: ( Vt in St & Vt c= Ut ) by A2, A4, A8, YELLOW_8:def_1;
reconsider V = Vt as Subset of (TopSpaceNorm X) by Def4;
take V = V; ::_thesis: ( V in S & V c= U )
thus ( V in S & V c= U ) by A1, A9; ::_thesis: verum
end;
x in Intersect S by A2, A3, A4, YELLOW_8:def_1;
hence S is Basis of by A5, A6, TOPS_2:64, YELLOW_8:def_1; ::_thesis: verum
end;
assume A10: S is Basis of ; ::_thesis: St is Basis of
then S c= the topology of (TopSpaceNorm X) by TOPS_2:64;
then A11: St c= the topology of (LinearTopSpaceNorm X) by A1, Def4;
A12: now__::_thesis:_for_Ut_being_Subset_of_(LinearTopSpaceNorm_X)_st_Ut_is_open_&_xt_in_Ut_holds_
ex_Vt_being_Subset_of_(LinearTopSpaceNorm_X)_st_
(_Vt_in_St_&_Vt_c=_Ut_)
let Ut be Subset of (LinearTopSpaceNorm X); ::_thesis: ( Ut is open & xt in Ut implies ex Vt being Subset of (LinearTopSpaceNorm X) st
( Vt in St & Vt c= Ut ) )
assume that
A13: Ut is open and
A14: xt in Ut ; ::_thesis: ex Vt being Subset of (LinearTopSpaceNorm X) st
( Vt in St & Vt c= Ut )
reconsider U = Ut as open Subset of (TopSpaceNorm X) by A13, Def4, Th20;
consider V being Subset of (TopSpaceNorm X) such that
A15: ( V in S & V c= U ) by A2, A10, A14, YELLOW_8:def_1;
reconsider Vt = V as Subset of (LinearTopSpaceNorm X) by Def4;
take Vt = Vt; ::_thesis: ( Vt in St & Vt c= Ut )
thus ( Vt in St & Vt c= Ut ) by A1, A15; ::_thesis: verum
end;
xt in Intersect St by A2, A3, A10, YELLOW_8:def_1;
hence St is Basis of by A11, A12, TOPS_2:64, YELLOW_8:def_1; ::_thesis: verum
end;
registration
let X be RealNormSpace;
cluster LinearTopSpaceNorm X -> non empty first-countable strict ;
coherence
LinearTopSpaceNorm X is first-countable
proof
now__::_thesis:_for_xt_being_Point_of_(LinearTopSpaceNorm_X)_ex_Bt_being_Basis_of_st_Bt_is_countable
let xt be Point of (LinearTopSpaceNorm X); ::_thesis: ex Bt being Basis of st Bt is countable
reconsider x = xt as Point of (TopSpaceNorm X) by Def4;
consider B being Basis of such that
A1: B is countable by FRECHET:def_2;
reconsider Bt = B as Basis of by Th25, Def4;
take Bt = Bt; ::_thesis: Bt is countable
thus Bt is countable by A1; ::_thesis: verum
end;
hence LinearTopSpaceNorm X is first-countable by FRECHET:def_2; ::_thesis: verum
end;
cluster LinearTopSpaceNorm X -> non empty Frechet strict ;
coherence
LinearTopSpaceNorm X is Frechet ;
cluster LinearTopSpaceNorm X -> non empty sequential strict ;
coherence
LinearTopSpaceNorm X is sequential ;
end;
theorem Th26: :: NORMSP_2:26
for X being RealNormSpace
for S being sequence of (TopSpaceNorm X)
for St being sequence of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )
proof
let X be RealNormSpace; ::_thesis: for S being sequence of (TopSpaceNorm X)
for St being sequence of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )
let S be sequence of (TopSpaceNorm X); ::_thesis: for St being sequence of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )
let St be sequence of (LinearTopSpaceNorm X); ::_thesis: for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )
let x be Point of (TopSpaceNorm X); ::_thesis: for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )
let xt be Point of (LinearTopSpaceNorm X); ::_thesis: ( S = St & x = xt implies ( St is_convergent_to xt iff S is_convergent_to x ) )
assume that
A1: S = St and
A2: x = xt ; ::_thesis: ( St is_convergent_to xt iff S is_convergent_to x )
A3: now__::_thesis:_(_S_is_convergent_to_x_implies_St_is_convergent_to_xt_)
assume A4: S is_convergent_to x ; ::_thesis: St is_convergent_to xt
now__::_thesis:_for_U1t_being_Subset_of_(LinearTopSpaceNorm_X)_st_U1t_is_open_&_xt_in_U1t_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
St_._m_in_U1t
let U1t be Subset of (LinearTopSpaceNorm X); ::_thesis: ( U1t is open & xt in U1t implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
St . m in U1t )
assume that
A5: U1t is open and
A6: xt in U1t ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
St . m in U1t
reconsider U1 = U1t as open Subset of (TopSpaceNorm X) by A5, Def4, Th20;
consider n being Element of NAT such that
A7: for m being Element of NAT st n <= m holds
S . m in U1 by A2, A4, A6, FRECHET:def_3;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
St . m in U1t
let m be Element of NAT ; ::_thesis: ( n <= m implies St . m in U1t )
assume n <= m ; ::_thesis: St . m in U1t
hence St . m in U1t by A1, A7; ::_thesis: verum
end;
hence St is_convergent_to xt by FRECHET:def_3; ::_thesis: verum
end;
now__::_thesis:_(_St_is_convergent_to_xt_implies_S_is_convergent_to_x_)
assume A8: St is_convergent_to xt ; ::_thesis: S is_convergent_to x
now__::_thesis:_for_U1_being_Subset_of_(TopSpaceNorm_X)_st_U1_is_open_&_x_in_U1_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
S_._m_in_U1
let U1 be Subset of (TopSpaceNorm X); ::_thesis: ( U1 is open & x in U1 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in U1 )
assume that
A9: U1 is open and
A10: x in U1 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in U1
reconsider U1t = U1 as open Subset of (LinearTopSpaceNorm X) by A9, Def4, Th20;
consider n being Element of NAT such that
A11: for m being Element of NAT st n <= m holds
St . m in U1t by A2, A8, A10, FRECHET:def_3;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
S . m in U1
let m be Element of NAT ; ::_thesis: ( n <= m implies S . m in U1 )
assume n <= m ; ::_thesis: S . m in U1
hence S . m in U1 by A1, A11; ::_thesis: verum
end;
hence S is_convergent_to x by FRECHET:def_3; ::_thesis: verum
end;
hence ( St is_convergent_to xt iff S is_convergent_to x ) by A3; ::_thesis: verum
end;
theorem Th27: :: NORMSP_2:27
for X being RealNormSpace
for S being sequence of (TopSpaceNorm X)
for St being sequence of (LinearTopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
proof
let X be RealNormSpace; ::_thesis: for S being sequence of (TopSpaceNorm X)
for St being sequence of (LinearTopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
let S be sequence of (TopSpaceNorm X); ::_thesis: for St being sequence of (LinearTopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
let St be sequence of (LinearTopSpaceNorm X); ::_thesis: ( S = St implies ( St is convergent iff S is convergent ) )
assume A1: S = St ; ::_thesis: ( St is convergent iff S is convergent )
A2: now__::_thesis:_(_S_is_convergent_implies_St_is_convergent_)
assume S is convergent ; ::_thesis: St is convergent
then consider x being Point of (TopSpaceNorm X) such that
A3: S is_convergent_to x by FRECHET:def_4;
reconsider xt = x as Point of (LinearTopSpaceNorm X) by Def4;
St is_convergent_to xt by A1, A3, Th26;
hence St is convergent by FRECHET:def_4; ::_thesis: verum
end;
now__::_thesis:_(_St_is_convergent_implies_S_is_convergent_)
assume St is convergent ; ::_thesis: S is convergent
then consider xt being Point of (LinearTopSpaceNorm X) such that
A4: St is_convergent_to xt by FRECHET:def_4;
reconsider x = xt as Point of (TopSpaceNorm X) by Def4;
S is_convergent_to x by A1, A4, Th26;
hence S is convergent by FRECHET:def_4; ::_thesis: verum
end;
hence ( St is convergent iff S is convergent ) by A2; ::_thesis: verum
end;
theorem Th28: :: NORMSP_2:28
for X being RealNormSpace
for S being sequence of (TopSpaceNorm X)
for St being sequence of (LinearTopSpaceNorm X) st S = St & St is convergent holds
( Lim S = Lim St & lim S = lim St )
proof
let X be RealNormSpace; ::_thesis: for S being sequence of (TopSpaceNorm X)
for St being sequence of (LinearTopSpaceNorm X) st S = St & St is convergent holds
( Lim S = Lim St & lim S = lim St )
let S be sequence of (TopSpaceNorm X); ::_thesis: for St being sequence of (LinearTopSpaceNorm X) st S = St & St is convergent holds
( Lim S = Lim St & lim S = lim St )
let St be sequence of (LinearTopSpaceNorm X); ::_thesis: ( S = St & St is convergent implies ( Lim S = Lim St & lim S = lim St ) )
assume that
A1: S = St and
A2: St is convergent ; ::_thesis: ( Lim S = Lim St & lim S = lim St )
A3: S is convergent by A1, A2, Th27;
then consider x being Point of (TopSpaceNorm X) such that
A4: S is_convergent_to x by FRECHET:def_4;
reconsider xxt = x as Point of (LinearTopSpaceNorm X) by Def4;
St is_convergent_to xxt by A1, A4, Th26;
then A5: lim St = xxt by FRECHET2:25
.= lim S by A4, FRECHET2:25 ;
reconsider Sn = S as sequence of X ;
consider xt being Point of (LinearTopSpaceNorm X) such that
A6: Lim St = {xt} by A2, FRECHET2:24;
xt in {xt} by TARSKI:def_1;
then St is_convergent_to xt by A6, FRECHET:def_5;
then Lim St = {(lim St)} by A6, FRECHET2:25
.= {(lim Sn)} by A3, A5, Th14
.= Lim S by A3, Th14 ;
hence ( Lim S = Lim St & lim S = lim St ) by A5; ::_thesis: verum
end;
theorem :: NORMSP_2:29
for X being RealNormSpace
for S being sequence of X
for St being sequence of (LinearTopSpaceNorm X)
for x being Point of X
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
proof
let X be RealNormSpace; ::_thesis: for S being sequence of X
for St being sequence of (LinearTopSpaceNorm X)
for x being Point of X
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
let S be sequence of X; ::_thesis: for St being sequence of (LinearTopSpaceNorm X)
for x being Point of X
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
let St be sequence of (LinearTopSpaceNorm X); ::_thesis: for x being Point of X
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
let x be Point of X; ::_thesis: for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
let xt be Point of (LinearTopSpaceNorm X); ::_thesis: ( S = St & x = xt implies ( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r ) )
reconsider xxt = xt as Point of (TopSpaceNorm X) by Def4;
assume A1: ( S = St & x = xt ) ; ::_thesis: ( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )
the carrier of (LinearTopSpaceNorm X) = the carrier of (TopSpaceNorm X) by Def4;
then reconsider SSt = St as sequence of (TopSpaceNorm X) ;
( St is_convergent_to xt iff SSt is_convergent_to xxt ) by Th26;
hence ( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r ) by A1, Th12; ::_thesis: verum
end;
theorem :: NORMSP_2:30
for X being RealNormSpace
for S being sequence of X
for St being sequence of (LinearTopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
proof
let X be RealNormSpace; ::_thesis: for S being sequence of X
for St being sequence of (LinearTopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
let S be sequence of X; ::_thesis: for St being sequence of (LinearTopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
let St be sequence of (LinearTopSpaceNorm X); ::_thesis: ( S = St implies ( St is convergent iff S is convergent ) )
assume A1: S = St ; ::_thesis: ( St is convergent iff S is convergent )
the carrier of (LinearTopSpaceNorm X) = the carrier of (TopSpaceNorm X) by Def4;
then reconsider SSt = St as sequence of (TopSpaceNorm X) ;
( St is convergent iff SSt is convergent ) by Th27;
hence ( St is convergent iff S is convergent ) by A1, Th13; ::_thesis: verum
end;
theorem :: NORMSP_2:31
for X being RealNormSpace
for S being sequence of X
for St being sequence of (LinearTopSpaceNorm X) st S = St & St is convergent holds
( Lim St = {(lim S)} & lim St = lim S )
proof
let X be RealNormSpace; ::_thesis: for S being sequence of X
for St being sequence of (LinearTopSpaceNorm X) st S = St & St is convergent holds
( Lim St = {(lim S)} & lim St = lim S )
let S be sequence of X; ::_thesis: for St being sequence of (LinearTopSpaceNorm X) st S = St & St is convergent holds
( Lim St = {(lim S)} & lim St = lim S )
let St be sequence of (LinearTopSpaceNorm X); ::_thesis: ( S = St & St is convergent implies ( Lim St = {(lim S)} & lim St = lim S ) )
assume that
A1: S = St and
A2: St is convergent ; ::_thesis: ( Lim St = {(lim S)} & lim St = lim S )
the carrier of (LinearTopSpaceNorm X) = the carrier of (TopSpaceNorm X) by Def4;
then reconsider SSt = St as sequence of (TopSpaceNorm X) ;
SSt is convergent by A2, Th27;
then ( Lim SSt = {(lim S)} & lim SSt = lim S ) by A1, Th14;
hence ( Lim St = {(lim S)} & lim St = lim S ) by A2, Th28; ::_thesis: verum
end;
theorem :: NORMSP_2:32
for X being RealNormSpace
for V being Subset of X
for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is closed iff Vt is closed )
proof
let X be RealNormSpace; ::_thesis: for V being Subset of X
for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is closed iff Vt is closed )
let V be Subset of X; ::_thesis: for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is closed iff Vt is closed )
let Vt be Subset of (LinearTopSpaceNorm X); ::_thesis: ( V = Vt implies ( V is closed iff Vt is closed ) )
reconsider VVt = Vt as Subset of (TopSpaceNorm X) by Def4;
assume A1: V = Vt ; ::_thesis: ( V is closed iff Vt is closed )
( Vt is closed iff VVt is closed ) by Th21;
hence ( V is closed iff Vt is closed ) by A1, Th15; ::_thesis: verum
end;
theorem :: NORMSP_2:33
for X being RealNormSpace
for V being Subset of X
for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is open iff Vt is open )
proof
let X be RealNormSpace; ::_thesis: for V being Subset of X
for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is open iff Vt is open )
let V be Subset of X; ::_thesis: for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is open iff Vt is open )
let Vt be Subset of (LinearTopSpaceNorm X); ::_thesis: ( V = Vt implies ( V is open iff Vt is open ) )
reconsider VVt = Vt as Subset of (TopSpaceNorm X) by Def4;
assume A1: V = Vt ; ::_thesis: ( V is open iff Vt is open )
( Vt is open iff VVt is open ) by Th20;
hence ( V is open iff Vt is open ) by A1, Th16; ::_thesis: verum
end;
theorem Th34: :: NORMSP_2:34
for X being RealNormSpace
for U being Subset of (TopSpaceNorm X)
for Ut being Subset of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st U = Ut & x = xt holds
( U is a_neighborhood of x iff Ut is a_neighborhood of xt )
proof
let X be RealNormSpace; ::_thesis: for U being Subset of (TopSpaceNorm X)
for Ut being Subset of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st U = Ut & x = xt holds
( U is a_neighborhood of x iff Ut is a_neighborhood of xt )
let U be Subset of (TopSpaceNorm X); ::_thesis: for Ut being Subset of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st U = Ut & x = xt holds
( U is a_neighborhood of x iff Ut is a_neighborhood of xt )
let Ut be Subset of (LinearTopSpaceNorm X); ::_thesis: for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st U = Ut & x = xt holds
( U is a_neighborhood of x iff Ut is a_neighborhood of xt )
let x be Point of (TopSpaceNorm X); ::_thesis: for xt being Point of (LinearTopSpaceNorm X) st U = Ut & x = xt holds
( U is a_neighborhood of x iff Ut is a_neighborhood of xt )
let xt be Point of (LinearTopSpaceNorm X); ::_thesis: ( U = Ut & x = xt implies ( U is a_neighborhood of x iff Ut is a_neighborhood of xt ) )
assume that
A1: U = Ut and
A2: x = xt ; ::_thesis: ( U is a_neighborhood of x iff Ut is a_neighborhood of xt )
hereby ::_thesis: ( Ut is a_neighborhood of xt implies U is a_neighborhood of x )
assume U is a_neighborhood of x ; ::_thesis: Ut is a_neighborhood of xt
then consider V being Subset of (TopSpaceNorm X) such that
A3: V is open and
A4: V c= U and
A5: x in V by CONNSP_2:6;
reconsider Vt = V as open Subset of (LinearTopSpaceNorm X) by A3, Def4, Th20;
Vt c= Ut by A1, A4;
hence Ut is a_neighborhood of xt by A2, A5, CONNSP_2:6; ::_thesis: verum
end;
assume Ut is a_neighborhood of xt ; ::_thesis: U is a_neighborhood of x
then consider Vt being Subset of (LinearTopSpaceNorm X) such that
A6: Vt is open and
A7: Vt c= Ut and
A8: xt in Vt by CONNSP_2:6;
reconsider V = Vt as open Subset of (TopSpaceNorm X) by A6, Def4, Th20;
V c= U by A1, A7;
hence U is a_neighborhood of x by A2, A8, CONNSP_2:6; ::_thesis: verum
end;
theorem Th35: :: NORMSP_2:35
for X, Y being RealNormSpace
for f being Function of (TopSpaceNorm X),(TopSpaceNorm Y)
for ft being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_at x iff ft is_continuous_at xt )
proof
let X, Y be RealNormSpace; ::_thesis: for f being Function of (TopSpaceNorm X),(TopSpaceNorm Y)
for ft being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_at x iff ft is_continuous_at xt )
let f be Function of (TopSpaceNorm X),(TopSpaceNorm Y); ::_thesis: for ft being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_at x iff ft is_continuous_at xt )
let ft be Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y); ::_thesis: for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_at x iff ft is_continuous_at xt )
let x be Point of (TopSpaceNorm X); ::_thesis: for xt being Point of (LinearTopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_at x iff ft is_continuous_at xt )
let xt be Point of (LinearTopSpaceNorm X); ::_thesis: ( f = ft & x = xt implies ( f is_continuous_at x iff ft is_continuous_at xt ) )
assume that
A1: f = ft and
A2: x = xt ; ::_thesis: ( f is_continuous_at x iff ft is_continuous_at xt )
hereby ::_thesis: ( ft is_continuous_at xt implies f is_continuous_at x )
assume A3: f is_continuous_at x ; ::_thesis: ft is_continuous_at xt
now__::_thesis:_for_Gt_being_a_neighborhood_of_ft_._xt_ex_Ht_being_a_neighborhood_of_xt_st_ft_.:_Ht_c=_Gt
let Gt be a_neighborhood of ft . xt; ::_thesis: ex Ht being a_neighborhood of xt st ft .: Ht c= Gt
Gt is Subset of (TopSpaceNorm Y) by Def4;
then reconsider G = Gt as a_neighborhood of f . x by A1, A2, Th34;
consider H being a_neighborhood of x such that
A4: f .: H c= G by A3, TMAP_1:def_2;
H is Subset of (LinearTopSpaceNorm X) by Def4;
then reconsider Ht = H as a_neighborhood of xt by A2, Th34;
take Ht = Ht; ::_thesis: ft .: Ht c= Gt
thus ft .: Ht c= Gt by A1, A4; ::_thesis: verum
end;
hence ft is_continuous_at xt by TMAP_1:def_2; ::_thesis: verum
end;
assume A5: ft is_continuous_at xt ; ::_thesis: f is_continuous_at x
now__::_thesis:_for_G_being_a_neighborhood_of_f_._x_ex_H_being_a_neighborhood_of_x_st_f_.:_H_c=_G
let G be a_neighborhood of f . x; ::_thesis: ex H being a_neighborhood of x st f .: H c= G
G is Subset of (LinearTopSpaceNorm Y) by Def4;
then reconsider Gt = G as a_neighborhood of ft . xt by A1, A2, Th34;
consider Ht being a_neighborhood of xt such that
A6: ft .: Ht c= Gt by A5, TMAP_1:def_2;
Ht is Subset of (TopSpaceNorm X) by Def4;
then reconsider H = Ht as a_neighborhood of x by A2, Th34;
take H = H; ::_thesis: f .: H c= G
thus f .: H c= G by A1, A6; ::_thesis: verum
end;
hence f is_continuous_at x by TMAP_1:def_2; ::_thesis: verum
end;
theorem :: NORMSP_2:36
for X, Y being RealNormSpace
for f being Function of (TopSpaceNorm X),(TopSpaceNorm Y)
for ft being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y) st f = ft holds
( f is continuous iff ft is continuous )
proof
let X, Y be RealNormSpace; ::_thesis: for f being Function of (TopSpaceNorm X),(TopSpaceNorm Y)
for ft being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y) st f = ft holds
( f is continuous iff ft is continuous )
let f be Function of (TopSpaceNorm X),(TopSpaceNorm Y); ::_thesis: for ft being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y) st f = ft holds
( f is continuous iff ft is continuous )
let ft be Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y); ::_thesis: ( f = ft implies ( f is continuous iff ft is continuous ) )
assume A1: f = ft ; ::_thesis: ( f is continuous iff ft is continuous )
hereby ::_thesis: ( ft is continuous implies f is continuous )
assume A2: f is continuous ; ::_thesis: ft is continuous
now__::_thesis:_for_xt_being_Point_of_(LinearTopSpaceNorm_X)_holds_ft_is_continuous_at_xt
let xt be Point of (LinearTopSpaceNorm X); ::_thesis: ft is_continuous_at xt
reconsider x = xt as Point of (TopSpaceNorm X) by Def4;
f is_continuous_at x by A2, TMAP_1:44;
hence ft is_continuous_at xt by A1, Th35; ::_thesis: verum
end;
hence ft is continuous by TMAP_1:44; ::_thesis: verum
end;
assume A3: ft is continuous ; ::_thesis: f is continuous
now__::_thesis:_for_x_being_Point_of_(TopSpaceNorm_X)_holds_f_is_continuous_at_x
let x be Point of (TopSpaceNorm X); ::_thesis: f is_continuous_at x
reconsider xt = x as Point of (LinearTopSpaceNorm X) by Def4;
ft is_continuous_at xt by A3, TMAP_1:44;
hence f is_continuous_at x by A1, Th35; ::_thesis: verum
end;
hence f is continuous by TMAP_1:44; ::_thesis: verum
end;