:: 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;