:: Functional Space Consisted by Continuous Functions on Topological Space
:: by Hiroshi Yamazaki , Keiichi Miyajima and Yasunari Shidama
::
:: Copyright (c) 2021 Association of Mizar Users

theorem Th1: :: C0SP3:1
for X being non empty TopSpace
for S being LinearTopSpace
for f, g being Function of X,S
for x being Point of X st f is_continuous_at x & g is_continuous_at x holds
f + g is_continuous_at x
proof end;

theorem Th2: :: C0SP3:2
for X being non empty TopSpace
for S being LinearTopSpace
for f being Function of X,S
for x being Point of X
for a being Real st f is_continuous_at x holds
a (#) f is_continuous_at x
proof end;

theorem Th3: :: C0SP3:3
for X being non empty TopSpace
for S being LinearTopSpace
for f, g being Function of X,S st f is continuous & g is continuous holds
f + g is continuous
proof end;

theorem Th4: :: C0SP3:4
for X being non empty TopSpace
for S being LinearTopSpace
for f being Function of X,S
for a being Real st f is continuous holds
a (#) f is continuous
proof end;

definition
let S be non empty TopSpace;
let T be LinearTopSpace;
func ContinuousFunctions (S,T) -> Subset of (RealVectSpace ( the carrier of S,T)) equals :: C0SP3:def 1
{ f where f is Function of the carrier of S, the carrier of T : f is continuous } ;
correctness
coherence
{ f where f is Function of the carrier of S, the carrier of T : f is continuous } is Subset of (RealVectSpace ( the carrier of S,T))
;
proof end;
end;

:: deftheorem defines ContinuousFunctions C0SP3:def 1 :
for S being non empty TopSpace
for T being LinearTopSpace holds ContinuousFunctions (S,T) = { f where f is Function of the carrier of S, the carrier of T : f is continuous } ;

registration
let S be non empty TopSpace;
let T be LinearTopSpace;
cluster ContinuousFunctions (S,T) -> functional non empty ;
coherence
( not ContinuousFunctions (S,T) is empty & ContinuousFunctions (S,T) is functional )
proof end;
end;

theorem Th5: :: C0SP3:5
for S being non empty TopSpace
for T being LinearTopSpace holds ContinuousFunctions (S,T) is linearly-closed
proof end;

theorem :: C0SP3:6
for S being non empty TopSpace
for T being LinearTopSpace holds RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is Subspace of RealVectSpace ( the carrier of S,T) by ;

registration
let S be non empty TopSpace;
let T be LinearTopSpace;
cluster RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is Abelian & RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is add-associative & RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is right_zeroed & RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is right_complementable & RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is vector-distributive & RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is scalar-distributive & RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is scalar-associative & RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is scalar-unital )
by ;
end;

definition
let S be non empty TopSpace;
let T be LinearTopSpace;
func R_VectorSpace_of_ContinuousFunctions (S,T) -> strict RealLinearSpace equals :: C0SP3:def 2
RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #);
coherence
RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is strict RealLinearSpace
;
end;

:: deftheorem defines R_VectorSpace_of_ContinuousFunctions C0SP3:def 2 :
for S being non empty TopSpace
for T being LinearTopSpace holds R_VectorSpace_of_ContinuousFunctions (S,T) = RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #);

registration
let S be non empty TopSpace;
let T be LinearTopSpace;
coherence by MONOID_0:80;
end;

definition
let S be non empty TopSpace;
let T be LinearTopSpace;
let f be VECTOR of ;
let v be Element of S;
:: original: .
redefine func f . v -> VECTOR of T;
correctness
coherence
f . v is VECTOR of T
;
proof end;
end;

theorem Th7: :: C0SP3:7
for S being non empty TopSpace
for T being LinearTopSpace
for f, g, h being VECTOR of holds
( h = f + g iff for x being Element of S holds h . x = (f . x) + (g . x) )
proof end;

theorem Th8: :: C0SP3:8
for S being non empty TopSpace
for T being LinearTopSpace
for f, h being VECTOR of
for a being Real holds
( h = a * f iff for x being Element of S holds h . x = a * (f . x) )
proof end;

theorem Th9: :: C0SP3:9
for S being non empty TopSpace
for T being LinearTopSpace holds 0. = the carrier of S --> (0. T)
proof end;

registration
let S be non empty TopSpace;
let T be LinearTopSpace;
cluster the carrier of -> functional ;
coherence
the carrier of is functional
;
end;

theorem Th10: :: C0SP3:10
for S, T being RealNormSpace
for x being Point of T holds the carrier of S --> x is_continuous_on the carrier of S
proof end;

definition
let S, T be RealNormSpace;
func ContinuousFunctions (S,T) -> Subset of (RealVectSpace ( the carrier of S,T)) equals :: C0SP3:def 3
{ f where f is Function of the carrier of S, the carrier of T : f is_continuous_on the carrier of S } ;
correctness
coherence
{ f where f is Function of the carrier of S, the carrier of T : f is_continuous_on the carrier of S } is Subset of (RealVectSpace ( the carrier of S,T))
;
proof end;
end;

:: deftheorem defines ContinuousFunctions C0SP3:def 3 :
for S, T being RealNormSpace holds ContinuousFunctions (S,T) = { f where f is Function of the carrier of S, the carrier of T : f is_continuous_on the carrier of S } ;

registration
let S, T be RealNormSpace;
cluster ContinuousFunctions (S,T) -> functional non empty ;
coherence
( not ContinuousFunctions (S,T) is empty & ContinuousFunctions (S,T) is functional )
proof end;
end;

theorem Th11: :: C0SP3:11
for S, T being RealNormSpace holds ContinuousFunctions (S,T) is linearly-closed
proof end;

theorem :: C0SP3:12
for S, T being RealNormSpace holds RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is Subspace of RealVectSpace ( the carrier of S,T) by ;

registration
let S, T be RealNormSpace;
cluster RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is Abelian & RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is add-associative & RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is right_zeroed & RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is right_complementable & RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is vector-distributive & RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is scalar-distributive & RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is scalar-associative & RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is scalar-unital )
by ;
end;

