C0SP3: Functional Space Consisted by Continuous Functions on Topological Space

:: Functional Space Consisted by Continuous Functions on Topological Space
:: by Hiroshi Yamazaki , Keiichi Miyajima and Yasunari Shidama
::
:: Received March 30, 2021
:: 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

proof end;

end;

:: deftheorem defines ContinuousFunctions C0SP3:def 1 :

registration

let S be non empty TopSpace;
let T be LinearTopSpace;

cluster ContinuousFunctions (S,T) -> functional non empty ;

coherence

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 Th5, RSSPACE:11;

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 by Th5, RSSPACE:11;

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 ;

end;

:: deftheorem defines R_VectorSpace_of_ContinuousFunctions C0SP3:def 2 :

registration

let S be non empty TopSpace;
let T be LinearTopSpace;

cluster R_VectorSpace_of_ContinuousFunctions (S,T) -> strict constituted-Functions ;

coherence by MONOID_0:80;

end;

definition

let S be non empty TopSpace;
let T be LinearTopSpace;
let f be VECTOR of (R_VectorSpace_of_ContinuousFunctions (S,T));
let v be Element of S;
:: original: .
redefine func f . v -> VECTOR of T;
correctness

proof end;

end;

theorem Th7: :: C0SP3:7

for S being non empty TopSpace
for T being LinearTopSpace
for f, g, h being VECTOR of (R_VectorSpace_of_ContinuousFunctions (S,T)) 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 (R_VectorSpace_of_ContinuousFunctions (S,T))
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. (R_VectorSpace_of_ContinuousFunctions (S,T)) = the carrier of S --> (0. T)

proof end;

registration

let S be non empty TopSpace;
let T be LinearTopSpace;

cluster the carrier of (R_VectorSpace_of_ContinuousFunctions (S,T)) -> functional ;

coherence ;

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

proof end;

end;

:: deftheorem defines ContinuousFunctions C0SP3:def 3 :

registration

let S, T be RealNormSpace;

cluster ContinuousFunctions (S,T) -> functional non empty ;

coherence

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 Th11, RSSPACE:11;

registration

let S, T be RealNormSpace;

coherence by Th11, RSSPACE:11;

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 ;

end;

:: deftheorem defines R_VectorSpace_of_ContinuousFunctions C0SP3:def 4 :

registration

let S, T be RealNormSpace;

cluster R_VectorSpace_of_ContinuousFunctions (S,T) -> strict constituted-Functions ;

coherence by MONOID_0:80;

end;

definition

let S, T be RealNormSpace;
let f be VECTOR of (R_VectorSpace_of_ContinuousFunctions (S,T));
let v be Element of S;
:: original: .
redefine func f . v -> VECTOR of T;
correctness

proof end;

end;

theorem :: C0SP3:13

for S, T being RealNormSpace
for f, g, h being VECTOR of (R_VectorSpace_of_ContinuousFunctions (S,T)) 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 (R_VectorSpace_of_ContinuousFunctions (S,T))
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 Th11, RSSPACE:11;

theorem :: C0SP3:16

for S, T being RealNormSpace holds 0. (R_VectorSpace_of_ContinuousFunctions (S,T)) = 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 by A1;
uniqueness ;

end;

:: deftheorem defines modetrans C0SP3:def 5 :

definition

attr c₁ is strict ;
struct RLNormTopStruct -> RLTopStruct , NORMSTR ;
aggr RLNormTopStruct(# carrier, ZeroF, addF, Mult, topology, normF #) -> RLNormTopStruct ;

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 ;

end;

registration

cluster non empty strict for RLNormTopStruct ;

existence

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 :

registration

cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like TopSpace-like T_2 add-continuous Mult-continuous strict norm-generated for RLNormTopStruct ;

existence

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 & ||.x.|| = ||.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

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

proof end;

end;

:: deftheorem defines ContinuousFunctionsNorm C0SP3:def 7 :

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)))),(ContinuousFunctionsNorm (S,T)) #);

correctness ;

end;

:: deftheorem defines R_NormSpace_of_ContinuousFunctions C0SP3:def 8 :

registration

let S be non empty compact TopSpace;
let T be NormedLinearTopSpace;

