:: 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
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, FUNCOP_1, NUMBERS, VALUED_0, PRE_TOPC, ORDINAL2,
SUBSET_1, RCOMP_1, RELAT_1, XBOOLE_0, FUNCT_1, TARSKI, CARD_1, ARYTM_3,
ARYTM_1, COMPLEX1, CONNSP_2, RLVECT_1, ALGSTR_0, FUNCSDOM, REAL_1,
FUNCT_2, VALUED_1, RSSPACE, BINOP_1, SUPINF_2, REALSET1, ZFMISC_1,
RSSPACE4, XXREAL_2, XXREAL_0, NORMSP_1, NORMSP_2, REWRITE1, NAT_1,
MONOID_0, NORMSP_0, FRECHET, RSSPACE3, SEQ_2, TMAP_1, ORDEQ_01, PARTFUN1,
SEQFUNC, C0SP2, LOPBAN_1, METRIC_1, RELAT_2, PRE_POLY, RLSUB_1, RLTOPSP1,
SETFAM_1, FINSET_1, FCONT_1, CFCONT_1, SEQ_4, C0SP3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1,
REALSET1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1,
XXREAL_2, VALUED_0, SEQ_2, SEQ_4, RCOMP_1, SEQFUNC, STRUCT_0, ALGSTR_0,
PRE_POLY, RLVECT_1, RLSUB_1, NORMSP_0, NORMSP_1, NFCONT_1, PRE_TOPC,
TOPS_2, COMPTS_1, FRECHET, FRECHET2, VFUNCT_1, CONNSP_2, RUSUB_4, TMAP_1,
CONVEX1, RLTOPSP1, RSSPACE, RSSPACE3, LOPBAN_1, NORMSP_2, MONOID_0,
RSSPACE4, SEQFUNC2;
constructors REALSET1, RSSPACE3, COMPLEX1, RCOMP_1, C0SP1, FRECHET, FRECHET2,
NFCONT_1, SEQFUNC, MEASURE6, TOPMETR, SEQ_4, COMPTS_1, COMSEQ_2,
NORMSP_2, VFUNCT_1, TMAP_1, RUSUB_4, CONVEX1, TOPS_2, MONOID_0, RSSPACE4,
PRE_POLY, SEQFUNC2;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, XREAL_0, REALSET1,
NUMBERS, ORDINAL1, VALUED_0, PSCOMP_1, XXREAL_0, FUNCT_2, XXREAL_2,
RELSET_1, WAYBEL_2, VFUNCT_1, NORMSP_0, NORMSP_1, NORMSP_2, RLVECT_1,
RLTOPSP1, BORSUK_1, MONOID_0, RSSPACE4;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
begin :: Real Vector Space of Continuous Functions
reserve
S for non empty TopSpace,
T for LinearTopSpace,
X for non empty Subset of the carrier of S;
theorem :: C0SP3:1
for X be non empty TopSpace, S be non empty LinearTopSpace,
f,g be Function of X,S,
x be Point of X
st f is_continuous_at x & g is_continuous_at x
holds f+g is_continuous_at x;
theorem :: C0SP3:2
for X be non empty TopSpace, S be non empty LinearTopSpace,
f be Function of X,S,
x be Point of X,
a be Real
st f is_continuous_at x
holds a(#)f is_continuous_at x;
theorem :: C0SP3:3
for X be non empty TopSpace, S be non empty LinearTopSpace,
f,g be Function of X,S
st f is continuous & g is continuous
holds f+g is continuous;
theorem :: C0SP3:4
for X be non empty TopSpace, S be non empty LinearTopSpace,
f be Function of X,S,
a be Real
st f is continuous
holds a(#)f is continuous;
definition
let S be non empty TopSpace, T be non empty 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 };
end;
registration
let S be non empty TopSpace, T be non empty LinearTopSpace;
cluster ContinuousFunctions(S,T) -> non empty functional;
end;
theorem :: C0SP3:5
for S be non empty TopSpace, T be non empty LinearTopSpace
holds ContinuousFunctions(S,T) is linearly-closed;
theorem :: C0SP3:6
for S be non empty TopSpace, T be non empty 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);
registration
let S be non empty TopSpace, T be non empty 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))
#) -> Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative
scalar-unital;
end;
definition
let S be non empty TopSpace, T be non empty 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))
#);
end;
registration
let S be non empty TopSpace, T be non empty LinearTopSpace;
cluster R_VectorSpace_of_ContinuousFunctions(S,T) -> constituted-Functions;
end;
definition
let S be non empty TopSpace, T be non empty LinearTopSpace,
f be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T);
let v be Element of S;
redefine func f .v -> VECTOR of T;
end;
theorem :: C0SP3:7
for S be non empty TopSpace, T be non empty LinearTopSpace
for f,g,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T)
holds h = f+g iff
for x be Element of S holds h.x = f.x + g.x;
theorem :: C0SP3:8
for S be non empty TopSpace, T be non empty LinearTopSpace
for f,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T)
for a be Real holds h = a*f iff for x be Element of S holds h.x = a * f.x;
theorem :: C0SP3:9
for S be non empty TopSpace, T be non empty LinearTopSpace
holds 0. R_VectorSpace_of_ContinuousFunctions(S,T)
= (the carrier of S) --> 0.T;
registration
let S be non empty TopSpace, T be non empty LinearTopSpace;
cluster the carrier of R_VectorSpace_of_ContinuousFunctions(S,T) ->
functional;
end;
::::::::::::Norm Space version::::::::::::::::::::::::::::
begin :: Real Vector Space of Continuous Functions
reserve
S,T for RealNormSpace,
X for non empty Subset of the carrier of S;
theorem :: C0SP3:10
for x being Point of T holds
(the carrier of S) --> x is_continuous_on the carrier of S;
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 };
end;
registration
let S,T be RealNormSpace;
cluster ContinuousFunctions(S,T) -> non empty functional;
end;
theorem :: C0SP3:11
for S,T be RealNormSpace
holds ContinuousFunctions(S,T) is linearly-closed;
theorem :: C0SP3:12
for S,T be 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);
registration
let S,T be RealNormSpace;
cluster RLSStruct (# ContinuousFunctions(S,T),
Zero_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Add_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T)),
Mult_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))
#) -> Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital;
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))
#);
end;
registration
let S,T be RealNormSpace;
cluster R_VectorSpace_of_ContinuousFunctions(S,T) -> constituted-Functions;
end;
definition
let S,T be RealNormSpace,
f be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T);
let v be Element of S;
redefine func f .v -> VECTOR of T;
end;
theorem :: C0SP3:13
for S,T be RealNormSpace
for f,g,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T)
holds h = f+g iff for x be Element of S holds h.x = f.x + g.x;
theorem :: C0SP3:14
for S,T be RealNormSpace
for f,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T)
for a be Real holds h = a*f iff for x be Element of S holds h.x = a * f.x;
theorem :: C0SP3:15
for S,T be RealNormSpace holds
R_VectorSpace_of_ContinuousFunctions(S,T)
is Subspace of RealVectSpace(the carrier of S,T);
theorem :: C0SP3:16
for S,T be RealNormSpace
holds 0. R_VectorSpace_of_ContinuousFunctions(S,T)
= (the carrier of S) --> 0.T;
definition
let S,T be RealNormSpace;
let f be object such that
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;
end;
begin :: Normed Topological Linear Space
definition
struct(RLTopStruct,NORMSTR) RLNormTopStruct
(# carrier -> set, ZeroF -> Element of the carrier,
addF -> BinOp of the carrier,
Mult -> Function of [:REAL, the carrier:],the carrier,
topology -> Subset-Family of the carrier,
normF -> Function of the carrier,REAL #);
end;
registration
let X be non empty set, O be Element of X,
F be BinOp of X, G be Function of [:REAL,X:],X,
T be Subset-Family of X,
N be Function of X,REAL;
cluster RLNormTopStruct (# X,O,F,G,T,N #) -> non empty;
end;
registration
cluster strict non empty for RLNormTopStruct;
end;
definition
let X be non empty RLNormTopStruct;
attr X is norm-generated means
:: C0SP3:def 6
ex RNS be RealNormSpace
st RNS = the NORMSTR of X
& the topology of X = the topology of TopSpaceNorm RNS;
end;
registration
cluster strict add-continuous Mult-continuous TopSpace-like Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital
discerning reflexive RealNormSpace-like
norm-generated T_2 for non empty RLNormTopStruct;
end;
definition
mode NormedLinearTopSpace is strict add-continuous
Mult-continuous TopSpace-like Abelian add-associative right_zeroed
right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital
discerning reflexive RealNormSpace-like norm-generated
T_2 non empty RLNormTopStruct;
end;
theorem :: C0SP3:17
for X be NormedLinearTopSpace holds X is LinearTopSpace;
theorem :: C0SP3:18
for X be NormedLinearTopSpace holds X is RealNormSpace;
theorem :: C0SP3:19
for X being NormedLinearTopSpace,
RNS being RealNormSpace
st RNS = the NORMSTR of X
for x,y be Point of X,
x1,y1 be Point of RNS,
a be Real
st x1=x & y1=y
holds
x+y = x1+y1
&
a*x = a*x1
&
x-y = x1-y1
&
||.x.|| = ||.x1.||;
theorem :: C0SP3:20
for X being NormedLinearTopSpace,
S being sequence of X,
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;
theorem :: C0SP3:21
for X being NormedLinearTopSpace,
S being sequence of X,
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;
theorem :: C0SP3:22
for X being NormedLinearTopSpace,
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;
theorem :: C0SP3:23
for X being NormedLinearTopSpace,
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;
theorem :: 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;
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;
theorem :: C0SP3:26
for X being NormedLinearTopSpace,
RNS being RealNormSpace,
t being sequence of X,
s being sequence of RNS
st RNS = the NORMSTR of X & t=s
& t is convergent
holds s is convergent & lim s = lim t;
theorem :: C0SP3:27
for X being NormedLinearTopSpace,
RNS being RealNormSpace,
s being sequence of X,
t being sequence of RNS
st RNS = the NORMSTR of X & s=t
holds
s is convergent
iff
t is convergent;
theorem :: C0SP3:28
for X being NormedLinearTopSpace,
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;
theorem :: C0SP3:29
for X being NormedLinearTopSpace,
RNS be RealNormSpace,
V being Subset of X,
W being Subset of RNS st
RNS = the NORMSTR of X
& the topology of X = the topology of (TopSpaceNorm RNS)
& V = W
holds
V is closed iff W is closed;
theorem :: C0SP3:30
for X being NormedLinearTopSpace,
V be Subset of X,
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 ));
theorem :: C0SP3:31
for X being NormedLinearTopSpace,
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;
theorem :: C0SP3:32
for X being NormedLinearTopSpace,
RNS be RealNormSpace,
V being Subset of X,
W being Subset of RNS st
RNS = the NORMSTR of X
& the topology of X = the topology of TopSpaceNorm RNS
& V = W
holds
V is compact iff W is compact;
begin :: Real Norm Space of Continuous Functions
theorem :: 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;
theorem :: C0SP3:34
for S be non empty compact TopSpace,T be NormedLinearTopSpace holds
for x being set st x in ContinuousFunctions(S,T) holds
x in BoundedFunctions (the carrier of S,T);
theorem :: C0SP3:35
for S be non empty compact TopSpace,T be NormedLinearTopSpace holds
(R_VectorSpace_of_ContinuousFunctions(S,T) is
Subspace of R_VectorSpace_of_BoundedFunctions(the carrier of S,T));
definition
let S be non empty compact TopSpace,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));
end;
definition
let S be non empty compact TopSpace,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) #);
end;
registration
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
cluster R_NormSpace_of_ContinuousFunctions(S,T) -> non empty;
end;
theorem :: C0SP3:36
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for x be Point of R_NormSpace_of_ContinuousFunctions(S,T),
y be Point of R_NormSpace_of_BoundedFunctions(the carrier of S,T)
st x=y holds ||.x.||= ||.y.||;
theorem :: C0SP3:37
for S be non empty compact TopSpace,
T be NormedLinearTopSpace,
f be Point of R_NormSpace_of_ContinuousFunctions(S,T),
g be Function of S,T
st f=g holds
for t be Point of S holds ||.g.t.|| <= ||.f.||;
theorem :: C0SP3:38
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for x1,x2 be Point of R_NormSpace_of_ContinuousFunctions(S,T),
y1,y2 be Point of R_NormSpace_of_BoundedFunctions(the carrier of S,T)
st x1=y1 & x2=y2 holds x1+x2=y1+y2;
theorem :: C0SP3:39
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for a be Real,
x be Point of R_NormSpace_of_ContinuousFunctions(S,T),
y be Point of R_NormSpace_of_BoundedFunctions(the carrier of S,T)
st x=y holds a*x=a*y;
registration
let S be non empty compact TopSpace,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;
end;
theorem :: C0SP3:40
for S be non empty compact TopSpace,T be NormedLinearTopSpace holds
(the carrier of S) --> 0.T = 0.R_NormSpace_of_ContinuousFunctions(S,T);
theorem :: C0SP3:41
for S be non empty compact TopSpace,T be NormedLinearTopSpace holds
0.R_NormSpace_of_ContinuousFunctions(S,T)
= 0.R_NormSpace_of_BoundedFunctions(the carrier of S,T);
theorem :: C0SP3:42
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for F be Point of R_NormSpace_of_ContinuousFunctions(S,T)
holds 0 <= ||.F.||;
theorem :: C0SP3:43
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for F be Point of R_NormSpace_of_ContinuousFunctions(S,T) holds
F = 0.R_NormSpace_of_ContinuousFunctions(S,T) implies 0 = ||.F.||;
theorem :: C0SP3:44
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for F,G,H being Point of R_NormSpace_of_ContinuousFunctions(S,T)
for f,g,h be Function of S,T holds
(f=F & g=G & h=H implies
(H = F+G iff for x be Element of S holds h.x = f.x + g.x));
theorem :: C0SP3:45
for a be Real
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for F,G being Point of R_NormSpace_of_ContinuousFunctions(S,T)
for f,g being Function of S,T holds
(f=F & g=G implies ( G = a*F iff for x be Element of S holds g.x = a*f.x ));
theorem :: C0SP3:46
for a being Real
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for F,G being Point of R_NormSpace_of_ContinuousFunctions(S,T) holds
( ||.F.|| = 0 iff F = 0.R_NormSpace_of_ContinuousFunctions(S,T)) &
(||.a*F.|| = |.a.| * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||);
registration
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
cluster R_NormSpace_of_ContinuousFunctions(S,T)
-> reflexive discerning RealNormSpace-like;
end;
theorem :: C0SP3:47
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for x1,x2 be Point of R_NormSpace_of_ContinuousFunctions(S,T),
y1,y2 be Point of R_NormSpace_of_BoundedFunctions(the carrier of S,T)
st x1=y1 & x2=y2 holds x1-x2=y1-y2;
theorem :: C0SP3:48
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for F,G,H be Point of R_NormSpace_of_ContinuousFunctions(S,T)
for f,g,h be Function of S,T holds
f=F & g=G & h=H implies
(H = F-G iff (for x be Element of S holds h.x = f.x - g.x));
theorem :: C0SP3:49
for S be non empty TopSpace,T be NormedLinearTopSpace,
H be Functional_Sequence of the carrier of S,the carrier of T,
LimH be Function of S,T
st H is_unif_conv_on (the carrier of S)
&
( for n be Nat holds
ex Hn be Function of S,T st Hn = H.n & Hn is continuous )
& LimH = lim(H,the carrier of S)
holds LimH is continuous;
theorem :: C0SP3:50
for S be non empty compact TopSpace,T be NormedLinearTopSpace holds
for Y be Subset of the carrier of
R_NormSpace_of_BoundedFunctions(the carrier of S,T) st
Y = ContinuousFunctions(S,T) holds Y is closed;
theorem :: C0SP3:51
for S be non empty compact TopSpace,
T be NormedLinearTopSpace st T is complete holds
for seq be sequence of R_NormSpace_of_ContinuousFunctions(S,T)
st seq is Cauchy_sequence_by_Norm holds seq is convergent;
theorem :: C0SP3:52
for S be non empty compact TopSpace,
T be NormedLinearTopSpace st T is complete holds
R_NormSpace_of_ContinuousFunctions(S,T) is complete;
begin :: Some Properties of Support
definition
let X be ZeroStr;
let f be (the carrier of X)-valued Function;
func support f -> set means
:: C0SP3:def 9
for x being object holds
x in it iff x in dom f & f /. x <> 0.X;
end;
theorem :: C0SP3:53
for X be ZeroStr,
f be (the carrier of X)-valued Function
holds support f c= dom f;
definition
let X be non empty TopSpace, T be RealLinearSpace;
let f be Function of X,T;
redefine func support f -> Subset of X;
end;
theorem :: C0SP3:54
for X be non empty TopSpace, T be RealLinearSpace
for f,g be Function of X,T holds
support(f+g) c= support(f) \/ support(g);
theorem :: C0SP3:55
for X be non empty TopSpace,T be RealLinearSpace,
f be Function of X,T,
a be Real holds
support(a(#)f) c= support(f);
begin :: Space of Real-valued Continuous Functionals with Bounded Support
definition
let X be non empty TopSpace, 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 be non empty Subset of X st Y is compact
& Cl support f c= Y };
end;
theorem :: C0SP3:56
for X be non empty TopSpace,T be NormedLinearTopSpace
for v,u be 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);
theorem :: C0SP3:57
for X be non empty TopSpace,T be NormedLinearTopSpace
for a be Real,u be 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);
theorem :: C0SP3:58
for X be non empty TopSpace,T be NormedLinearTopSpace holds
C_0_Functions(X,T) is linearly-closed;
registration
let X be non empty TopSpace,T be NormedLinearTopSpace;
cluster C_0_Functions(X,T) -> non empty linearly-closed;
end;
definition
let X be non empty TopSpace,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)) #);
end;
theorem :: C0SP3:59
for X be non empty TopSpace,T be NormedLinearTopSpace holds
R_VectorSpace_of_C_0_Functions(X,T)
is Subspace of RealVectSpace(the carrier of X,T);
theorem :: C0SP3:60
for X be non empty TopSpace,T be NormedLinearTopSpace
for x being set st x in C_0_Functions(X,T) holds
x in BoundedFunctions(the carrier of X,T);
definition
let X be non empty TopSpace, 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));
end;
definition
let X be non empty TopSpace,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) #);
end;
registration
let X be non empty TopSpace,T be NormedLinearTopSpace;
cluster R_Normed_Space_of_C_0_Functions (X,T) -> strict non empty;
end;
theorem :: C0SP3:61
for X be non empty TopSpace, T be NormedLinearTopSpace
for x being set st x in C_0_Functions(X,T) holds
x in ContinuousFunctions(X,T);
theorem :: C0SP3:62
for X be non empty TopSpace, T be NormedLinearTopSpace holds
0.R_VectorSpace_of_C_0_Functions(X,T) = X -->0.T;
theorem :: C0SP3:63
for X be non empty TopSpace,T be NormedLinearTopSpace holds
0.R_Normed_Space_of_C_0_Functions (X,T) = X --> 0.T;
theorem :: C0SP3:64
for X be non empty TopSpace,T be NormedLinearTopSpace
for x1,x2 be Point of R_Normed_Space_of_C_0_Functions (X,T),
y1,y2 be Point of R_NormSpace_of_BoundedFunctions(the carrier of X,T)
st x1=y1 & x2=y2 holds x1+x2=y1+y2;
theorem :: C0SP3:65
for X be non empty TopSpace,T be NormedLinearTopSpace
for a be Real,x be Point of R_Normed_Space_of_C_0_Functions (X,T),
y be Point of R_NormSpace_of_BoundedFunctions(the carrier of X,T)
st x=y holds a*x=a*y;
theorem :: C0SP3:66
for a be Real
for X be non empty TopSpace,T be NormedLinearTopSpace
for F,G be Point of R_Normed_Space_of_C_0_Functions (X,T) holds
(||.F.|| = 0 iff F = 0.R_Normed_Space_of_C_0_Functions (X,T) ) &
||.a*F.|| = |.a.| * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||;
theorem :: C0SP3:67
for X be non empty TopSpace,T be NormedLinearTopSpace holds
R_Normed_Space_of_C_0_Functions (X,T) is RealNormSpace-like;
registration
let X be non empty TopSpace,T be NormedLinearTopSpace;
cluster R_Normed_Space_of_C_0_Functions (X,T) ->
reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
end;
theorem :: C0SP3:68
for X be non empty TopSpace,T be NormedLinearTopSpace holds
R_Normed_Space_of_C_0_Functions (X,T) is RealNormSpace;