definition
let S, T be RealNormSpace;
func R_VectorSpace_of_ContinuousFunctions (S,T) -> strict RealLinearSpace equals :: C0SP3:def 4
RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #);
coherence
RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is strict RealLinearSpace
;
end;

:: deftheorem defines R_VectorSpace_of_ContinuousFunctions C0SP3:def 4 :
for S, T being RealNormSpace holds R_VectorSpace_of_ContinuousFunctions (S,T) = RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #);

registration
let S, T be RealNormSpace;
coherence by MONOID_0:80;
end;

definition
let S, T be RealNormSpace;
let f be VECTOR of ;
let v be Element of S;
:: original: .
redefine func f . v -> VECTOR of T;
correctness
coherence
f . v is VECTOR of T
;
proof end;
end;

theorem :: C0SP3:13
for S, T being RealNormSpace
for f, g, h being VECTOR of holds
( h = f + g iff for x being Element of S holds h . x = (f . x) + (g . x) )
proof end;

theorem :: C0SP3:14
for S, T being RealNormSpace
for f, h being VECTOR of
for a being Real holds
( h = a * f iff for x being Element of S holds h . x = a * (f . x) )
proof end;

theorem :: C0SP3:15
for S, T being RealNormSpace holds R_VectorSpace_of_ContinuousFunctions (S,T) is Subspace of RealVectSpace ( the carrier of S,T) by ;

theorem :: C0SP3:16
for S, T being RealNormSpace holds 0. = the carrier of S --> (0. T)
proof end;