cluster R_NormSpace_of_ContinuousFunctions (S,T) -> non empty strict ;

correctness ;

end;

theorem Th36: :: C0SP3:36

for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for x being Point of (R_NormSpace_of_ContinuousFunctions (S,T))
for y being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st x = y holds
||.x.|| = ||.y.|| by FUNCT_1:49;

theorem :: C0SP3:37

for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for f being Point of (R_NormSpace_of_ContinuousFunctions (S,T))
for g being Function of S,T st f = g holds
for t being Point of S holds ||.(g . t).|| <= ||.f.||

proof end;

theorem Th38: :: C0SP3:38

for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for x1, x2 being Point of (R_NormSpace_of_ContinuousFunctions (S,T))
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 (R_NormSpace_of_ContinuousFunctions (S,T))
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;

cluster R_NormSpace_of_ContinuousFunctions (S,T) -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ;

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. (R_NormSpace_of_ContinuousFunctions (S,T))

proof end;

theorem Th41: :: C0SP3:41

for S being non empty compact TopSpace
for T being NormedLinearTopSpace holds 0. (R_NormSpace_of_ContinuousFunctions (S,T)) = 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 (R_NormSpace_of_ContinuousFunctions (S,T)) holds 0 <= ||.F.||

proof end;

theorem :: C0SP3:43

for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for F being Point of (R_NormSpace_of_ContinuousFunctions (S,T)) st F = 0. (R_NormSpace_of_ContinuousFunctions (S,T)) holds
0 = ||.F.||

proof end;

theorem Th44: :: C0SP3:44

for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for F, G, H being Point of (R_NormSpace_of_ContinuousFunctions (S,T))
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 (R_NormSpace_of_ContinuousFunctions (S,T))
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 (R_NormSpace_of_ContinuousFunctions (S,T)) holds
( ( ||.F.|| = 0 implies F = 0. (R_NormSpace_of_ContinuousFunctions (S,T)) ) & ( F = 0. (R_NormSpace_of_ContinuousFunctions (S,T)) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

proof end;

registration

let S be non empty compact TopSpace;
let T be NormedLinearTopSpace;

cluster R_NormSpace_of_ContinuousFunctions (S,T) -> discerning reflexive strict RealNormSpace-like ;

correctness by Th46;

end;

theorem Th47: :: C0SP3:47

proof end;

theorem :: C0SP3:48

for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for F, G, H being Point of (R_NormSpace_of_ContinuousFunctions (S,T))
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 (R_NormSpace_of_ContinuousFunctions (S,T)) 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines support C0SP3:def 9 :

theorem :: C0SP3:53

for X being ZeroStr
for f being the carrier of b₁ -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

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= (support f) \/ (support g)

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 (support f) c= Y ) ) } ;

correctness

proof end;

end;

:: deftheorem defines C_0_Functions C0SP3:def 10 :

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 Th56, Th57;

registration

let X be non empty TopSpace;
let T be NormedLinearTopSpace;

cluster C_0_Functions (X,T) -> non empty linearly-closed ;

correctness by Th56, Th57;

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 by RSSPACE:11;

end;

:: deftheorem defines R_VectorSpace_of_C_0_Functions C0SP3:def 11 :

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

proof end;

end;

:: deftheorem defines C_0_FunctionsNorm C0SP3:def 12 :

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 ;

end;

:: deftheorem defines R_Normed_Space_of_C_0_Functions C0SP3:def 13 :

registration

let X be non empty TopSpace;
let T be NormedLinearTopSpace;

cluster R_Normed_Space_of_C_0_Functions (X,T) -> non empty strict ;

correctness ;

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. (R_VectorSpace_of_C_0_Functions (X,T)) = X --> (0. T)

proof end;

theorem Th63: :: C0SP3:63

for X being non empty TopSpace
for T being NormedLinearTopSpace holds 0. (R_Normed_Space_of_C_0_Functions (X,T)) = 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 (R_Normed_Space_of_C_0_Functions (X,T))
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 (R_Normed_Space_of_C_0_Functions (X,T))
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 (R_Normed_Space_of_C_0_Functions (X,T)) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions (X,T)) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions (X,T)) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.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;

cluster R_Normed_Space_of_C_0_Functions (X,T) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;

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 ;