:: The Continuous Functions on Normed Linear Spaces :: by Takaya Nishiyama, Keiji Ohkubo and Yasunari Shidama :: :: Received April 6, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users begin theorem :: NFCONT_1:1 for S being non empty addLoopStr for seq1, seq2 being sequence of S holds seq1 - seq2 = seq1 + (- seq2) proofend; theorem Th2: :: NFCONT_1:2 for S being RealNormSpace for seq being sequence of S holds - seq = (- 1) * seq proofend; definition let S be RealNormSpace; let x0 be Point of S; mode Neighbourhood of x0 -> Subset of S means :Def1: :: NFCONT_1:def 1 ex g being Real st ( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= it ); existence ex b1 being Subset of S ex g being Real st ( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= b1 ) proofend; end; :: deftheorem Def1 defines Neighbourhood NFCONT_1:def_1_:_ for S being RealNormSpace for x0 being Point of S for b3 being Subset of S holds ( b3 is Neighbourhood of x0 iff ex g being Real st ( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= b3 ) ); theorem Th3: :: NFCONT_1:3 for S being RealNormSpace for x0 being Point of S for g being Real st 0 < g holds { y where y is Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0 proofend; theorem Th4: :: NFCONT_1:4 for S being RealNormSpace for x0 being Point of S for N being Neighbourhood of x0 holds x0 in N proofend; definition let S be RealNormSpace; let X be Subset of S; attrX is compact means :Def2: :: NFCONT_1:def 2 for s1 being sequence of S st rng s1 c= X holds ex s2 being sequence of S st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ); end; :: deftheorem Def2 defines compact NFCONT_1:def_2_:_ for S being RealNormSpace for X being Subset of S holds ( X is compact iff for s1 being sequence of S st rng s1 c= X holds ex s2 being sequence of S st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) ); definition let S be RealNormSpace; let X be Subset of S; attrX is closed means :: NFCONT_1:def 3 for s1 being sequence of S st rng s1 c= X & s1 is convergent holds lim s1 in X; end; :: deftheorem defines closed NFCONT_1:def_3_:_ for S being RealNormSpace for X being Subset of S holds ( X is closed iff for s1 being sequence of S st rng s1 c= X & s1 is convergent holds lim s1 in X ); definition let S be RealNormSpace; let X be Subset of S; attrX is open means :: NFCONT_1:def 4 X ` is closed ; end; :: deftheorem defines open NFCONT_1:def_4_:_ for S being RealNormSpace for X being Subset of S holds ( X is open iff X ` is closed ); definition let S, T be RealNormSpace; let f be PartFunc of S,T; let x0 be Point of S; predf is_continuous_in x0 means :Def5: :: NFCONT_1:def 5 ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ); end; :: deftheorem Def5 defines is_continuous_in NFCONT_1:def_5_:_ for S, T being RealNormSpace for f being PartFunc of S,T for x0 being Point of S holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ); definition let S be RealNormSpace; let f be PartFunc of the carrier of S,REAL; let x0 be Point of S; predf is_continuous_in x0 means :Def6: :: NFCONT_1:def 6 ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ); end; :: deftheorem Def6 defines is_continuous_in NFCONT_1:def_6_:_ for S being RealNormSpace for f being PartFunc of the carrier of S,REAL for x0 being Point of S holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ); theorem Th5: :: NFCONT_1:5 for n being Element of NAT for S, T being RealNormSpace for seq being sequence of S for h being PartFunc of S,T st rng seq c= dom h holds seq . n in dom h proofend; theorem Th6: :: NFCONT_1:6 for S being RealNormSpace for seq being sequence of S for x being set holds ( x in rng seq iff ex n being Element of NAT st x = seq . n ) proofend; theorem Th7: :: NFCONT_1:7 for T, S being RealNormSpace for f being PartFunc of S,T for x0 being Point of S holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ) proofend; theorem Th8: :: NFCONT_1:8 for S being RealNormSpace for x0 being Point of S for f being PartFunc of the carrier of S,REAL holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ) ) ) proofend; theorem Th9: :: NFCONT_1:9 for T, S being RealNormSpace for f being PartFunc of S,T for x0 being Point of S holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st for x1 being Point of S st x1 in dom f & x1 in N holds f /. x1 in N1 ) ) ) proofend; theorem Th10: :: NFCONT_1:10 for T, S being RealNormSpace for f being PartFunc of S,T for x0 being Point of S holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) ) ) proofend; theorem :: NFCONT_1:11 for T, S being RealNormSpace for f being PartFunc of S,T for x0 being Point of S st x0 in dom f & ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds f is_continuous_in x0 proofend; theorem Th12: :: NFCONT_1:12 for S, T being RealNormSpace for h1, h2 being PartFunc of S,T for seq being sequence of S st rng seq c= (dom h1) /\ (dom h2) holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) proofend; theorem Th13: :: NFCONT_1:13 for S, T being RealNormSpace for h being PartFunc of S,T for seq being sequence of S for r being Real st rng seq c= dom h holds (r (#) h) /* seq = r * (h /* seq) proofend; theorem Th14: :: NFCONT_1:14 for S, T being RealNormSpace for h being PartFunc of S,T for seq being sequence of S st rng seq c= dom h holds ( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq ) proofend; theorem :: NFCONT_1:15 for T, S being RealNormSpace for f1, f2 being PartFunc of S,T for x0 being Point of S st f1 is_continuous_in x0 & f2 is_continuous_in x0 holds ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 ) proofend; theorem Th16: :: NFCONT_1:16 for r being Real for T, S being RealNormSpace for f being PartFunc of S,T for x0 being Point of S st f is_continuous_in x0 holds r (#) f is_continuous_in x0 proofend; theorem :: NFCONT_1:17 for T, S being RealNormSpace for f being PartFunc of S,T for x0 being Point of S st f is_continuous_in x0 holds ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 ) proofend; definition let S, T be RealNormSpace; let f be PartFunc of S,T; let X be set ; predf is_continuous_on X means :Def7: :: NFCONT_1:def 7 ( X c= dom f & ( for x0 being Point of S st x0 in X holds f | X is_continuous_in x0 ) ); end; :: deftheorem Def7 defines is_continuous_on NFCONT_1:def_7_:_ for S, T being RealNormSpace for f being PartFunc of S,T for X being set holds ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S st x0 in X holds f | X is_continuous_in x0 ) ) ); definition let S be RealNormSpace; let f be PartFunc of the carrier of S,REAL; let X be set ; predf is_continuous_on X means :Def8: :: NFCONT_1:def 8 ( X c= dom f & ( for x0 being Point of S st x0 in X holds f | X is_continuous_in x0 ) ); end; :: deftheorem Def8 defines is_continuous_on NFCONT_1:def_8_:_ for S being RealNormSpace for f being PartFunc of the carrier of S,REAL for X being set holds ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S st x0 in X holds f | X is_continuous_in x0 ) ) ); theorem Th18: :: NFCONT_1:18 for T, S being RealNormSpace for X being set for f being PartFunc of S,T holds ( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of S st rng s1 c= X & s1 is convergent & lim s1 in X holds ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) ) proofend; theorem Th19: :: NFCONT_1:19 for X being set for T, S being RealNormSpace for f being PartFunc of S,T holds ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ) proofend; theorem :: NFCONT_1:20 for X being set for S being RealNormSpace for f being PartFunc of the carrier of S,REAL holds ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ) ) ) proofend; theorem :: NFCONT_1:21 for X being set for S, T being RealNormSpace for f being PartFunc of S,T holds ( f is_continuous_on X iff f | X is_continuous_on X ) proofend; theorem Th22: :: NFCONT_1:22 for X being set for S being RealNormSpace for f being PartFunc of the carrier of S,REAL holds ( f is_continuous_on X iff f | X is_continuous_on X ) proofend; theorem Th23: :: NFCONT_1:23 for X, X1 being set for S, T being RealNormSpace for f being PartFunc of S,T st f is_continuous_on X & X1 c= X holds f is_continuous_on X1 proofend; theorem :: NFCONT_1:24 for T, S being RealNormSpace for f being PartFunc of S,T for x0 being Point of S st x0 in dom f holds f is_continuous_on {x0} proofend; theorem Th25: :: NFCONT_1:25 for T, S being RealNormSpace for X being set for f1, f2 being PartFunc of S,T st f1 is_continuous_on X & f2 is_continuous_on X holds ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X ) proofend; theorem :: NFCONT_1:26 for T, S being RealNormSpace for X, X1 being set for f1, f2 being PartFunc of S,T st f1 is_continuous_on X & f2 is_continuous_on X1 holds ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 ) proofend; theorem Th27: :: NFCONT_1:27 for T, S being RealNormSpace for r being Real for X being set for f being PartFunc of S,T st f is_continuous_on X holds r (#) f is_continuous_on X proofend; theorem Th28: :: NFCONT_1:28 for X being set for S, T being RealNormSpace for f being PartFunc of S,T st f is_continuous_on X holds ( ||.f.|| is_continuous_on X & - f is_continuous_on X ) proofend; theorem :: NFCONT_1:29 for T, S being RealNormSpace for f being PartFunc of S,T st f is total & ( for x1, x2 being Point of S holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Point of S st f is_continuous_in x0 holds f is_continuous_on the carrier of S proofend; theorem Th30: :: NFCONT_1:30 for T, S being RealNormSpace for f being PartFunc of S,T st dom f is compact & f is_continuous_on dom f holds rng f is compact proofend; theorem Th31: :: NFCONT_1:31 for S being RealNormSpace for f being PartFunc of the carrier of S,REAL st dom f is compact & f is_continuous_on dom f holds rng f is compact proofend; theorem :: NFCONT_1:32 for T, S being RealNormSpace for f being PartFunc of S,T for Y being Subset of S st Y c= dom f & Y is compact & f is_continuous_on Y holds f .: Y is compact proofend; theorem Th33: :: NFCONT_1:33 for S being RealNormSpace for f being PartFunc of the carrier of S,REAL st dom f <> {} & dom f is compact & f is_continuous_on dom f holds ex x1, x2 being Point of S st ( x1 in dom f & x2 in dom f & f /. x1 = upper_bound (rng f) & f /. x2 = lower_bound (rng f) ) proofend; theorem Th34: :: NFCONT_1:34 for T, S being RealNormSpace for f being PartFunc of S,T st dom f <> {} & dom f is compact & f is_continuous_on dom f holds ex x1, x2 being Point of S st ( x1 in dom f & x2 in dom f & ||.f.|| /. x1 = upper_bound (rng ||.f.||) & ||.f.|| /. x2 = lower_bound (rng ||.f.||) ) proofend; theorem Th35: :: NFCONT_1:35 for X being set for S, T being RealNormSpace for f being PartFunc of S,T holds ||.f.|| | X = ||.(f | X).|| proofend; theorem :: NFCONT_1:36 for T, S being RealNormSpace for f being PartFunc of S,T for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds ex x1, x2 being Point of S st ( x1 in Y & x2 in Y & ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) ) proofend; theorem :: NFCONT_1:37 for S being RealNormSpace for f being PartFunc of the carrier of S,REAL for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds ex x1, x2 being Point of S st ( x1 in Y & x2 in Y & f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) proofend; definition let S, T be RealNormSpace; let X be set ; let f be PartFunc of S,T; predf is_Lipschitzian_on X means :Def9: :: NFCONT_1:def 9 ( X c= dom f & ex r being Real st ( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) ) ); end; :: deftheorem Def9 defines is_Lipschitzian_on NFCONT_1:def_9_:_ for S, T being RealNormSpace for X being set for f being PartFunc of S,T holds ( f is_Lipschitzian_on X iff ( X c= dom f & ex r being Real st ( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) ) ) ); definition let S be RealNormSpace; let X be set ; let f be PartFunc of the carrier of S,REAL; predf is_Lipschitzian_on X means :Def10: :: NFCONT_1:def 10 ( X c= dom f & ex r being Real st ( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds abs ((f /. x1) - (f /. x2)) <= r * ||.(x1 - x2).|| ) ) ); end; :: deftheorem Def10 defines is_Lipschitzian_on NFCONT_1:def_10_:_ for S being RealNormSpace for X being set for f being PartFunc of the carrier of S,REAL holds ( f is_Lipschitzian_on X iff ( X c= dom f & ex r being Real st ( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds abs ((f /. x1) - (f /. x2)) <= r * ||.(x1 - x2).|| ) ) ) ); theorem Th38: :: NFCONT_1:38 for X, X1 being set for S, T being RealNormSpace for f being PartFunc of S,T st f is_Lipschitzian_on X & X1 c= X holds f is_Lipschitzian_on X1 proofend; theorem :: NFCONT_1:39 for X, X1 being set for S, T being RealNormSpace for f1, f2 being PartFunc of S,T st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds f1 + f2 is_Lipschitzian_on X /\ X1 proofend; theorem :: NFCONT_1:40 for X, X1 being set for S, T being RealNormSpace for f1, f2 being PartFunc of S,T st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds f1 - f2 is_Lipschitzian_on X /\ X1 proofend; theorem Th41: :: NFCONT_1:41 for X being set for p being Real for S, T being RealNormSpace for f being PartFunc of S,T st f is_Lipschitzian_on X holds p (#) f is_Lipschitzian_on X proofend; theorem :: NFCONT_1:42 for X being set for S, T being RealNormSpace for f being PartFunc of S,T st f is_Lipschitzian_on X holds ( - f is_Lipschitzian_on X & ||.f.|| is_Lipschitzian_on X ) proofend; theorem Th43: :: NFCONT_1:43 for X being set for S, T being RealNormSpace for f being PartFunc of S,T st X c= dom f & f | X is V23() holds f is_Lipschitzian_on X proofend; theorem :: NFCONT_1:44 for S being RealNormSpace for Y being Subset of S holds id Y is_Lipschitzian_on Y proofend; theorem Th45: :: NFCONT_1:45 for X being set for S, T being RealNormSpace for f being PartFunc of S,T st f is_Lipschitzian_on X holds f is_continuous_on X proofend; theorem Th46: :: NFCONT_1:46 for X being set for S being RealNormSpace for f being PartFunc of the carrier of S,REAL st f is_Lipschitzian_on X holds f is_continuous_on X proofend; theorem :: NFCONT_1:47 for T, S being RealNormSpace for f being PartFunc of S,T st ex r being Point of T st rng f = {r} holds f is_continuous_on dom f proofend; theorem :: NFCONT_1:48 for X being set for S, T being RealNormSpace for f being PartFunc of S,T st X c= dom f & f | X is V23() holds f is_continuous_on X by Th43, Th45; theorem Th49: :: NFCONT_1:49 for S being RealNormSpace for f being PartFunc of S,S st ( for x0 being Point of S st x0 in dom f holds f /. x0 = x0 ) holds f is_continuous_on dom f proofend; theorem :: NFCONT_1:50 for S being RealNormSpace for f being PartFunc of S,S st f = id (dom f) holds f is_continuous_on dom f proofend; theorem :: NFCONT_1:51 for S being RealNormSpace for Y being Subset of S for f being PartFunc of S,S st Y c= dom f & f | Y = id Y holds f is_continuous_on Y proofend; theorem :: NFCONT_1:52 for X being set for S being RealNormSpace for f being PartFunc of S,S for r being Real for p being Point of S st X c= dom f & ( for x0 being Point of S st x0 in X holds f /. x0 = (r * x0) + p ) holds f is_continuous_on X proofend; theorem Th53: :: NFCONT_1:53 for S being RealNormSpace for f being PartFunc of the carrier of S,REAL st ( for x0 being Point of S st x0 in dom f holds f /. x0 = ||.x0.|| ) holds f is_continuous_on dom f proofend; theorem :: NFCONT_1:54 for X being set for S being RealNormSpace for f being PartFunc of the carrier of S,REAL st X c= dom f & ( for x0 being Point of S st x0 in X holds f /. x0 = ||.x0.|| ) holds f is_continuous_on X proofend;