definition
let S, T be RealNormSpace;
let f be object ;
assume A1: f in ContinuousFunctions (S,T) ;
func modetrans (f,S,T) -> Function of S,T means :: C0SP3:def 5
( it = f & it is_continuous_on the carrier of S );
existence
ex b1 being Function of S,T st
( b1 = f & b1 is_continuous_on the carrier of S )
by A1;
uniqueness
for b1, b2 being Function of S,T st b1 = f & b1 is_continuous_on the carrier of S & b2 = f & b2 is_continuous_on the carrier of S holds
b1 = b2
;
end;

:: deftheorem defines modetrans C0SP3:def 5 :
for S, T being RealNormSpace
for f being object st f in ContinuousFunctions (S,T) holds
for b4 being Function of S,T holds
( b4 = modetrans (f,S,T) iff ( b4 = f & b4 is_continuous_on the carrier of S ) );

definition end;

registration
let X be non empty set ;
let O be Element of X;
let F be BinOp of X;
let G be Function of [:REAL,X:],X;
let T be Subset-Family of X;
let N be Function of X,REAL;
cluster RLNormTopStruct(# X,O,F,G,T,N #) -> non empty ;
coherence
not RLNormTopStruct(# X,O,F,G,T,N #) is empty
;
end;

registration
existence
ex b1 being RLNormTopStruct st
( b1 is strict & not b1 is empty )
proof end;
end;

definition
let X be non empty RLNormTopStruct ;
attr X is norm-generated means :Def7: :: C0SP3:def 6
ex RNS being RealNormSpace st
( RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) );
end;

:: deftheorem Def7 defines norm-generated C0SP3:def 6 :
for X being non empty RLNormTopStruct holds
( X is norm-generated iff ex RNS being RealNormSpace st
( RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) ) );

registration
existence
ex b1 being non empty RLNormTopStruct st
( b1 is strict & b1 is add-continuous & b1 is Mult-continuous & b1 is TopSpace-like & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is discerning & b1 is reflexive & b1 is RealNormSpace-like & b1 is norm-generated & b1 is T_2 )
proof end;
end;

definition end;

theorem :: C0SP3:17
for X being NormedLinearTopSpace holds X is LinearTopSpace ;

theorem :: C0SP3:18
for X being NormedLinearTopSpace holds X is RealNormSpace ;

theorem Th19: :: C0SP3:19
for X being NormedLinearTopSpace
for RNS being RealNormSpace st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) holds
for x, y being Point of X
for x1, y1 being Point of RNS
for a being Real st x1 = x & y1 = y holds
( x + y = x1 + y1 & a * x = a * x1 & x - y = x1 - y1 & = ||.x1.|| )
proof end;

theorem Th20: :: C0SP3:20
for X being NormedLinearTopSpace
for S being sequence of X
for x being Point of X holds
( S is_convergent_to x iff for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r )
proof end;

theorem Th21: :: C0SP3:21
for X being NormedLinearTopSpace
for S being sequence of X
for x being Point of X holds
( ( S is convergent & x = lim S ) iff for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r )
proof end;

theorem Th22: :: C0SP3:22
for X being NormedLinearTopSpace
for S being sequence of X st S is convergent holds
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - (lim S)).|| < r
proof end;

theorem Th23: :: C0SP3:23
for X being NormedLinearTopSpace
for V being Subset of 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 end;

theorem Th24: :: C0SP3:24
for X being NormedLinearTopSpace
for x being Point of X
for r being Real
for V being Subset of X st V = { y where y is Point of X : ||.(x - y).|| < r } holds
V is open
proof end;

theorem :: C0SP3:25
for X being NormedLinearTopSpace
for x being Point of X
for r being Real
for V being Subset of X st V = { y where y is Point of X : ||.(x - y).|| <= r } holds
V is closed
proof end;

theorem Th26: :: C0SP3:26
for X being NormedLinearTopSpace
for RNS being RealNormSpace
for t being sequence of X
for s being sequence of RNS st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & t = s & t is convergent holds
( s is convergent & lim s = lim t )
proof end;

theorem Th27: :: C0SP3:27
for X being NormedLinearTopSpace
for RNS being RealNormSpace
for s being sequence of X
for t being sequence of RNS st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & s = t holds
( s is convergent iff t is convergent )
proof end;

