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

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

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

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

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;

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

end;
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 { f where f is Function of the carrier of S, the carrier of T : f is continuous } ;

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;

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

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;

coherence

( not ContinuousFunctions (S,T) is empty & ContinuousFunctions (S,T) is functional )

end;
let T be LinearTopSpace;

coherence

( not ContinuousFunctions (S,T) is empty & ContinuousFunctions (S,T) is functional )

proof end;

theorem Th5: :: C0SP3:5

for S being non empty TopSpace

for T being LinearTopSpace holds ContinuousFunctions (S,T) is linearly-closed

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;

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;

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

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

definition

let S be non empty TopSpace;

let T be LinearTopSpace;

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;
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)))) #);

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 ;

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

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

R_VectorSpace_of_ContinuousFunctions (S,T) is constituted-Functions by MONOID_0:80;

end;
let T be LinearTopSpace;

coherence

R_VectorSpace_of_ContinuousFunctions (S,T) is constituted-Functions by MONOID_0:80;

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

coherence

f . v is VECTOR of T;

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

coherence

f . v is VECTOR of T;

proof 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) )

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) )

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)

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;

coherence

the carrier of (R_VectorSpace_of_ContinuousFunctions (S,T)) is functional ;

end;
let T be LinearTopSpace;

coherence

the carrier of (R_VectorSpace_of_ContinuousFunctions (S,T)) is functional ;

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

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;

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

end;
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 { f where f is Function of the carrier of S, the carrier of T : f is_continuous_on the carrier of S } ;

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;

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

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;

coherence

( not ContinuousFunctions (S,T) is empty & ContinuousFunctions (S,T) is functional )

end;
coherence

( not ContinuousFunctions (S,T) is empty & ContinuousFunctions (S,T) is functional )

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;

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

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

definition

let S, T be RealNormSpace;

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;
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)))) #);

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 ;

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

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

R_VectorSpace_of_ContinuousFunctions (S,T) is constituted-Functions by MONOID_0:80;

end;
coherence

R_VectorSpace_of_ContinuousFunctions (S,T) is constituted-Functions by MONOID_0:80;

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

coherence

f . v is VECTOR of T;

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

coherence

f . v is VECTOR of T;

proof 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) )

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) )

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

ex b_{1} being Function of S,T st

( b_{1} = f & b_{1} is_continuous_on the carrier of S )
by A1;

uniqueness

for b_{1}, b_{2} being Function of S,T st b_{1} = f & b_{1} is_continuous_on the carrier of S & b_{2} = f & b_{2} is_continuous_on the carrier of S holds

b_{1} = b_{2}
;

end;
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 ( it = f & it is_continuous_on the carrier of S );

ex b

( b

uniqueness

for b

b

:: deftheorem defines modetrans C0SP3:def 5 :

for S, T being RealNormSpace

for f being object st f in ContinuousFunctions (S,T) holds

for b_{4} being Function of S,T holds

( b_{4} = modetrans (f,S,T) iff ( b_{4} = f & b_{4} is_continuous_on the carrier of S ) );

for S, T being RealNormSpace

for f being object st f in ContinuousFunctions (S,T) holds

for b

( b

definition

attr c_{1} is strict ;

struct RLNormTopStruct -> RLTopStruct , NORMSTR ;

aggr RLNormTopStruct(# carrier, ZeroF, addF, Mult, topology, normF #) -> RLNormTopStruct ;

end;
struct RLNormTopStruct -> RLTopStruct , NORMSTR ;

aggr RLNormTopStruct(# carrier, ZeroF, addF, Mult, topology, normF #) -> RLNormTopStruct ;

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;

coherence

not RLNormTopStruct(# X,O,F,G,T,N #) is empty ;

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

coherence

not RLNormTopStruct(# X,O,F,G,T,N #) is empty ;

registration
end;

definition

let X be non empty RLNormTopStruct ;

end;
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) );

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

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

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

ex b_{1} being non empty RLNormTopStruct st

( b_{1} is strict & b_{1} is add-continuous & b_{1} is Mult-continuous & b_{1} is TopSpace-like & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital & b_{1} is discerning & b_{1} is reflexive & b_{1} is RealNormSpace-like & b_{1} is norm-generated & b_{1} is T_2 )
end;

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 ex b

( b

proof end;

definition

mode NormedLinearTopSpace is 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 RLNormTopStruct ;

end;
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.|| )

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 )

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 )

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

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 ) )

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

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

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 )

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 )

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 )

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 )

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 ) )

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 ) )

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 )

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

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)

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)

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;

coherence

(BoundedFunctionsNorm ( the carrier of S,T)) | (ContinuousFunctions (S,T)) is Function of (ContinuousFunctions (S,T)),REAL;

end;
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 (BoundedFunctionsNorm ( the carrier of S,T)) | (ContinuousFunctions (S,T));

coherence

(BoundedFunctionsNorm ( the carrier of S,T)) | (ContinuousFunctions (S,T)) is Function of (ContinuousFunctions (S,T)),REAL;

proof 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));

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;

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

;

end;
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 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)) #);

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