theorem Th28: :: C0SP3:28
for X being NormedLinearTopSpace
for V being Subset of X holds
( V is closed iff for s1 being sequence of X st rng s1 c= V & s1 is convergent holds
lim s1 in V )
proof end;

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

theorem :: C0SP3:29
for X being NormedLinearTopSpace
for RNS being RealNormSpace
for V being Subset of X
for W being Subset of RNS st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) & V = W holds
( V is closed iff W is closed )
proof end;

theorem Th30: :: C0SP3:30
for X being NormedLinearTopSpace
for V being Subset of X
for x being Point of X holds
( V is a_neighborhood of x iff ex r being Real st
( r > 0 & { y where y is Point of X : ||.(y - x).|| < r } c= V ) )
proof end;

theorem Th31: :: C0SP3:31
for X being NormedLinearTopSpace
for V being Subset of X holds
( V is compact iff for s1 being sequence of X st rng s1 c= V holds
ex s2 being sequence of X st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in V ) )
proof end;

theorem Th32: :: C0SP3:32
for X being NormedLinearTopSpace
for RNS being RealNormSpace
for V being Subset of X
for W being Subset of RNS st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) & V = W holds
( V is compact iff W is compact )
proof end;

theorem Th33: :: C0SP3:33
for X, X1 being set
for S being RealNormSpace
for f being PartFunc of S,REAL st f is_continuous_on X & X1 c= X holds
f is_continuous_on X1
proof end;

Lm2: for S being non empty TopSpace
for T being NormedLinearTopSpace
for f being Function of S,T
for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is continuous holds
ex K being Real st
( 0 <= K & ( for x being Point of S st x in Y holds
||.(f . x).|| <= K ) )

proof end;

theorem Th34: :: C0SP3:34
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for x being set st x in ContinuousFunctions (S,T) holds
x in BoundedFunctions ( the carrier of S,T)
proof end;

theorem :: C0SP3:35
for S being non empty compact TopSpace
for T being NormedLinearTopSpace holds R_VectorSpace_of_ContinuousFunctions (S,T) is Subspace of R_VectorSpace_of_BoundedFunctions ( the carrier of S,T)
proof end;

definition
let S be non empty compact TopSpace;
let T be NormedLinearTopSpace;
func ContinuousFunctionsNorm (S,T) -> Function of (ContinuousFunctions (S,T)),REAL equals :: C0SP3:def 7
(BoundedFunctionsNorm ( the carrier of S,T)) | (ContinuousFunctions (S,T));
correctness
coherence
(BoundedFunctionsNorm ( the carrier of S,T)) | (ContinuousFunctions (S,T)) is Function of (ContinuousFunctions (S,T)),REAL
;
proof end;
end;

:: deftheorem defines ContinuousFunctionsNorm C0SP3:def 7 :
for S being non empty compact TopSpace
for T being NormedLinearTopSpace holds ContinuousFunctionsNorm (S,T) = (BoundedFunctionsNorm ( the carrier of S,T)) | (ContinuousFunctions (S,T));

definition
let S be non empty compact TopSpace;
let T be NormedLinearTopSpace;
func R_NormSpace_of_ContinuousFunctions (S,T) -> strict NORMSTR equals :: C0SP3:def 8
NORMSTR(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),() #);
correctness
coherence
NORMSTR(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),() #) is strict NORMSTR
;
;
end;

:: deftheorem defines R_NormSpace_of_ContinuousFunctions C0SP3:def 8 :
for S being non empty compact TopSpace
for T being NormedLinearTopSpace holds R_NormSpace_of_ContinuousFunctions (S,T) = NORMSTR(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),() #);

registration
let S be non empty compact TopSpace;
let T be NormedLinearTopSpace;
correctness
coherence
not R_NormSpace_of_ContinuousFunctions (S,T) is empty
;
;
end;

theorem Th36: :: C0SP3:36
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for x being Point of
for y being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st x = y holds
= by FUNCT_1:49;

theorem :: C0SP3:37
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for f being Point of
for g being Function of S,T st f = g holds
for t being Point of S holds ||.(g . t).|| <=
proof end;

theorem Th38: :: C0SP3:38
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for x1, x2 being Point of
for y1, y2 being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
proof end;

theorem Th39: :: C0SP3:39
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for a being Real
for x being Point of
for y being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st x = y holds
a * x = a * y
proof end;

registration
let S be non empty compact TopSpace;
let T be NormedLinearTopSpace;
coherence
proof end;
end;

theorem Th40: :: C0SP3:40
for S being non empty compact TopSpace
for T being NormedLinearTopSpace holds the carrier of S --> (0. T) = 0.
proof end;

theorem Th41: :: C0SP3:41
for S being non empty compact TopSpace
for T being NormedLinearTopSpace holds 0. = 0. (R_NormSpace_of_BoundedFunctions ( the carrier of S,T))
proof end;

theorem :: C0SP3:42
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for F being Point of holds 0 <=
proof end;

theorem :: C0SP3:43
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for F being Point of st F = 0. holds
0 =
proof end;

theorem Th44: :: C0SP3:44
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for F, G, H being Point of
for f, g, h being Function of S,T st f = F & g = G & h = H holds
( H = F + G iff for x being Element of S holds h . x = (f . x) + (g . x) )
proof end;

theorem :: C0SP3:45
for a being Real
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for F, G being Point of
for f, g being Function of S,T st f = F & g = G holds
( G = a * F iff for x being Element of S holds g . x = a * (f . x) )
proof end;

theorem Th46: :: C0SP3:46
for a being Real
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for F, G being Point of holds
( ( = 0 implies F = 0. ) & ( F = 0. implies = 0 ) & ||.(a * F).|| = |.a.| * & ||.(F + G).|| <= + )
proof end;

registration
let S be non empty compact TopSpace;
let T be NormedLinearTopSpace;
correctness
coherence ;
by Th46;
end;

theorem Th47: :: C0SP3:47
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for x1, x2 being Point of
for y1, y2 being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st x1 = y1 & x2 = y2 holds
x1 - x2 = y1 - y2
proof end;

theorem :: C0SP3:48
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for F, G, H being Point of
for f, g, h being Function of S,T st f = F & g = G & h = H holds
( H = F - G iff for x being Element of S holds h . x = (f . x) - (g . x) )
proof end;

theorem Th49: :: C0SP3:49
for S being non empty TopSpace
for T being NormedLinearTopSpace
for H being Functional_Sequence of the carrier of S, the carrier of T
for LimH being Function of S,T st H is_unif_conv_on the carrier of S & ( for n being Nat ex Hn being Function of S,T st
( Hn = H . n & Hn is continuous ) ) & LimH = lim (H, the carrier of S) holds
LimH is continuous
proof end;

theorem Th50: :: C0SP3:50
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for Y being Subset of the carrier of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st Y = ContinuousFunctions (S,T) holds
Y is closed
proof end;

theorem Th51: :: C0SP3:51
for S being non empty compact TopSpace
for T being NormedLinearTopSpace st T is complete holds
for seq being sequence of st seq is Cauchy_sequence_by_Norm holds
seq is convergent
proof end;

theorem :: C0SP3:52
for S being non empty compact TopSpace
for T being NormedLinearTopSpace st T is complete holds
R_NormSpace_of_ContinuousFunctions (S,T) is complete
proof end;