;

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

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)))),(ContinuousFunctionsNorm (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;
let T be NormedLinearTopSpace;

correctness

coherence

not R_NormSpace_of_ContinuousFunctions (S,T) is empty ;

;

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;

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.||

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

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

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;

( not R_NormSpace_of_ContinuousFunctions (S,T) is empty & R_NormSpace_of_ContinuousFunctions (S,T) is right_complementable & R_NormSpace_of_ContinuousFunctions (S,T) is Abelian & R_NormSpace_of_ContinuousFunctions (S,T) is add-associative & R_NormSpace_of_ContinuousFunctions (S,T) is right_zeroed & R_NormSpace_of_ContinuousFunctions (S,T) is vector-distributive & R_NormSpace_of_ContinuousFunctions (S,T) is scalar-distributive & R_NormSpace_of_ContinuousFunctions (S,T) is scalar-associative & R_NormSpace_of_ContinuousFunctions (S,T) is scalar-unital )

end;
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 ( not R_NormSpace_of_ContinuousFunctions (S,T) is empty & R_NormSpace_of_ContinuousFunctions (S,T) is right_complementable & R_NormSpace_of_ContinuousFunctions (S,T) is Abelian & R_NormSpace_of_ContinuousFunctions (S,T) is add-associative & R_NormSpace_of_ContinuousFunctions (S,T) is right_zeroed & R_NormSpace_of_ContinuousFunctions (S,T) is vector-distributive & R_NormSpace_of_ContinuousFunctions (S,T) is scalar-distributive & R_NormSpace_of_ContinuousFunctions (S,T) is scalar-associative & R_NormSpace_of_ContinuousFunctions (S,T) is scalar-unital )

proof 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))

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))

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.||

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.||

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) )

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) )

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.|| )

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;

coherence

( R_NormSpace_of_ContinuousFunctions (S,T) is reflexive & R_NormSpace_of_ContinuousFunctions (S,T) is discerning & R_NormSpace_of_ContinuousFunctions (S,T) is RealNormSpace-like );

by Th46;

end;
let T be NormedLinearTopSpace;

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

correctness coherence

( R_NormSpace_of_ContinuousFunctions (S,T) is reflexive & R_NormSpace_of_ContinuousFunctions (S,T) is discerning & R_NormSpace_of_ContinuousFunctions (S,T) is RealNormSpace-like );

by Th46;

theorem Th47: :: C0SP3:47

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

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

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

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

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

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

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;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ( x in dom f & f /. x <> 0. X ) )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff ( x in dom f & f /. x <> 0. X ) ) ) & ( for x being object holds

( x in b_{2} iff ( x in dom f & f /. x <> 0. X ) ) ) holds

b_{1} = b_{2}

end;
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 for x being object holds

( x in it iff ( x in dom f & f /. x <> 0. X ) );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def10 defines support C0SP3:def 9 :

for X being ZeroStr

for f being the carrier of b_{1} -valued Function

for b_{3} being set holds

( b_{3} = support f iff for x being object holds

( x in b_{3} iff ( x in dom f & f /. x <> 0. X ) ) );

for X being ZeroStr

for f being the carrier of b

for b

( b

( x in b

theorem :: C0SP3:53

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;

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

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)

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

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;

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 (support f) c= Y ) ) } is non empty Subset of (RealVectSpace ( the carrier of X,T));

end;
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 { 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 ) ) } ;

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 (support f) c= Y ) ) } is non empty Subset of (RealVectSpace ( the carrier of X,T));

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

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 (support f) 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)

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)

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;

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;

correctness

coherence

( not C_0_Functions (X,T) is empty & C_0_Functions (X,T) is linearly-closed );

by Th56, Th57;

end;
let T be NormedLinearTopSpace;

correctness

coherence

( not C_0_Functions (X,T) is empty & C_0_Functions (X,T) is linearly-closed );

by Th56, Th57;

definition

let X be non empty TopSpace;

let T be NormedLinearTopSpace;

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;

by RSSPACE:11;

end;
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 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)))) #);

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;

by RSSPACE:11;

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

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;

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)

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;

coherence

(BoundedFunctionsNorm ( the carrier of X,T)) | (C_0_Functions (X,T)) is Function of (C_0_Functions (X,T)),REAL;

end;
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 (BoundedFunctionsNorm ( the carrier of X,T)) | (C_0_Functions (X,T));

coherence

(BoundedFunctionsNorm ( the carrier of X,T)) | (C_0_Functions (X,T)) is Function of (C_0_Functions (X,T)),REAL;

proof 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));

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;

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;
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 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)) #);

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 ;

;

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

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

;

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)

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)

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)

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

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

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.|| )

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;

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;

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

end;
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 ( R_Normed_Space_of_C_0_Functions (X,T) is reflexive & R_Normed_Space_of_C_0_Functions (X,T) is discerning & R_Normed_Space_of_C_0_Functions (X,T) is RealNormSpace-like & R_Normed_Space_of_C_0_Functions (X,T) is vector-distributive & R_Normed_Space_of_C_0_Functions (X,T) is scalar-distributive & R_Normed_Space_of_C_0_Functions (X,T) is scalar-associative & R_Normed_Space_of_C_0_Functions (X,T) is scalar-unital & R_Normed_Space_of_C_0_Functions (X,T) is Abelian & R_Normed_Space_of_C_0_Functions (X,T) is add-associative & R_Normed_Space_of_C_0_Functions (X,T) is right_zeroed & R_Normed_Space_of_C_0_Functions (X,T) is right_complementable )

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

for T being NormedLinearTopSpace holds R_Normed_Space_of_C_0_Functions (X,T) is RealNormSpace ;