definition
let X be ZeroStr ;
let f be the carrier of X -valued Function;
func support f -> set means :Def10: :: C0SP3:def 9
for x being object holds
( x in it iff ( x in dom f & f /. x <> 0. X ) );
existence
ex b1 being set st
for x being object holds
( x in b1 iff ( x in dom f & f /. x <> 0. X ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff ( x in dom f & f /. x <> 0. X ) ) ) & ( for x being object holds
( x in b2 iff ( x in dom f & f /. x <> 0. X ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines support C0SP3:def 9 :
for X being ZeroStr
for f being the carrier of b1 -valued Function
for b3 being set holds
( b3 = support f iff for x being object holds
( x in b3 iff ( x in dom f & f /. x <> 0. X ) ) );

theorem :: C0SP3:53
for X being ZeroStr
for f being the carrier of b1 -valued Function holds support f c= dom f by Def10;

definition
let X be non empty TopSpace;
let T be RealLinearSpace;
let f be Function of X,T;
:: original: support
redefine func support f -> Subset of X;
correctness
coherence
support f is Subset of X
;
proof end;
end;

theorem Th54: :: C0SP3:54
for X being non empty TopSpace
for T being RealLinearSpace
for f, g being Function of X,T holds support (f + g) c= () \/ ()
proof end;

theorem Th55: :: C0SP3:55
for X being non empty TopSpace
for T being RealLinearSpace
for f being Function of X,T
for a being Real holds support (a (#) f) c= support f
proof end;

definition
let X be non empty TopSpace;
let T be NormedLinearTopSpace;
func C_0_Functions (X,T) -> non empty Subset of (RealVectSpace ( the carrier of X,T)) equals :: C0SP3:def 10
{ f where f is Function of the carrier of X, the carrier of T : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & Cl () c= Y ) )
}
;
correctness
coherence
{ f where f is Function of the carrier of X, the carrier of T : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & Cl () c= Y ) )
}
is non empty Subset of (RealVectSpace ( the carrier of X,T))
;
proof end;
end;

:: deftheorem defines C_0_Functions C0SP3:def 10 :
for X being non empty TopSpace
for T being NormedLinearTopSpace holds C_0_Functions (X,T) = { f where f is Function of the carrier of X, the carrier of T : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & Cl () c= Y ) )
}
;

theorem Th56: :: C0SP3:56
for X being non empty TopSpace
for T being NormedLinearTopSpace
for v, u being Element of (RealVectSpace ( the carrier of X,T)) st v in C_0_Functions (X,T) & u in C_0_Functions (X,T) holds
v + u in C_0_Functions (X,T)
proof end;

theorem Th57: :: C0SP3:57
for X being non empty TopSpace
for T being NormedLinearTopSpace
for a being Real
for u being Element of (RealVectSpace ( the carrier of X,T)) st u in C_0_Functions (X,T) holds
a * u in C_0_Functions (X,T)
proof end;

theorem :: C0SP3:58
for X being non empty TopSpace
for T being NormedLinearTopSpace holds C_0_Functions (X,T) is linearly-closed by ;

registration
let X be non empty TopSpace;
let T be NormedLinearTopSpace;
cluster C_0_Functions (X,T) -> non empty linearly-closed ;
correctness
coherence
( not C_0_Functions (X,T) is empty & C_0_Functions (X,T) is linearly-closed )
;
by ;
end;

definition
let X be non empty TopSpace;
let T be NormedLinearTopSpace;
func R_VectorSpace_of_C_0_Functions (X,T) -> RealLinearSpace equals :: C0SP3:def 11
RLSStruct(# (C_0_Functions (X,T)),(Zero_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(Add_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(Mult_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))) #);
correctness
coherence
RLSStruct(# (C_0_Functions (X,T)),(Zero_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(Add_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(Mult_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))) #) is RealLinearSpace
;
end;

:: deftheorem defines R_VectorSpace_of_C_0_Functions C0SP3:def 11 :
for X being non empty TopSpace
for T being NormedLinearTopSpace holds R_VectorSpace_of_C_0_Functions (X,T) = RLSStruct(# (C_0_Functions (X,T)),(Zero_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(Add_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(Mult_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))) #);

theorem :: C0SP3:59
for X being non empty TopSpace
for T being NormedLinearTopSpace holds R_VectorSpace_of_C_0_Functions (X,T) is Subspace of RealVectSpace ( the carrier of X,T) by RSSPACE:11;

theorem Th60: :: C0SP3:60
for X being non empty TopSpace
for T being NormedLinearTopSpace
for x being set st x in C_0_Functions (X,T) holds
x in BoundedFunctions ( the carrier of X,T)
proof end;

definition
let X be non empty TopSpace;
let T be NormedLinearTopSpace;
func C_0_FunctionsNorm (X,T) -> Function of (C_0_Functions (X,T)),REAL equals :: C0SP3:def 12
(BoundedFunctionsNorm ( the carrier of X,T)) | (C_0_Functions (X,T));
correctness
coherence
(BoundedFunctionsNorm ( the carrier of X,T)) | (C_0_Functions (X,T)) is Function of (C_0_Functions (X,T)),REAL
;
proof end;
end;

:: deftheorem defines C_0_FunctionsNorm C0SP3:def 12 :
for X being non empty TopSpace
for T being NormedLinearTopSpace holds C_0_FunctionsNorm (X,T) = (BoundedFunctionsNorm ( the carrier of X,T)) | (C_0_Functions (X,T));

definition
let X be non empty TopSpace;
let T be NormedLinearTopSpace;
func R_Normed_Space_of_C_0_Functions (X,T) -> NORMSTR equals :: C0SP3:def 13
NORMSTR(# (C_0_Functions (X,T)),(Zero_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(Add_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(Mult_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(C_0_FunctionsNorm (X,T)) #);
correctness
coherence
NORMSTR(# (C_0_Functions (X,T)),(Zero_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(Add_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(Mult_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(C_0_FunctionsNorm (X,T)) #) is NORMSTR
;
;
end;

:: deftheorem defines R_Normed_Space_of_C_0_Functions C0SP3:def 13 :
for X being non empty TopSpace
for T being NormedLinearTopSpace holds R_Normed_Space_of_C_0_Functions (X,T) = NORMSTR(# (C_0_Functions (X,T)),(Zero_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(Add_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(Mult_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(C_0_FunctionsNorm (X,T)) #);

registration
let X be non empty TopSpace;
let T be NormedLinearTopSpace;
correctness
coherence
( R_Normed_Space_of_C_0_Functions (X,T) is strict & not R_Normed_Space_of_C_0_Functions (X,T) is empty )
;
;
end;

theorem :: C0SP3:61
for X being non empty TopSpace
for T being NormedLinearTopSpace
for x being set st x in C_0_Functions (X,T) holds
x in ContinuousFunctions (X,T)
proof end;

theorem Th62: :: C0SP3:62
for X being non empty TopSpace
for T being NormedLinearTopSpace holds 0. () = X --> (0. T)
proof end;

theorem Th63: :: C0SP3:63
for X being non empty TopSpace
for T being NormedLinearTopSpace holds 0. () = X --> (0. T)
proof end;

theorem Th64: :: C0SP3:64
for X being non empty TopSpace
for T being NormedLinearTopSpace
for x1, x2 being Point of ()
for y1, y2 being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
proof end;

theorem Th65: :: C0SP3:65
for X being non empty TopSpace
for T being NormedLinearTopSpace
for a being Real
for x being Point of ()
for y being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)) st x = y holds
a * x = a * y
proof end;

theorem Th66: :: C0SP3:66
for a being Real
for X being non empty TopSpace
for T being NormedLinearTopSpace
for F, G being Point of () holds
( ( = 0 implies F = 0. () ) & ( F = 0. () implies = 0 ) & ||.(a * F).|| = |.a.| * & ||.(F + G).|| <= + )
proof end;

theorem :: C0SP3:67
for X being non empty TopSpace
for T being NormedLinearTopSpace holds R_Normed_Space_of_C_0_Functions (X,T) is RealNormSpace-like by Th66;

registration
let X be non empty TopSpace;
let T be NormedLinearTopSpace;
coherence
proof end;
end;

theorem :: C0SP3:68
for X being non empty TopSpace
for T being NormedLinearTopSpace holds R_Normed_Space_of_C_0_Functions (X,T) is RealNormSpace ;