:: RSSPACE4 semantic presentation
begin
Lm1: for rseq being Real_Sequence
for K being real number st ( for n being Element of NAT holds rseq . n <= K ) holds
upper_bound (rng rseq) <= K
proof
let rseq be Real_Sequence; ::_thesis: for K being real number st ( for n being Element of NAT holds rseq . n <= K ) holds
upper_bound (rng rseq) <= K
let K be real number ; ::_thesis: ( ( for n being Element of NAT holds rseq . n <= K ) implies upper_bound (rng rseq) <= K )
assume A1: for n being Element of NAT holds rseq . n <= K ; ::_thesis: upper_bound (rng rseq) <= K
now__::_thesis:_for_s_being_real_number_st_s_in_rng_rseq_holds_
s_<=_K
let s be real number ; ::_thesis: ( s in rng rseq implies s <= K )
assume s in rng rseq ; ::_thesis: s <= K
then ex n being set st
( n in NAT & rseq . n = s ) by FUNCT_2:11;
hence s <= K by A1; ::_thesis: verum
end;
hence upper_bound (rng rseq) <= K by SEQ_4:45; ::_thesis: verum
end;
Lm2: for rseq being Real_Sequence st rseq is bounded holds
for n being Element of NAT holds rseq . n <= upper_bound (rng rseq)
proof
let rseq be Real_Sequence; ::_thesis: ( rseq is bounded implies for n being Element of NAT holds rseq . n <= upper_bound (rng rseq) )
assume rseq is bounded ; ::_thesis: for n being Element of NAT holds rseq . n <= upper_bound (rng rseq)
then rng rseq is real-bounded by MEASURE6:39;
then A1: rng rseq is bounded_above by XXREAL_2:def_11;
let n be Element of NAT ; ::_thesis: rseq . n <= upper_bound (rng rseq)
NAT = dom rseq by FUNCT_2:def_1;
then rseq . n in rng rseq by FUNCT_1:3;
hence rseq . n <= upper_bound (rng rseq) by A1, SEQ_4:def_1; ::_thesis: verum
end;
definition
func the_set_of_BoundedRealSequences -> Subset of Linear_Space_of_RealSequences means :Def1: :: RSSPACE4:def 1
for x being set holds
( x in it iff ( x in the_set_of_RealSequences & seq_id x is bounded ) );
existence
ex b1 being Subset of Linear_Space_of_RealSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) )
proof
defpred S1[ set ] means seq_id $1 is bounded ;
consider IT being set such that
A1: for x being set holds
( x in IT iff ( x in the_set_of_RealSequences & S1[x] ) ) from XBOOLE_0:sch_1();
for x being set st x in IT holds
x in the_set_of_RealSequences by A1;
then IT is Subset of the_set_of_RealSequences by TARSKI:def_3;
hence ex b1 being Subset of Linear_Space_of_RealSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) ) by A1, RSSPACE:def_7; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of Linear_Space_of_RealSequences st ( for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) ) ) & ( for x being set holds
( x in b2 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) ) ) holds
b1 = b2
proof
let X1, X2 be Subset of Linear_Space_of_RealSequences; ::_thesis: ( ( for x being set holds
( x in X1 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) ) ) & ( for x being set holds
( x in X2 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) ) ) implies X1 = X2 )
assume that
A2: for x being set holds
( x in X1 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) ) and
A3: for x being set holds
( x in X2 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) ) ; ::_thesis: X1 = X2
thus X1 c= X2 :: according to XBOOLE_0:def_10 ::_thesis: X2 c= X1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X1 or x in X2 )
assume x in X1 ; ::_thesis: x in X2
then ( x in the_set_of_RealSequences & seq_id x is bounded ) by A2;
hence x in X2 by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X2 or x in X1 )
assume x in X2 ; ::_thesis: x in X1
then ( x in the_set_of_RealSequences & seq_id x is bounded ) by A3;
hence x in X1 by A2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines the_set_of_BoundedRealSequences RSSPACE4:def_1_:_
for b1 being Subset of Linear_Space_of_RealSequences holds
( b1 = the_set_of_BoundedRealSequences iff for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & seq_id x is bounded ) ) );
registration
cluster the_set_of_BoundedRealSequences -> non empty ;
coherence
not the_set_of_BoundedRealSequences is empty
proof
seq_id Zeroseq is bounded
proof
reconsider rseq = seq_id Zeroseq as Real_Sequence ;
for n being Nat holds rseq . n = 0
proof
let n be Nat; ::_thesis: rseq . n = 0
n in NAT by ORDINAL1:def_12;
hence rseq . n = 0 by RSSPACE:def_6; ::_thesis: verum
end;
then rseq is constant by VALUED_0:def_18;
hence seq_id Zeroseq is bounded ; ::_thesis: verum
end;
hence not the_set_of_BoundedRealSequences is empty by Def1; ::_thesis: verum
end;
cluster the_set_of_BoundedRealSequences -> linearly-closed ;
coherence
the_set_of_BoundedRealSequences is linearly-closed
proof
set W = the_set_of_BoundedRealSequences ;
A1: for a being Real
for v being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_BoundedRealSequences holds
a * v in the_set_of_BoundedRealSequences
proof
let a be Real; ::_thesis: for v being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_BoundedRealSequences holds
a * v in the_set_of_BoundedRealSequences
let v be VECTOR of Linear_Space_of_RealSequences; ::_thesis: ( v in the_set_of_BoundedRealSequences implies a * v in the_set_of_BoundedRealSequences )
assume v in the_set_of_BoundedRealSequences ; ::_thesis: a * v in the_set_of_BoundedRealSequences
then A2: seq_id v is bounded by Def1;
seq_id (a * v) = seq_id (a (#) (seq_id v)) by RSSPACE:3, RSSPACE:def_7
.= a (#) (seq_id v) by RSSPACE:1 ;
then seq_id (a * v) is bounded by A2, SEQM_3:37;
hence a * v in the_set_of_BoundedRealSequences by Def1, RSSPACE:def_7; ::_thesis: verum
end;
for v, u being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_BoundedRealSequences & u in the_set_of_BoundedRealSequences holds
v + u in the_set_of_BoundedRealSequences
proof
let v, u be VECTOR of Linear_Space_of_RealSequences; ::_thesis: ( v in the_set_of_BoundedRealSequences & u in the_set_of_BoundedRealSequences implies v + u in the_set_of_BoundedRealSequences )
assume ( v in the_set_of_BoundedRealSequences & u in the_set_of_BoundedRealSequences ) ; ::_thesis: v + u in the_set_of_BoundedRealSequences
then A3: ( seq_id v is bounded & seq_id u is bounded ) by Def1;
seq_id (v + u) = seq_id ((seq_id v) + (seq_id u)) by RSSPACE:2, RSSPACE:def_7
.= (seq_id v) + (seq_id u) by RSSPACE:1 ;
hence v + u in the_set_of_BoundedRealSequences by A3, Def1, RSSPACE:def_7; ::_thesis: verum
end;
hence the_set_of_BoundedRealSequences is linearly-closed by A1, RLSUB_1:def_1; ::_thesis: verum
end;
end;
Lm3: RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is Subspace of Linear_Space_of_RealSequences
by RSSPACE:11;
registration
cluster RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is Abelian & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is add-associative & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is right_zeroed & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is right_complementable & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is vector-distributive & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-distributive & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-associative & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-unital ) by RSSPACE:11;
end;
Lm4: ( RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is Abelian & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is add-associative & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is right_zeroed & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is right_complementable & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is vector-distributive & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-distributive & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-associative & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-unital )
;
definition
func linfty_norm -> Function of the_set_of_BoundedRealSequences,REAL means :Def2: :: RSSPACE4:def 2
for x being set st x in the_set_of_BoundedRealSequences holds
it . x = upper_bound (rng (abs (seq_id x)));
existence
ex b1 being Function of the_set_of_BoundedRealSequences,REAL st
for x being set st x in the_set_of_BoundedRealSequences holds
b1 . x = upper_bound (rng (abs (seq_id x)))
proof
deffunc H1( set ) -> Element of REAL = upper_bound (rng (abs (seq_id $1)));
A1: for z being set st z in the_set_of_BoundedRealSequences holds
H1(z) in REAL ;
ex f being Function of the_set_of_BoundedRealSequences,REAL st
for x being set st x in the_set_of_BoundedRealSequences holds
f . x = H1(x) from FUNCT_2:sch_2(A1);
hence ex b1 being Function of the_set_of_BoundedRealSequences,REAL st
for x being set st x in the_set_of_BoundedRealSequences holds
b1 . x = upper_bound (rng (abs (seq_id x))) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of the_set_of_BoundedRealSequences,REAL st ( for x being set st x in the_set_of_BoundedRealSequences holds
b1 . x = upper_bound (rng (abs (seq_id x))) ) & ( for x being set st x in the_set_of_BoundedRealSequences holds
b2 . x = upper_bound (rng (abs (seq_id x))) ) holds
b1 = b2
proof
let NORM1, NORM2 be Function of the_set_of_BoundedRealSequences,REAL; ::_thesis: ( ( for x being set st x in the_set_of_BoundedRealSequences holds
NORM1 . x = upper_bound (rng (abs (seq_id x))) ) & ( for x being set st x in the_set_of_BoundedRealSequences holds
NORM2 . x = upper_bound (rng (abs (seq_id x))) ) implies NORM1 = NORM2 )
assume that
A2: for x being set st x in the_set_of_BoundedRealSequences holds
NORM1 . x = upper_bound (rng (abs (seq_id x))) and
A3: for x being set st x in the_set_of_BoundedRealSequences holds
NORM2 . x = upper_bound (rng (abs (seq_id x))) ; ::_thesis: NORM1 = NORM2
A4: for z being set st z in the_set_of_BoundedRealSequences holds
NORM1 . z = NORM2 . z
proof
let z be set ; ::_thesis: ( z in the_set_of_BoundedRealSequences implies NORM1 . z = NORM2 . z )
assume A5: z in the_set_of_BoundedRealSequences ; ::_thesis: NORM1 . z = NORM2 . z
NORM1 . z = upper_bound (rng (abs (seq_id z))) by A2, A5;
hence NORM1 . z = NORM2 . z by A3, A5; ::_thesis: verum
end;
( dom NORM1 = the_set_of_BoundedRealSequences & dom NORM2 = the_set_of_BoundedRealSequences ) by FUNCT_2:def_1;
hence NORM1 = NORM2 by A4, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines linfty_norm RSSPACE4:def_2_:_
for b1 being Function of the_set_of_BoundedRealSequences,REAL holds
( b1 = linfty_norm iff for x being set st x in the_set_of_BoundedRealSequences holds
b1 . x = upper_bound (rng (abs (seq_id x))) );
Lm5: for rseq being Real_Sequence st ( for n being Nat holds rseq . n = 0 ) holds
( rseq is bounded & upper_bound (rng (abs rseq)) = 0 )
proof
let rseq be Real_Sequence; ::_thesis: ( ( for n being Nat holds rseq . n = 0 ) implies ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 ) )
assume A1: for n being Nat holds rseq . n = 0 ; ::_thesis: ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 )
A2: for n being Nat holds (abs rseq) . n = 0
proof
let n be Nat; ::_thesis: (abs rseq) . n = 0
n in NAT by ORDINAL1:def_12;
then A3: (abs rseq) . n = abs (rseq . n) by SEQ_1:12;
rseq . n = 0 by A1;
hence (abs rseq) . n = 0 by A3, ABSVALUE:2; ::_thesis: verum
end;
rng (abs rseq) c= {0}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (abs rseq) or y in {0} )
assume y in rng (abs rseq) ; ::_thesis: y in {0}
then ex n being set st
( n in NAT & (abs rseq) . n = y ) by FUNCT_2:11;
then y = 0 by A2;
hence y in {0} by TARSKI:def_1; ::_thesis: verum
end;
then A4: rng (abs rseq) = {0} by ZFMISC_1:33;
rseq is constant by A1, VALUED_0:def_18;
hence ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 ) by A4, SEQ_4:9; ::_thesis: verum
end;
Lm6: for rseq being Real_Sequence st rseq is bounded & upper_bound (rng (abs rseq)) = 0 holds
for n being Nat holds rseq . n = 0
proof
let rseq be Real_Sequence; ::_thesis: ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 implies for n being Nat holds rseq . n = 0 )
assume A1: ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 ) ; ::_thesis: for n being Nat holds rseq . n = 0
let n be Nat; ::_thesis: rseq . n = 0
A2: n in NAT by ORDINAL1:def_12;
0 <= abs (rseq . n) by COMPLEX1:46;
then 0 <= (abs rseq) . n by A2, SEQ_1:12;
then (abs rseq) . n = 0 by A1, A2, Lm2;
then abs (rseq . n) = 0 by A2, SEQ_1:12;
hence rseq . n = 0 by ABSVALUE:2; ::_thesis: verum
end;
theorem :: RSSPACE4:1
for rseq being Real_Sequence holds
( ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 ) iff for n being Nat holds rseq . n = 0 ) by Lm5, Lm6;
registration
cluster NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is Abelian & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is add-associative & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is right_zeroed & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is right_complementable & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is vector-distributive & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is scalar-distributive & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is scalar-associative & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is scalar-unital ) by Lm4, RSSPACE3:2;
end;
definition
func linfty_Space -> non empty NORMSTR equals :: RSSPACE4:def 3
NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #);
coherence
NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is non empty NORMSTR ;
end;
:: deftheorem defines linfty_Space RSSPACE4:def_3_:_
linfty_Space = NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #);
theorem Th2: :: RSSPACE4:2
( the carrier of linfty_Space = the_set_of_BoundedRealSequences & ( for x being set holds
( x is VECTOR of linfty_Space iff ( x is Real_Sequence & seq_id x is bounded ) ) ) & 0. linfty_Space = Zeroseq & ( for u being VECTOR of linfty_Space holds u = seq_id u ) & ( for u, v being VECTOR of linfty_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of linfty_Space holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of linfty_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of linfty_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of linfty_Space holds seq_id v is bounded ) & ( for v being VECTOR of linfty_Space holds ||.v.|| = upper_bound (rng (abs (seq_id v))) ) )
proof
set l1 = linfty_Space ;
A1: 0. linfty_Space = 0. Linear_Space_of_RealSequences by RSSPACE:def_10
.= Zeroseq by RSSPACE:def_7 ;
A2: for x being set holds
( x is Element of linfty_Space iff ( x is Real_Sequence & seq_id x is bounded ) )
proof
let x be set ; ::_thesis: ( x is Element of linfty_Space iff ( x is Real_Sequence & seq_id x is bounded ) )
( x in the_set_of_RealSequences iff x is Real_Sequence ) by RSSPACE:def_1;
hence ( x is Element of linfty_Space iff ( x is Real_Sequence & seq_id x is bounded ) ) by Def1; ::_thesis: verum
end;
A3: for u, v being VECTOR of linfty_Space holds u + v = (seq_id u) + (seq_id v)
proof
let u, v be VECTOR of linfty_Space; ::_thesis: u + v = (seq_id u) + (seq_id v)
reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_RealSequences by Lm3, RLSUB_1:10;
set L1 = Linear_Space_of_RealSequences ;
set W = the_set_of_BoundedRealSequences ;
dom the addF of Linear_Space_of_RealSequences = [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def_1;
then A4: dom ( the addF of Linear_Space_of_RealSequences || the_set_of_BoundedRealSequences) = [:the_set_of_BoundedRealSequences,the_set_of_BoundedRealSequences:] by RELAT_1:62;
u + v = ( the addF of Linear_Space_of_RealSequences || the_set_of_BoundedRealSequences) . [u,v] by RSSPACE:def_8
.= u1 + v1 by A4, FUNCT_1:47 ;
hence u + v = (seq_id u) + (seq_id v) by RSSPACE:2, RSSPACE:def_7; ::_thesis: verum
end;
A5: for r being Real
for u being VECTOR of linfty_Space holds r * u = r (#) (seq_id u)
proof
let r be Real; ::_thesis: for u being VECTOR of linfty_Space holds r * u = r (#) (seq_id u)
let u be VECTOR of linfty_Space; ::_thesis: r * u = r (#) (seq_id u)
reconsider u1 = u as VECTOR of Linear_Space_of_RealSequences by Lm3, RLSUB_1:10;
set L1 = Linear_Space_of_RealSequences ;
set W = the_set_of_BoundedRealSequences ;
dom the Mult of Linear_Space_of_RealSequences = [:REAL, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def_1;
then A6: dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_BoundedRealSequences:]) = [:REAL,the_set_of_BoundedRealSequences:] by RELAT_1:62, ZFMISC_1:96;
r * u = ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_BoundedRealSequences:]) . [r,u] by RSSPACE:def_9
.= r * u1 by A6, FUNCT_1:47 ;
hence r * u = r (#) (seq_id u) by RSSPACE:3, RSSPACE:def_7; ::_thesis: verum
end;
A7: for u being VECTOR of linfty_Space holds u = seq_id u
proof
let u be VECTOR of linfty_Space; ::_thesis: u = seq_id u
u is VECTOR of Linear_Space_of_RealSequences by Lm3, RLSUB_1:10;
hence u = seq_id u by RSSPACE:def_2, RSSPACE:def_7; ::_thesis: verum
end;
A8: for u being VECTOR of linfty_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
proof
let u be VECTOR of linfty_Space; ::_thesis: ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
- u = (- 1) * u by RLVECT_1:16
.= - (seq_id u) by A5 ;
hence ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) by A7; ::_thesis: verum
end;
for u, v being VECTOR of linfty_Space holds u - v = (seq_id u) - (seq_id v)
proof
let u, v be VECTOR of linfty_Space; ::_thesis: u - v = (seq_id u) - (seq_id v)
thus u - v = (seq_id u) + (seq_id (- v)) by A3
.= (seq_id u) - (seq_id v) by A8 ; ::_thesis: verum
end;
hence ( the carrier of linfty_Space = the_set_of_BoundedRealSequences & ( for x being set holds
( x is VECTOR of linfty_Space iff ( x is Real_Sequence & seq_id x is bounded ) ) ) & 0. linfty_Space = Zeroseq & ( for u being VECTOR of linfty_Space holds u = seq_id u ) & ( for u, v being VECTOR of linfty_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of linfty_Space holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of linfty_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of linfty_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of linfty_Space holds seq_id v is bounded ) & ( for v being VECTOR of linfty_Space holds ||.v.|| = upper_bound (rng (abs (seq_id v))) ) ) by A2, A7, A3, A5, A8, A1, Def2; ::_thesis: verum
end;
theorem Th3: :: RSSPACE4:3
for x, y being Point of linfty_Space
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. linfty_Space ) & ( x = 0. linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
proof
let x, y be Point of linfty_Space; ::_thesis: for a being Real holds
( ( ||.x.|| = 0 implies x = 0. linfty_Space ) & ( x = 0. linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
let a be Real; ::_thesis: ( ( ||.x.|| = 0 implies x = 0. linfty_Space ) & ( x = 0. linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
A1: for n being Element of NAT holds (abs (a (#) (seq_id x))) . n = (abs a) * ((abs (seq_id x)) . n)
proof
let n be Element of NAT ; ::_thesis: (abs (a (#) (seq_id x))) . n = (abs a) * ((abs (seq_id x)) . n)
(abs (a (#) (seq_id x))) . n = abs ((a (#) (seq_id x)) . n) by SEQ_1:12
.= abs (a * ((seq_id x) . n)) by SEQ_1:9
.= (abs a) * (abs ((seq_id x) . n)) by COMPLEX1:65
.= (abs a) * ((abs (seq_id x)) . n) by SEQ_1:12 ;
hence (abs (a (#) (seq_id x))) . n = (abs a) * ((abs (seq_id x)) . n) ; ::_thesis: verum
end;
(abs (seq_id x)) . 1 = abs ((seq_id x) . 1) by SEQ_1:12;
then A2: 0 <= (abs (seq_id x)) . 1 by COMPLEX1:46;
A3: for n being Element of NAT holds (abs (seq_id (x + y))) . n = abs (((seq_id x) . n) + ((seq_id y) . n))
proof
let n be Element of NAT ; ::_thesis: (abs (seq_id (x + y))) . n = abs (((seq_id x) . n) + ((seq_id y) . n))
(abs (seq_id (x + y))) . n = (abs (seq_id ((seq_id x) + (seq_id y)))) . n by Th2
.= (abs ((seq_id x) + (seq_id y))) . n by RSSPACE:1
.= abs (((seq_id x) + (seq_id y)) . n) by SEQ_1:12
.= abs (((seq_id x) . n) + ((seq_id y) . n)) by SEQ_1:7 ;
hence (abs (seq_id (x + y))) . n = abs (((seq_id x) . n) + ((seq_id y) . n)) ; ::_thesis: verum
end;
A4: for n being Element of NAT holds (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n)
proof
let n be Element of NAT ; ::_thesis: (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n)
abs (((seq_id x) . n) + ((seq_id y) . n)) <= (abs ((seq_id x) . n)) + (abs ((seq_id y) . n)) by COMPLEX1:56;
then (abs (seq_id (x + y))) . n <= (abs ((seq_id x) . n)) + (abs ((seq_id y) . n)) by A3;
then (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + (abs ((seq_id y) . n)) by SEQ_1:12;
hence (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n) by SEQ_1:12; ::_thesis: verum
end;
A5: for n being Element of NAT holds (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n
proof
let n be Element of NAT ; ::_thesis: (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n
((abs (seq_id x)) . n) + ((abs (seq_id y)) . n) = ((abs (seq_id x)) + (abs (seq_id y))) . n by SEQ_1:7;
hence (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n by A4; ::_thesis: verum
end;
A6: now__::_thesis:_(_x_=_0._linfty_Space_implies_||.x.||_=_0_)
assume A7: x = 0. linfty_Space ; ::_thesis: ||.x.|| = 0
A8: for n being Nat holds (seq_id x) . n = 0
proof
let n be Nat; ::_thesis: (seq_id x) . n = 0
n in NAT by ORDINAL1:def_12;
hence (seq_id x) . n = 0 by A7, Th2, RSSPACE:def_6; ::_thesis: verum
end;
thus ||.x.|| = upper_bound (rng (abs (seq_id x))) by Th2
.= 0 by A8, Lm5 ; ::_thesis: verum
end;
seq_id x is bounded by Def1;
then A9: 0 <= upper_bound (rng (abs (seq_id x))) by A2, Lm2;
seq_id x is bounded by Def1;
then rng (abs (seq_id x)) is real-bounded by MEASURE6:39;
then A10: rng (abs (seq_id x)) is bounded_above by XXREAL_2:def_11;
A11: now__::_thesis:_(_||.x.||_=_0_implies_x_=_0._linfty_Space_)
A12: x in the_set_of_RealSequences by Def1;
assume A13: ||.x.|| = 0 ; ::_thesis: x = 0. linfty_Space
( ||.x.|| = upper_bound (rng (abs (seq_id x))) & seq_id x is bounded ) by Th2;
then for n being Element of NAT holds 0 = (seq_id x) . n by A13, Lm6;
hence x = 0. linfty_Space by A12, Th2, RSSPACE:def_6; ::_thesis: verum
end;
A14: seq_id y is bounded by Def1;
A15: seq_id x is bounded by Def1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(seq_id_(x_+_y)))_._n_<=_(upper_bound_(rng_(abs_(seq_id_x))))_+_(upper_bound_(rng_(abs_(seq_id_y))))
let n be Element of NAT ; ::_thesis: (abs (seq_id (x + y))) . n <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y))))
A16: (abs (seq_id y)) . n <= upper_bound (rng (abs (seq_id y))) by A14, Lm2;
( ((abs (seq_id x)) + (abs (seq_id y))) . n = ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n) & (abs (seq_id x)) . n <= upper_bound (rng (abs (seq_id x))) ) by A15, Lm2, SEQ_1:7;
then A17: ((abs (seq_id x)) + (abs (seq_id y))) . n <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y)))) by A16, XREAL_1:7;
(abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n by A5;
hence (abs (seq_id (x + y))) . n <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y)))) by A17, XXREAL_0:2; ::_thesis: verum
end;
then A18: upper_bound (rng (abs (seq_id (x + y)))) <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y)))) by Lm1;
A19: ( ||.y.|| = upper_bound (rng (abs (seq_id y))) & upper_bound (rng (abs (seq_id (x + y)))) = ||.(x + y).|| ) by Th2;
||.(a * x).|| = upper_bound (rng (abs (seq_id (a * x)))) by Th2
.= upper_bound (rng (abs (seq_id (a (#) (seq_id x))))) by Th2
.= upper_bound (rng (abs (a (#) (seq_id x)))) by RSSPACE:1
.= upper_bound (rng ((abs a) (#) (abs (seq_id x)))) by A1, SEQ_1:9
.= upper_bound ((abs a) ** (rng (abs (seq_id x)))) by INTEGRA2:17
.= (abs a) * (upper_bound (rng (abs (seq_id x)))) by A10, COMPLEX1:46, INTEGRA2:13
.= (abs a) * ||.x.|| by Th2 ;
hence ( ( ||.x.|| = 0 implies x = 0. linfty_Space ) & ( x = 0. linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| ) by A11, A6, A9, A19, A18, Th2; ::_thesis: verum
end;
registration
cluster linfty_Space -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;
coherence
( linfty_Space is reflexive & linfty_Space is discerning & linfty_Space is RealNormSpace-like & linfty_Space is vector-distributive & linfty_Space is scalar-distributive & linfty_Space is scalar-associative & linfty_Space is scalar-unital & linfty_Space is Abelian & linfty_Space is add-associative & linfty_Space is right_zeroed & linfty_Space is right_complementable )
proof
thus ||.(0. linfty_Space).|| = 0 by Th3; :: according to NORMSP_0:def_6 ::_thesis: ( linfty_Space is discerning & linfty_Space is RealNormSpace-like & linfty_Space is vector-distributive & linfty_Space is scalar-distributive & linfty_Space is scalar-associative & linfty_Space is scalar-unital & linfty_Space is Abelian & linfty_Space is add-associative & linfty_Space is right_zeroed & linfty_Space is right_complementable )
thus ( linfty_Space is discerning & linfty_Space is RealNormSpace-like & linfty_Space is vector-distributive & linfty_Space is scalar-distributive & linfty_Space is scalar-associative & linfty_Space is scalar-unital & linfty_Space is Abelian & linfty_Space is add-associative & linfty_Space is right_zeroed & linfty_Space is right_complementable ) by Th3, NORMSP_0:def_5, NORMSP_1:def_1; ::_thesis: verum
end;
end;
theorem :: RSSPACE4:4
for vseq being sequence of linfty_Space st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent
proof
let vseq be sequence of linfty_Space; ::_thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A1: vseq is Cauchy_sequence_by_Norm ; ::_thesis: vseq is convergent
defpred S1[ set , set ] means ex i being Element of NAT st
( $1 = i & ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & $2 = lim rseqi ) );
A2: for x being set st x in NAT holds
ex y being set st
( y in REAL & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in REAL & S1[x,y] ) )
assume x in NAT ; ::_thesis: ex y being set st
( y in REAL & S1[x,y] )
then reconsider i = x as Element of NAT ;
deffunc H1( Nat) -> Element of REAL = (seq_id (vseq . $1)) . i;
consider rseqi being Real_Sequence such that
A3: for n being Element of NAT holds rseqi . n = H1(n) from SEQ_1:sch_1();
take lim rseqi ; ::_thesis: ( lim rseqi in REAL & S1[x, lim rseqi] )
now__::_thesis:_for_e_being_real_number_st_e_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_((rseqi_._m)_-_(rseqi_._k))_<_e
let e be real number ; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e )
assume A4: e > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e
thus ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e ::_thesis: verum
proof
e is Real by XREAL_0:def_1;
then consider k being Element of NAT such that
A5: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A4, RSSPACE3:8;
take k ; ::_thesis: for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e
let m be Element of NAT ; ::_thesis: ( k <= m implies abs ((rseqi . m) - (rseqi . k)) < e )
assume A6: k <= m ; ::_thesis: abs ((rseqi . m) - (rseqi . k)) < e
seq_id ((vseq . m) - (vseq . k)) is bounded by Def1;
then A7: (abs (seq_id ((vseq . m) - (vseq . k)))) . i <= upper_bound (rng (abs (seq_id ((vseq . m) - (vseq . k))))) by Lm2;
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th2
.= (seq_id (vseq . m)) + (- (seq_id (vseq . k))) by RSSPACE:1 ;
then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by SEQ_1:7
.= ((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i)) by SEQ_1:10
.= ((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i)
.= (rseqi . m) - ((seq_id (vseq . k)) . i) by A3
.= (rseqi . m) - (rseqi . k) by A3 ;
then A8: abs ((rseqi . m) - (rseqi . k)) = (abs (seq_id ((vseq . m) - (vseq . k)))) . i by SEQ_1:12;
||.((vseq . m) - (vseq . k)).|| = upper_bound (rng (abs (seq_id ((vseq . m) - (vseq . k))))) by Th2;
then upper_bound (rng (abs (seq_id ((vseq . m) - (vseq . k))))) < e by A5, A6;
hence abs ((rseqi . m) - (rseqi . k)) < e by A7, A8, XXREAL_0:2; ::_thesis: verum
end;
end;
then rseqi is convergent by SEQ_4:41;
hence ( lim rseqi in REAL & S1[x, lim rseqi] ) by A3; ::_thesis: verum
end;
consider f being Function of NAT,REAL such that
A9: for x being set st x in NAT holds
S1[x,f . x] from FUNCT_2:sch_1(A2);
reconsider tseq = f as Real_Sequence ;
A10: now__::_thesis:_for_i_being_Element_of_NAT_ex_rseqi_being_Real_Sequence_st_
(_(_for_n_being_Element_of_NAT_holds_rseqi_._n_=_(seq_id_(vseq_._n))_._i_)_&_rseqi_is_convergent_&_tseq_._i_=_lim_rseqi_)
let i be Element of NAT ; ::_thesis: ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi )
reconsider x = i as set ;
ex i0 being Element of NAT st
( x = i0 & ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i0 ) & rseqi is convergent & f . x = lim rseqi ) ) by A9;
hence ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi ) ; ::_thesis: verum
end;
A11: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e )
proof
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e ) )
assume A12: e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e )
consider k being Element of NAT such that
A13: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A12, RSSPACE3:8;
A14: for m, n being Element of NAT st n >= k & m >= k holds
( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & upper_bound (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e )
proof
let m, n be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & upper_bound (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e ) )
assume ( n >= k & m >= k ) ; ::_thesis: ( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & upper_bound (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e )
then A15: ||.((vseq . n) - (vseq . m)).|| < e by A13;
seq_id ((vseq . n) - (vseq . m)) is bounded by Def1;
hence ( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & upper_bound (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e ) by A15, Def2; ::_thesis: verum
end;
A16: for n, i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i )
proof
let n be Element of NAT ; ::_thesis: for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i )
A17: for m, k being Element of NAT holds seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))
proof
let m, k be Element of NAT ; ::_thesis: seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th2;
hence seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) by RSSPACE:1; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_NAT_
for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_(abs_(seq_id_((vseq_._m)_-_(vseq_._n))))_._i_)_holds_
(_rseq_is_convergent_&_lim_rseq_=_(abs_((seq_id_tseq)_-_(seq_id_(vseq_._n))))_._i_)
let i be Element of NAT ; ::_thesis: for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i )
consider rseqi being Real_Sequence such that
A18: for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i and
A19: ( rseqi is convergent & tseq . i = lim rseqi ) by A10;
now__::_thesis:_for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_(abs_(seq_id_((vseq_._m)_-_(vseq_._n))))_._i_)_holds_
(_rseq_is_convergent_&_lim_rseq_=_(abs_((seq_id_tseq)_-_(seq_id_(vseq_._n))))_._i_)
let rseq be Real_Sequence; ::_thesis: ( ( for m being Element of NAT holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) implies ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) )
assume A20: for m being Element of NAT holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ; ::_thesis: ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i )
A21: now__::_thesis:_for_m_being_Element_of_NAT_holds_rseq_._m_=_abs_((rseqi_._m)_-_((seq_id_(vseq_._n))_._i))
let m be Element of NAT ; ::_thesis: rseq . m = abs ((rseqi . m) - ((seq_id (vseq . n)) . i))
A22: seq_id ((vseq . m) - (vseq . n)) = (seq_id (vseq . m)) - (seq_id (vseq . n)) by A17;
thus rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i by A20
.= abs ((seq_id ((vseq . m) - (vseq . n))) . i) by SEQ_1:12
.= abs (((seq_id (vseq . m)) . i) - ((seq_id (vseq . n)) . i)) by A22, RFUNCT_2:1
.= abs ((rseqi . m) - ((seq_id (vseq . n)) . i)) by A18 ; ::_thesis: verum
end;
abs ((tseq . i) - ((seq_id (vseq . n)) . i)) = abs ((tseq - (seq_id (vseq . n))) . i) by RFUNCT_2:1
.= abs (((seq_id tseq) - (seq_id (vseq . n))) . i) by RSSPACE:1
.= (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i by SEQ_1:12 ;
hence ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) by A19, A21, RSSPACE3:1; ::_thesis: verum
end;
hence for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) ; ::_thesis: verum
end;
hence for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) ; ::_thesis: verum
end;
for n being Element of NAT st n >= k holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e )
proof
let n be Element of NAT ; ::_thesis: ( n >= k implies ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e ) )
assume A23: n >= k ; ::_thesis: ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e )
A24: for i being Element of NAT holds (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i <= e
proof
let i be Element of NAT ; ::_thesis: (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i <= e
deffunc H1( Element of NAT ) -> Element of REAL = (abs (seq_id ((vseq . $1) - (vseq . n)))) . i;
consider rseq being Real_Sequence such that
A25: for m being Element of NAT holds rseq . m = H1(m) from SEQ_1:sch_1();
A26: for m being Element of NAT st m >= k holds
rseq . m <= e
proof
let m be Element of NAT ; ::_thesis: ( m >= k implies rseq . m <= e )
A27: rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i by A25;
assume A28: m >= k ; ::_thesis: rseq . m <= e
then abs (seq_id ((vseq . m) - (vseq . n))) is bounded by A14, A23;
then A29: (abs (seq_id ((vseq . m) - (vseq . n)))) . i <= upper_bound (rng (abs (seq_id ((vseq . m) - (vseq . n))))) by Lm2;
upper_bound (rng (abs (seq_id ((vseq . m) - (vseq . n))))) <= e by A14, A23, A28;
hence rseq . m <= e by A29, A27, XXREAL_0:2; ::_thesis: verum
end;
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) by A16, A25;
hence (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i <= e by A26, RSSPACE2:5; ::_thesis: verum
end;
A30: 0 + e < 1 + e by XREAL_1:8;
now__::_thesis:_for_i_being_Element_of_NAT_holds_abs_(((seq_id_tseq)_-_(seq_id_(vseq_._n)))_._i)_<_e_+_1
let i be Element of NAT ; ::_thesis: abs (((seq_id tseq) - (seq_id (vseq . n))) . i) < e + 1
( (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i <= e & (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i = abs (((seq_id tseq) - (seq_id (vseq . n))) . i) ) by A24, SEQ_1:12;
hence abs (((seq_id tseq) - (seq_id (vseq . n))) . i) < e + 1 by A30, XXREAL_0:2; ::_thesis: verum
end;
then (seq_id tseq) - (seq_id (vseq . n)) is bounded by A12, SEQ_2:3;
hence ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e ) by A24, Lm1; ::_thesis: verum
end;
hence ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e ) ; ::_thesis: verum
end;
A31: seq_id tseq is bounded
proof
consider m being Element of NAT such that
A32: for n being Element of NAT st n >= m holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= 1 ) by A11;
A33: abs ((seq_id tseq) - (seq_id (vseq . m))) is bounded by A32;
set d = abs (seq_id tseq);
set b = abs (seq_id (vseq . m));
set a = abs ((seq_id tseq) - (seq_id (vseq . m)));
A34: seq_id (vseq . m) is bounded by Def1;
A35: for i being Element of NAT holds (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i
proof
let i be Element of NAT ; ::_thesis: (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i
A36: ( (abs (seq_id (vseq . m))) . i = abs ((seq_id (vseq . m)) . i) & (abs (seq_id tseq)) . i = abs ((seq_id tseq) . i) ) by SEQ_1:12;
(abs ((seq_id tseq) - (seq_id (vseq . m)))) . i = abs (((seq_id tseq) + (- (seq_id (vseq . m)))) . i) by SEQ_1:12
.= abs (((seq_id tseq) . i) + ((- (seq_id (vseq . m))) . i)) by SEQ_1:7
.= abs (((seq_id tseq) . i) + (- ((seq_id (vseq . m)) . i))) by SEQ_1:10
.= abs (((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)) ;
then ((abs (seq_id tseq)) . i) - ((abs (seq_id (vseq . m))) . i) <= (abs ((seq_id tseq) - (seq_id (vseq . m)))) . i by A36, COMPLEX1:59;
then (((abs (seq_id tseq)) . i) - ((abs (seq_id (vseq . m))) . i)) + ((abs (seq_id (vseq . m))) . i) <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) . i) + ((abs (seq_id (vseq . m))) . i) by XREAL_1:6;
hence (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i by SEQ_1:7; ::_thesis: verum
end;
abs (seq_id tseq) is bounded
proof
reconsider r = (upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))))) + 1 as real number ;
(abs (seq_id (vseq . m))) . 1 = abs ((seq_id (vseq . m)) . 1) by SEQ_1:12;
then A37: 0 <= (abs (seq_id (vseq . m))) . 1 by COMPLEX1:46;
A38: (upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))))) + 0 < (upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))))) + 1 by XREAL_1:8;
A39: now__::_thesis:_for_i_being_Element_of_NAT_holds_abs_((seq_id_tseq)_._i)_<_r
let i be Element of NAT ; ::_thesis: abs ((seq_id tseq) . i) < r
( (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i & ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i <= upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m))))) ) by A33, A34, A35, Lm2;
then A40: (abs (seq_id tseq)) . i <= upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m))))) by XXREAL_0:2;
(abs (seq_id tseq)) . i = abs ((seq_id tseq) . i) by SEQ_1:12;
hence abs ((seq_id tseq) . i) < r by A38, A40, XXREAL_0:2; ::_thesis: verum
end;
(abs ((seq_id tseq) - (seq_id (vseq . m)))) . 1 = abs (((seq_id tseq) - (seq_id (vseq . m))) . 1) by SEQ_1:12;
then ( ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . 1 = ((abs ((seq_id tseq) - (seq_id (vseq . m)))) . 1) + ((abs (seq_id (vseq . m))) . 1) & 0 <= (abs ((seq_id tseq) - (seq_id (vseq . m)))) . 1 ) by COMPLEX1:46, SEQ_1:7;
then 0 <= upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m))))) by A33, A34, A37, Lm2;
then seq_id tseq is bounded by A39, SEQ_2:3;
hence abs (seq_id tseq) is bounded ; ::_thesis: verum
end;
hence seq_id tseq is bounded by SEQM_3:37; ::_thesis: verum
end;
A41: tseq in the_set_of_RealSequences by RSSPACE:def_1;
then reconsider tv = tseq as Point of linfty_Space by A31, Def1;
take tv ; :: according to NORMSP_1:def_6 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= ||.((vseq . b3) - tv).|| ) )
let e1 be Real; ::_thesis: ( e1 <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not e1 <= ||.((vseq . b2) - tv).|| ) )
assume A42: e1 > 0 ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not e1 <= ||.((vseq . b2) - tv).|| )
set e = e1 / 2;
consider m being Element of NAT such that
A43: for n being Element of NAT st n >= m holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e1 / 2 ) by A11, A42, XREAL_1:215;
A44: e1 / 2 < e1 by A42, XREAL_1:216;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_
||.((vseq_._n)_-_tv).||_<_e1
reconsider u = tseq as VECTOR of linfty_Space by A31, A41, Def1;
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e1 )
assume n >= m ; ::_thesis: ||.((vseq . n) - tv).|| < e1
then A45: upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e1 / 2 by A43;
reconsider v = vseq . n as VECTOR of linfty_Space ;
seq_id (u - v) = u - v by Th2;
then upper_bound (rng (abs (seq_id (u - v)))) = upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) by Th2;
then A46: the normF of linfty_Space . (u - v) <= e1 / 2 by A45, Def2;
||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:33
.= ||.(tv - (vseq . n)).|| by NORMSP_1:2 ;
hence ||.((vseq . n) - tv).|| < e1 by A44, A46, XXREAL_0:2; ::_thesis: verum
end;
hence ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not e1 <= ||.((vseq . b2) - tv).|| ) ; ::_thesis: verum
end;
begin
definition
let X be non empty set ;
let Y be RealNormSpace;
let IT be Function of X, the carrier of Y;
attrIT is bounded means :Def4: :: RSSPACE4:def 4
ex K being Real st
( 0 <= K & ( for x being Element of X holds ||.(IT . x).|| <= K ) );
end;
:: deftheorem Def4 defines bounded RSSPACE4:def_4_:_
for X being non empty set
for Y being RealNormSpace
for IT being Function of X, the carrier of Y holds
( IT is bounded iff ex K being Real st
( 0 <= K & ( for x being Element of X holds ||.(IT . x).|| <= K ) ) );
theorem Th5: :: RSSPACE4:5
for X being non empty set
for Y being RealNormSpace
for f being Function of X, the carrier of Y st ( for x being Element of X holds f . x = 0. Y ) holds
f is bounded
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace
for f being Function of X, the carrier of Y st ( for x being Element of X holds f . x = 0. Y ) holds
f is bounded
let Y be RealNormSpace; ::_thesis: for f being Function of X, the carrier of Y st ( for x being Element of X holds f . x = 0. Y ) holds
f is bounded
let f be Function of X, the carrier of Y; ::_thesis: ( ( for x being Element of X holds f . x = 0. Y ) implies f is bounded )
assume A1: for x being Element of X holds f . x = 0. Y ; ::_thesis: f is bounded
A2: now__::_thesis:_for_x_being_Element_of_X_holds_||.(f_._x).||_=_0
let x be Element of X; ::_thesis: ||.(f . x).|| = 0
thus ||.(f . x).|| = ||.(0. Y).|| by A1
.= 0 ; ::_thesis: verum
end;
take 0 ; :: according to RSSPACE4:def_4 ::_thesis: ( 0 <= 0 & ( for x being Element of X holds ||.(f . x).|| <= 0 ) )
thus ( 0 <= 0 & ( for x being Element of X holds ||.(f . x).|| <= 0 ) ) by A2; ::_thesis: verum
end;
registration
let X be non empty set ;
let Y be RealNormSpace;
cluster non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total bounded for Element of bool [:X, the carrier of Y:];
existence
ex b1 being Function of X, the carrier of Y st b1 is bounded
proof
set f = X --> (0. Y);
reconsider f = X --> (0. Y) as Function of X, the carrier of Y ;
take f ; ::_thesis: f is bounded
for x being Element of X holds f . x = 0. Y by FUNCOP_1:7;
hence f is bounded by Th5; ::_thesis: verum
end;
end;
definition
let X be non empty set ;
let Y be RealNormSpace;
func BoundedFunctions (X,Y) -> Subset of (RealVectSpace (X,Y)) means :Def5: :: RSSPACE4:def 5
for x being set holds
( x in it iff x is bounded Function of X, the carrier of Y );
existence
ex b1 being Subset of (RealVectSpace (X,Y)) st
for x being set holds
( x in b1 iff x is bounded Function of X, the carrier of Y )
proof
A1: RealVectSpace (X,Y) = RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) by LOPBAN_1:def_4;
defpred S1[ set ] means $1 is bounded Function of X, the carrier of Y;
consider IT being set such that
A2: for x being set holds
( x in IT iff ( x in Funcs (X, the carrier of Y) & S1[x] ) ) from XBOOLE_0:sch_1();
take IT ; ::_thesis: ( IT is Subset of (RealVectSpace (X,Y)) & ( for x being set holds
( x in IT iff x is bounded Function of X, the carrier of Y ) ) )
for x being set st x in IT holds
x in Funcs (X, the carrier of Y) by A2;
hence IT is Subset of (RealVectSpace (X,Y)) by A1, TARSKI:def_3; ::_thesis: for x being set holds
( x in IT iff x is bounded Function of X, the carrier of Y )
let x be set ; ::_thesis: ( x in IT iff x is bounded Function of X, the carrier of Y )
thus ( x in IT implies x is bounded Function of X, the carrier of Y ) by A2; ::_thesis: ( x is bounded Function of X, the carrier of Y implies x in IT )
assume A3: x is bounded Function of X, the carrier of Y ; ::_thesis: x in IT
then x in Funcs (X, the carrier of Y) by FUNCT_2:8;
hence x in IT by A2, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of (RealVectSpace (X,Y)) st ( for x being set holds
( x in b1 iff x is bounded Function of X, the carrier of Y ) ) & ( for x being set holds
( x in b2 iff x is bounded Function of X, the carrier of Y ) ) holds
b1 = b2
proof
let X1, X2 be Subset of (RealVectSpace (X,Y)); ::_thesis: ( ( for x being set holds
( x in X1 iff x is bounded Function of X, the carrier of Y ) ) & ( for x being set holds
( x in X2 iff x is bounded Function of X, the carrier of Y ) ) implies X1 = X2 )
assume that
A4: for x being set holds
( x in X1 iff x is bounded Function of X, the carrier of Y ) and
A5: for x being set holds
( x in X2 iff x is bounded Function of X, the carrier of Y ) ; ::_thesis: X1 = X2
for x being set st x in X2 holds
x in X1
proof
let x be set ; ::_thesis: ( x in X2 implies x in X1 )
assume x in X2 ; ::_thesis: x in X1
then x is bounded Function of X, the carrier of Y by A5;
hence x in X1 by A4; ::_thesis: verum
end;
then A6: X2 c= X1 by TARSKI:def_3;
for x being set st x in X1 holds
x in X2
proof
let x be set ; ::_thesis: ( x in X1 implies x in X2 )
assume x in X1 ; ::_thesis: x in X2
then x is bounded Function of X, the carrier of Y by A4;
hence x in X2 by A5; ::_thesis: verum
end;
then X1 c= X2 by TARSKI:def_3;
hence X1 = X2 by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines BoundedFunctions RSSPACE4:def_5_:_
for X being non empty set
for Y being RealNormSpace
for b3 being Subset of (RealVectSpace (X,Y)) holds
( b3 = BoundedFunctions (X,Y) iff for x being set holds
( x in b3 iff x is bounded Function of X, the carrier of Y ) );
registration
let X be non empty set ;
let Y be RealNormSpace;
cluster BoundedFunctions (X,Y) -> non empty ;
coherence
not BoundedFunctions (X,Y) is empty
proof
set f = X --> (0. Y);
reconsider f = X --> (0. Y) as Function of X, the carrier of Y ;
for x being Element of X holds f . x = 0. Y by FUNCOP_1:7;
then f is bounded by Th5;
hence not BoundedFunctions (X,Y) is empty by Def5; ::_thesis: verum
end;
end;
theorem Th6: :: RSSPACE4:6
for X being non empty set
for Y being RealNormSpace holds BoundedFunctions (X,Y) is linearly-closed
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace holds BoundedFunctions (X,Y) is linearly-closed
let Y be RealNormSpace; ::_thesis: BoundedFunctions (X,Y) is linearly-closed
set W = BoundedFunctions (X,Y);
A1: RealVectSpace (X,Y) = RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) by LOPBAN_1:def_4;
A2: for v, u being VECTOR of (RealVectSpace (X,Y)) st v in BoundedFunctions (X,Y) & u in BoundedFunctions (X,Y) holds
v + u in BoundedFunctions (X,Y)
proof
let v, u be VECTOR of (RealVectSpace (X,Y)); ::_thesis: ( v in BoundedFunctions (X,Y) & u in BoundedFunctions (X,Y) implies v + u in BoundedFunctions (X,Y) )
assume that
A3: v in BoundedFunctions (X,Y) and
A4: u in BoundedFunctions (X,Y) ; ::_thesis: v + u in BoundedFunctions (X,Y)
reconsider f = v + u as Function of X, the carrier of Y by A1, FUNCT_2:66;
f is bounded
proof
reconsider v1 = v as bounded Function of X, the carrier of Y by A3, Def5;
consider K2 being Real such that
A5: 0 <= K2 and
A6: for x being Element of X holds ||.(v1 . x).|| <= K2 by Def4;
reconsider u1 = u as bounded Function of X, the carrier of Y by A4, Def5;
consider K1 being Real such that
A7: 0 <= K1 and
A8: for x being Element of X holds ||.(u1 . x).|| <= K1 by Def4;
take K3 = K1 + K2; :: according to RSSPACE4:def_4 ::_thesis: ( 0 <= K3 & ( for x being Element of X holds ||.(f . x).|| <= K3 ) )
now__::_thesis:_for_x_being_Element_of_X_holds_||.(f_._x).||_<=_K3
let x be Element of X; ::_thesis: ||.(f . x).|| <= K3
( ||.(u1 . x).|| <= K1 & ||.(v1 . x).|| <= K2 ) by A8, A6;
then A9: ||.(u1 . x).|| + ||.(v1 . x).|| <= K1 + K2 by XREAL_1:7;
( ||.(f . x).|| = ||.((v1 . x) + (u1 . x)).|| & ||.((u1 . x) + (v1 . x)).|| <= ||.(u1 . x).|| + ||.(v1 . x).|| ) by LOPBAN_1:11, NORMSP_1:def_1;
hence ||.(f . x).|| <= K3 by A9, XXREAL_0:2; ::_thesis: verum
end;
hence ( 0 <= K3 & ( for x being Element of X holds ||.(f . x).|| <= K3 ) ) by A7, A5; ::_thesis: verum
end;
hence v + u in BoundedFunctions (X,Y) by Def5; ::_thesis: verum
end;
for a being Real
for v being VECTOR of (RealVectSpace (X,Y)) st v in BoundedFunctions (X,Y) holds
a * v in BoundedFunctions (X,Y)
proof
let a be Real; ::_thesis: for v being VECTOR of (RealVectSpace (X,Y)) st v in BoundedFunctions (X,Y) holds
a * v in BoundedFunctions (X,Y)
let v be VECTOR of (RealVectSpace (X,Y)); ::_thesis: ( v in BoundedFunctions (X,Y) implies a * v in BoundedFunctions (X,Y) )
assume A10: v in BoundedFunctions (X,Y) ; ::_thesis: a * v in BoundedFunctions (X,Y)
reconsider f = a * v as Function of X, the carrier of Y by A1, FUNCT_2:66;
f is bounded
proof
reconsider v1 = v as bounded Function of X, the carrier of Y by A10, Def5;
consider K being Real such that
A11: 0 <= K and
A12: for x being Element of X holds ||.(v1 . x).|| <= K by Def4;
take (abs a) * K ; :: according to RSSPACE4:def_4 ::_thesis: ( 0 <= (abs a) * K & ( for x being Element of X holds ||.(f . x).|| <= (abs a) * K ) )
A13: now__::_thesis:_for_x_being_Element_of_X_holds_||.(f_._x).||_<=_(abs_a)_*_K
let x be Element of X; ::_thesis: ||.(f . x).|| <= (abs a) * K
A14: 0 <= abs a by COMPLEX1:46;
( ||.(f . x).|| = ||.(a * (v1 . x)).|| & ||.(a * (v1 . x)).|| = (abs a) * ||.(v1 . x).|| ) by LOPBAN_1:12, NORMSP_1:def_1;
hence ||.(f . x).|| <= (abs a) * K by A12, A14, XREAL_1:64; ::_thesis: verum
end;
0 <= abs a by COMPLEX1:46;
hence ( 0 <= (abs a) * K & ( for x being Element of X holds ||.(f . x).|| <= (abs a) * K ) ) by A11, A13; ::_thesis: verum
end;
hence a * v in BoundedFunctions (X,Y) by Def5; ::_thesis: verum
end;
hence BoundedFunctions (X,Y) is linearly-closed by A2, RLSUB_1:def_1; ::_thesis: verum
end;
theorem :: RSSPACE4:7
for X being non empty set
for Y being RealNormSpace holds RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is Subspace of RealVectSpace (X,Y) by Th6, RSSPACE:11;
registration
let X be non empty set ;
let Y be RealNormSpace;
cluster RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is Abelian & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is add-associative & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is right_zeroed & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is right_complementable & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is vector-distributive & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is scalar-distributive & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is scalar-associative & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is scalar-unital ) by Th6, RSSPACE:11;
end;
definition
let X be non empty set ;
let Y be RealNormSpace;
func R_VectorSpace_of_BoundedFunctions (X,Y) -> RealLinearSpace equals :: RSSPACE4:def 6
RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #);
coherence
RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is RealLinearSpace ;
end;
:: deftheorem defines R_VectorSpace_of_BoundedFunctions RSSPACE4:def_6_:_
for X being non empty set
for Y being RealNormSpace holds R_VectorSpace_of_BoundedFunctions (X,Y) = RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #);
registration
let X be non empty set ;
let Y be RealNormSpace;
cluster R_VectorSpace_of_BoundedFunctions (X,Y) -> strict ;
coherence
R_VectorSpace_of_BoundedFunctions (X,Y) is strict ;
end;
theorem Th8: :: RSSPACE4:8
for X being non empty set
for Y being RealNormSpace
for f, g, h being VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace
for f, g, h being VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
let Y be RealNormSpace; ::_thesis: for f, g, h being VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
let f, g, h be VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)); ::_thesis: for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
A1: R_VectorSpace_of_BoundedFunctions (X,Y) is Subspace of RealVectSpace (X,Y) by Th6, RSSPACE:11;
then reconsider f1 = f as VECTOR of (RealVectSpace (X,Y)) by RLSUB_1:10;
reconsider h1 = h as VECTOR of (RealVectSpace (X,Y)) by A1, RLSUB_1:10;
reconsider g1 = g as VECTOR of (RealVectSpace (X,Y)) by A1, RLSUB_1:10;
let f9, g9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & g9 = g & h9 = h implies ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) )
assume A2: ( f9 = f & g9 = g & h9 = h ) ; ::_thesis: ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
A3: now__::_thesis:_(_h_=_f_+_g_implies_for_x_being_Element_of_X_holds_h9_._x_=_(f9_._x)_+_(g9_._x)_)
assume A4: h = f + g ; ::_thesis: for x being Element of X holds h9 . x = (f9 . x) + (g9 . x)
let x be Element of X; ::_thesis: h9 . x = (f9 . x) + (g9 . x)
h1 = f1 + g1 by A1, A4, RLSUB_1:13;
hence h9 . x = (f9 . x) + (g9 . x) by A2, LOPBAN_1:11; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h9_._x_=_(f9_._x)_+_(g9_._x)_)_implies_h_=_f_+_g_)
assume for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ; ::_thesis: h = f + g
then h1 = f1 + g1 by A2, LOPBAN_1:11;
hence h = f + g by A1, RLSUB_1:13; ::_thesis: verum
end;
hence ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) by A3; ::_thesis: verum
end;
theorem Th9: :: RSSPACE4:9
for X being non empty set
for Y being RealNormSpace
for f, h being VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for a being Real holds
( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) )
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace
for f, h being VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for a being Real holds
( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) )
let Y be RealNormSpace; ::_thesis: for f, h being VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for a being Real holds
( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) )
let f, h be VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)); ::_thesis: for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for a being Real holds
( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) )
let f9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & h9 = h implies for a being Real holds
( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) ) )
assume A1: ( f9 = f & h9 = h ) ; ::_thesis: for a being Real holds
( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) )
let a be Real; ::_thesis: ( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) )
A2: R_VectorSpace_of_BoundedFunctions (X,Y) is Subspace of RealVectSpace (X,Y) by Th6, RSSPACE:11;
then reconsider f1 = f, h1 = h as VECTOR of (RealVectSpace (X,Y)) by RLSUB_1:10;
A3: now__::_thesis:_(_h_=_a_*_f_implies_for_x_being_Element_of_X_holds_h9_._x_=_a_*_(f9_._x)_)
assume A4: h = a * f ; ::_thesis: for x being Element of X holds h9 . x = a * (f9 . x)
let x be Element of X; ::_thesis: h9 . x = a * (f9 . x)
h1 = a * f1 by A2, A4, RLSUB_1:14;
hence h9 . x = a * (f9 . x) by A1, LOPBAN_1:12; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h9_._x_=_a_*_(f9_._x)_)_implies_h_=_a_*_f_)
assume for x being Element of X holds h9 . x = a * (f9 . x) ; ::_thesis: h = a * f
then h1 = a * f1 by A1, LOPBAN_1:12;
hence h = a * f by A2, RLSUB_1:14; ::_thesis: verum
end;
hence ( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) ) by A3; ::_thesis: verum
end;
theorem Th10: :: RSSPACE4:10
for X being non empty set
for Y being RealNormSpace holds 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y)
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace holds 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y)
let Y be RealNormSpace; ::_thesis: 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y)
( R_VectorSpace_of_BoundedFunctions (X,Y) is Subspace of RealVectSpace (X,Y) & 0. (RealVectSpace (X,Y)) = X --> (0. Y) ) by Th6, LOPBAN_1:13, RSSPACE:11;
hence 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y) by RLSUB_1:11; ::_thesis: verum
end;
definition
let X be non empty set ;
let Y be RealNormSpace;
let f be set ;
assume A1: f in BoundedFunctions (X,Y) ;
func modetrans (f,X,Y) -> bounded Function of X, the carrier of Y equals :Def7: :: RSSPACE4:def 7
f;
coherence
f is bounded Function of X, the carrier of Y by A1, Def5;
end;
:: deftheorem Def7 defines modetrans RSSPACE4:def_7_:_
for X being non empty set
for Y being RealNormSpace
for f being set st f in BoundedFunctions (X,Y) holds
modetrans (f,X,Y) = f;
definition
let X be non empty set ;
let Y be RealNormSpace;
let u be Function of X, the carrier of Y;
func PreNorms u -> non empty Subset of REAL equals :: RSSPACE4:def 8
{ ||.(u . t).|| where t is Element of X : verum } ;
coherence
{ ||.(u . t).|| where t is Element of X : verum } is non empty Subset of REAL
proof
set x = the Element of X;
A1: now__::_thesis:_for_x_being_set_st_x_in__{__||.(u_._t).||_where_t_is_Element_of_X_:_verum__}__holds_
x_in_REAL
let x be set ; ::_thesis: ( x in { ||.(u . t).|| where t is Element of X : verum } implies x in REAL )
now__::_thesis:_(_x_in__{__||.(u_._t).||_where_t_is_Element_of_X_:_verum__}__implies_x_in_REAL_)
assume x in { ||.(u . t).|| where t is Element of X : verum } ; ::_thesis: x in REAL
then ex t being Element of X st x = ||.(u . t).|| ;
hence x in REAL ; ::_thesis: verum
end;
hence ( x in { ||.(u . t).|| where t is Element of X : verum } implies x in REAL ) ; ::_thesis: verum
end;
||.(u . the Element of X).|| in { ||.(u . t).|| where t is Element of X : verum } ;
hence { ||.(u . t).|| where t is Element of X : verum } is non empty Subset of REAL by A1, TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines PreNorms RSSPACE4:def_8_:_
for X being non empty set
for Y being RealNormSpace
for u being Function of X, the carrier of Y holds PreNorms u = { ||.(u . t).|| where t is Element of X : verum } ;
theorem Th11: :: RSSPACE4:11
for X being non empty set
for Y being RealNormSpace
for g being bounded Function of X, the carrier of Y holds PreNorms g is bounded_above
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace
for g being bounded Function of X, the carrier of Y holds PreNorms g is bounded_above
let Y be RealNormSpace; ::_thesis: for g being bounded Function of X, the carrier of Y holds PreNorms g is bounded_above
let g be bounded Function of X, the carrier of Y; ::_thesis: PreNorms g is bounded_above
consider K being Real such that
0 <= K and
A1: for x being Element of X holds ||.(g . x).|| <= K by Def4;
take K ; :: according to XXREAL_2:def_10 ::_thesis: K is UpperBound of PreNorms g
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in PreNorms g or r <= K )
assume r in PreNorms g ; ::_thesis: r <= K
then ex t being Element of X st r = ||.(g . t).|| ;
hence r <= K by A1; ::_thesis: verum
end;
theorem :: RSSPACE4:12
for X being non empty set
for Y being RealNormSpace
for g being Function of X, the carrier of Y holds
( g is bounded iff PreNorms g is bounded_above )
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace
for g being Function of X, the carrier of Y holds
( g is bounded iff PreNorms g is bounded_above )
let Y be RealNormSpace; ::_thesis: for g being Function of X, the carrier of Y holds
( g is bounded iff PreNorms g is bounded_above )
let g be Function of X, the carrier of Y; ::_thesis: ( g is bounded iff PreNorms g is bounded_above )
now__::_thesis:_(_PreNorms_g_is_bounded_above_implies_ex_K_being_Real_st_g_is_bounded_)
reconsider K = upper_bound (PreNorms g) as Real ;
assume A1: PreNorms g is bounded_above ; ::_thesis: ex K being Real st g is bounded
A2: 0 <= K
proof
consider r0 being set such that
A3: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A3;
now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
0_<=_r
let r be Real; ::_thesis: ( r in PreNorms g implies 0 <= r )
assume r in PreNorms g ; ::_thesis: 0 <= r
then ex t being Element of X st r = ||.(g . t).|| ;
hence 0 <= r ; ::_thesis: verum
end;
then 0 <= r0 by A3;
hence 0 <= K by A1, A3, SEQ_4:def_1; ::_thesis: verum
end;
take K = K; ::_thesis: g is bounded
now__::_thesis:_for_t_being_Element_of_X_holds_||.(g_._t).||_<=_K
let t be Element of X; ::_thesis: ||.(g . t).|| <= K
||.(g . t).|| in PreNorms g ;
hence ||.(g . t).|| <= K by A1, SEQ_4:def_1; ::_thesis: verum
end;
hence g is bounded by A2, Def4; ::_thesis: verum
end;
hence ( g is bounded iff PreNorms g is bounded_above ) by Th11; ::_thesis: verum
end;
definition
let X be non empty set ;
let Y be RealNormSpace;
func BoundedFunctionsNorm (X,Y) -> Function of (BoundedFunctions (X,Y)),REAL means :Def9: :: RSSPACE4:def 9
for x being set st x in BoundedFunctions (X,Y) holds
it . x = upper_bound (PreNorms (modetrans (x,X,Y)));
existence
ex b1 being Function of (BoundedFunctions (X,Y)),REAL st
for x being set st x in BoundedFunctions (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y)))
proof
deffunc H1( set ) -> Element of REAL = upper_bound (PreNorms (modetrans ($1,X,Y)));
A1: for z being set st z in BoundedFunctions (X,Y) holds
H1(z) in REAL ;
ex f being Function of (BoundedFunctions (X,Y)),REAL st
for x being set st x in BoundedFunctions (X,Y) holds
f . x = H1(x) from FUNCT_2:sch_2(A1);
hence ex b1 being Function of (BoundedFunctions (X,Y)),REAL st
for x being set st x in BoundedFunctions (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (BoundedFunctions (X,Y)),REAL st ( for x being set st x in BoundedFunctions (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being set st x in BoundedFunctions (X,Y) holds
b2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds
b1 = b2
proof
let NORM1, NORM2 be Function of (BoundedFunctions (X,Y)),REAL; ::_thesis: ( ( for x being set st x in BoundedFunctions (X,Y) holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being set st x in BoundedFunctions (X,Y) holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) implies NORM1 = NORM2 )
assume that
A2: for x being set st x in BoundedFunctions (X,Y) holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) and
A3: for x being set st x in BoundedFunctions (X,Y) holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ; ::_thesis: NORM1 = NORM2
A4: for z being set st z in BoundedFunctions (X,Y) holds
NORM1 . z = NORM2 . z
proof
let z be set ; ::_thesis: ( z in BoundedFunctions (X,Y) implies NORM1 . z = NORM2 . z )
assume A5: z in BoundedFunctions (X,Y) ; ::_thesis: NORM1 . z = NORM2 . z
NORM1 . z = upper_bound (PreNorms (modetrans (z,X,Y))) by A2, A5;
hence NORM1 . z = NORM2 . z by A3, A5; ::_thesis: verum
end;
( dom NORM1 = BoundedFunctions (X,Y) & dom NORM2 = BoundedFunctions (X,Y) ) by FUNCT_2:def_1;
hence NORM1 = NORM2 by A4, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines BoundedFunctionsNorm RSSPACE4:def_9_:_
for X being non empty set
for Y being RealNormSpace
for b3 being Function of (BoundedFunctions (X,Y)),REAL holds
( b3 = BoundedFunctionsNorm (X,Y) iff for x being set st x in BoundedFunctions (X,Y) holds
b3 . x = upper_bound (PreNorms (modetrans (x,X,Y))) );
theorem Th13: :: RSSPACE4:13
for X being non empty set
for Y being RealNormSpace
for f being bounded Function of X, the carrier of Y holds modetrans (f,X,Y) = f
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace
for f being bounded Function of X, the carrier of Y holds modetrans (f,X,Y) = f
let Y be RealNormSpace; ::_thesis: for f being bounded Function of X, the carrier of Y holds modetrans (f,X,Y) = f
let f be bounded Function of X, the carrier of Y; ::_thesis: modetrans (f,X,Y) = f
f in BoundedFunctions (X,Y) by Def5;
hence modetrans (f,X,Y) = f by Def7; ::_thesis: verum
end;
theorem Th14: :: RSSPACE4:14
for X being non empty set
for Y being RealNormSpace
for f being bounded Function of X, the carrier of Y holds (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace
for f being bounded Function of X, the carrier of Y holds (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)
let Y be RealNormSpace; ::_thesis: for f being bounded Function of X, the carrier of Y holds (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)
let f be bounded Function of X, the carrier of Y; ::_thesis: (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)
reconsider f9 = f as set ;
f in BoundedFunctions (X,Y) by Def5;
hence (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms (modetrans (f9,X,Y))) by Def9
.= upper_bound (PreNorms f) by Th13 ;
::_thesis: verum
end;
definition
let X be non empty set ;
let Y be RealNormSpace;
func R_NormSpace_of_BoundedFunctions (X,Y) -> non empty NORMSTR equals :: RSSPACE4:def 10
NORMSTR(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(BoundedFunctionsNorm (X,Y)) #);
coherence
NORMSTR(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(BoundedFunctionsNorm (X,Y)) #) is non empty NORMSTR ;
end;
:: deftheorem defines R_NormSpace_of_BoundedFunctions RSSPACE4:def_10_:_
for X being non empty set
for Y being RealNormSpace holds R_NormSpace_of_BoundedFunctions (X,Y) = NORMSTR(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(BoundedFunctionsNorm (X,Y)) #);
theorem Th15: :: RSSPACE4:15
for X being non empty set
for Y being RealNormSpace holds X --> (0. Y) = 0. (R_NormSpace_of_BoundedFunctions (X,Y))
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace holds X --> (0. Y) = 0. (R_NormSpace_of_BoundedFunctions (X,Y))
let Y be RealNormSpace; ::_thesis: X --> (0. Y) = 0. (R_NormSpace_of_BoundedFunctions (X,Y))
X --> (0. Y) = 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) by Th10
.= 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ;
hence X --> (0. Y) = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ; ::_thesis: verum
end;
theorem Th16: :: RSSPACE4:16
for X being non empty set
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for g being bounded Function of X, the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <= ||.f.||
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for g being bounded Function of X, the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <= ||.f.||
let Y be RealNormSpace; ::_thesis: for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for g being bounded Function of X, the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <= ||.f.||
let f be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: for g being bounded Function of X, the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <= ||.f.||
let g be bounded Function of X, the carrier of Y; ::_thesis: ( g = f implies for t being Element of X holds ||.(g . t).|| <= ||.f.|| )
assume A1: g = f ; ::_thesis: for t being Element of X holds ||.(g . t).|| <= ||.f.||
A2: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th11;
now__::_thesis:_for_t_being_Element_of_X_holds_||.(g_._t).||_<=_||.f.||
let t be Element of X; ::_thesis: ||.(g . t).|| <= ||.f.||
||.(g . t).|| in PreNorms g ;
then ||.(g . t).|| <= upper_bound (PreNorms g) by A2, SEQ_4:def_1;
hence ||.(g . t).|| <= ||.f.|| by A1, Th14; ::_thesis: verum
end;
hence for t being Element of X holds ||.(g . t).|| <= ||.f.|| ; ::_thesis: verum
end;
theorem :: RSSPACE4:17
for X being non empty set
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.||
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.||
let Y be RealNormSpace; ::_thesis: for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.||
let f be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: 0 <= ||.f.||
reconsider g = f as bounded Function of X, the carrier of Y by Def5;
consider r0 being set such that
A1: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A1;
A2: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th11;
now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
0_<=_r
let r be Real; ::_thesis: ( r in PreNorms g implies 0 <= r )
assume r in PreNorms g ; ::_thesis: 0 <= r
then ex t being Element of X st r = ||.(g . t).|| ;
hence 0 <= r ; ::_thesis: verum
end;
then 0 <= r0 by A1;
then 0 <= upper_bound (PreNorms g) by A2, A1, SEQ_4:def_1;
hence 0 <= ||.f.|| by Th14; ::_thesis: verum
end;
theorem Th18: :: RSSPACE4:18
for X being non empty set
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) holds
0 = ||.f.||
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) holds
0 = ||.f.||
let Y be RealNormSpace; ::_thesis: for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) holds
0 = ||.f.||
let f be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: ( f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) implies 0 = ||.f.|| )
assume A1: f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ; ::_thesis: 0 = ||.f.||
thus ||.f.|| = 0 ::_thesis: verum
proof
reconsider g = f as bounded Function of X, the carrier of Y by Def5;
set z = X --> (0. Y);
reconsider z = X --> (0. Y) as Function of X, the carrier of Y ;
consider r0 being set such that
A2: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A2;
A3: ( ( for s being real number st s in PreNorms g holds
s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45;
A4: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th11;
A5: z = g by A1, Th15;
A6: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
(_0_<=_r_&_r_<=_0_)
let r be Real; ::_thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) )
assume r in PreNorms g ; ::_thesis: ( 0 <= r & r <= 0 )
then consider t being Element of X such that
A7: r = ||.(g . t).|| ;
||.(g . t).|| = ||.(0. Y).|| by A5, FUNCOP_1:7
.= 0 ;
hence ( 0 <= r & r <= 0 ) by A7; ::_thesis: verum
end;
then 0 <= r0 by A2;
then upper_bound (PreNorms g) = 0 by A6, A4, A2, A3, SEQ_4:def_1;
hence ||.f.|| = 0 by Th14; ::_thesis: verum
end;
end;
theorem Th19: :: RSSPACE4:19
for X being non empty set
for Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
let Y be RealNormSpace; ::_thesis: for f, g, h being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
let f, g, h be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
reconsider f1 = f, g1 = g, h1 = h as VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)) ;
A1: ( h = f + g iff h1 = f1 + g1 ) ;
let f9, g9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & g9 = g & h9 = h implies ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) )
assume ( f9 = f & g9 = g & h9 = h ) ; ::_thesis: ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
hence ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) by A1, Th8; ::_thesis: verum
end;
theorem Th20: :: RSSPACE4:20
for X being non empty set
for Y being RealNormSpace
for f, h being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for a being Real holds
( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) )
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace
for f, h being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for a being Real holds
( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) )
let Y be RealNormSpace; ::_thesis: for f, h being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for a being Real holds
( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) )
let f, h be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for a being Real holds
( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) )
let f9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & h9 = h implies for a being Real holds
( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) ) )
assume A1: ( f9 = f & h9 = h ) ; ::_thesis: for a being Real holds
( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) )
reconsider h1 = h as VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)) ;
reconsider f1 = f as VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)) ;
let a be Real; ::_thesis: ( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) )
( h = a * f iff h1 = a * f1 ) ;
hence ( h = a * f iff for x being Element of X holds h9 . x = a * (f9 . x) ) by A1, Th9; ::_thesis: verum
end;
theorem Th21: :: RSSPACE4:21
for X being non empty set
for Y being RealNormSpace
for f, g being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for a being Real holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace
for f, g being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for a being Real holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
let Y be RealNormSpace; ::_thesis: for f, g being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for a being Real holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
let f, g be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: for a being Real holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
let a be Real; ::_thesis: ( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
A1: now__::_thesis:_(_f_=_0._(R_NormSpace_of_BoundedFunctions_(X,Y))_implies_||.f.||_=_0_)
assume A2: f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ; ::_thesis: ||.f.|| = 0
thus ||.f.|| = 0 ::_thesis: verum
proof
reconsider g = f as bounded Function of X, the carrier of Y by Def5;
set z = X --> (0. Y);
reconsider z = X --> (0. Y) as Function of X, the carrier of Y ;
consider r0 being set such that
A3: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A3;
A4: ( ( for s being real number st s in PreNorms g holds
s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45;
A5: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th11;
A6: z = g by A2, Th15;
A7: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
(_0_<=_r_&_r_<=_0_)
let r be Real; ::_thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) )
assume r in PreNorms g ; ::_thesis: ( 0 <= r & r <= 0 )
then consider t being Element of X such that
A8: r = ||.(g . t).|| ;
||.(g . t).|| = ||.(0. Y).|| by A6, FUNCOP_1:7
.= 0 ;
hence ( 0 <= r & r <= 0 ) by A8; ::_thesis: verum
end;
then 0 <= r0 by A3;
then upper_bound (PreNorms g) = 0 by A7, A5, A3, A4, SEQ_4:def_1;
hence ||.f.|| = 0 by Th14; ::_thesis: verum
end;
end;
A9: ||.(f + g).|| <= ||.f.|| + ||.g.||
proof
reconsider f1 = f, g1 = g, h1 = f + g as bounded Function of X, the carrier of Y by Def5;
A10: now__::_thesis:_for_t_being_Element_of_X_holds_||.(h1_._t).||_<=_||.f.||_+_||.g.||
let t be Element of X; ::_thesis: ||.(h1 . t).|| <= ||.f.|| + ||.g.||
( ||.(f1 . t).|| <= ||.f.|| & ||.(g1 . t).|| <= ||.g.|| ) by Th16;
then A11: ||.(f1 . t).|| + ||.(g1 . t).|| <= ||.f.|| + ||.g.|| by XREAL_1:7;
( ||.(h1 . t).|| = ||.((f1 . t) + (g1 . t)).|| & ||.((f1 . t) + (g1 . t)).|| <= ||.(f1 . t).|| + ||.(g1 . t).|| ) by Th19, NORMSP_1:def_1;
hence ||.(h1 . t).|| <= ||.f.|| + ||.g.|| by A11, XXREAL_0:2; ::_thesis: verum
end;
A12: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_
r_<=_||.f.||_+_||.g.||
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= ||.f.|| + ||.g.|| )
assume r in PreNorms h1 ; ::_thesis: r <= ||.f.|| + ||.g.||
then ex t being Element of X st r = ||.(h1 . t).|| ;
hence r <= ||.f.|| + ||.g.|| by A10; ::_thesis: verum
end;
( ( for s being real number st s in PreNorms h1 holds
s <= ||.f.|| + ||.g.|| ) implies upper_bound (PreNorms h1) <= ||.f.|| + ||.g.|| ) by SEQ_4:45;
hence ||.(f + g).|| <= ||.f.|| + ||.g.|| by A12, Th14; ::_thesis: verum
end;
A13: ||.(a * f).|| = (abs a) * ||.f.||
proof
reconsider f1 = f, h1 = a * f as bounded Function of X, the carrier of Y by Def5;
A14: ( ( for s being real number st s in PreNorms h1 holds
s <= (abs a) * ||.f.|| ) implies upper_bound (PreNorms h1) <= (abs a) * ||.f.|| ) by SEQ_4:45;
A15: now__::_thesis:_for_t_being_Element_of_X_holds_||.(h1_._t).||_<=_(abs_a)_*_||.f.||
let t be Element of X; ::_thesis: ||.(h1 . t).|| <= (abs a) * ||.f.||
A16: 0 <= abs a by COMPLEX1:46;
( ||.(h1 . t).|| = ||.(a * (f1 . t)).|| & ||.(a * (f1 . t)).|| = (abs a) * ||.(f1 . t).|| ) by Th20, NORMSP_1:def_1;
hence ||.(h1 . t).|| <= (abs a) * ||.f.|| by A16, Th16, XREAL_1:64; ::_thesis: verum
end;
A17: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_
r_<=_(abs_a)_*_||.f.||
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= (abs a) * ||.f.|| )
assume r in PreNorms h1 ; ::_thesis: r <= (abs a) * ||.f.||
then ex t being Element of X st r = ||.(h1 . t).|| ;
hence r <= (abs a) * ||.f.|| by A15; ::_thesis: verum
end;
A18: now__::_thesis:_(_(_a_<>_0_&_(abs_a)_*_||.f.||_<=_||.(a_*_f).||_)_or_(_a_=_0_&_(abs_a)_*_||.f.||_=_||.(a_*_f).||_)_)
percases ( a <> 0 or a = 0 ) ;
caseA19: a <> 0 ; ::_thesis: (abs a) * ||.f.|| <= ||.(a * f).||
A20: now__::_thesis:_for_t_being_Element_of_X_holds_||.(f1_._t).||_<=_((abs_a)_")_*_||.(a_*_f).||
let t be Element of X; ::_thesis: ||.(f1 . t).|| <= ((abs a) ") * ||.(a * f).||
A21: abs (a ") = abs (1 * (a "))
.= abs (1 / a) by XCMPLX_0:def_9
.= 1 / (abs a) by ABSVALUE:7
.= 1 * ((abs a) ") by XCMPLX_0:def_9
.= (abs a) " ;
h1 . t = a * (f1 . t) by Th20;
then A22: (a ") * (h1 . t) = ((a ") * a) * (f1 . t) by RLVECT_1:def_7
.= 1 * (f1 . t) by A19, XCMPLX_0:def_7
.= f1 . t by RLVECT_1:def_8 ;
( ||.((a ") * (h1 . t)).|| = (abs (a ")) * ||.(h1 . t).|| & 0 <= abs (a ") ) by COMPLEX1:46, NORMSP_1:def_1;
hence ||.(f1 . t).|| <= ((abs a) ") * ||.(a * f).|| by A22, A21, Th16, XREAL_1:64; ::_thesis: verum
end;
A23: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_f1_holds_
r_<=_((abs_a)_")_*_||.(a_*_f).||
let r be Real; ::_thesis: ( r in PreNorms f1 implies r <= ((abs a) ") * ||.(a * f).|| )
assume r in PreNorms f1 ; ::_thesis: r <= ((abs a) ") * ||.(a * f).||
then ex t being Element of X st r = ||.(f1 . t).|| ;
hence r <= ((abs a) ") * ||.(a * f).|| by A20; ::_thesis: verum
end;
A24: ( ( for s being real number st s in PreNorms f1 holds
s <= ((abs a) ") * ||.(a * f).|| ) implies upper_bound (PreNorms f1) <= ((abs a) ") * ||.(a * f).|| ) by SEQ_4:45;
( (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f1) & 0 <= abs a ) by Th14, COMPLEX1:46;
then (abs a) * ||.f.|| <= (abs a) * (((abs a) ") * ||.(a * f).||) by A23, A24, XREAL_1:64;
then A25: (abs a) * ||.f.|| <= ((abs a) * ((abs a) ")) * ||.(a * f).|| ;
abs a <> 0 by A19, COMPLEX1:47;
then (abs a) * ||.f.|| <= 1 * ||.(a * f).|| by A25, XCMPLX_0:def_7;
hence (abs a) * ||.f.|| <= ||.(a * f).|| ; ::_thesis: verum
end;
caseA26: a = 0 ; ::_thesis: (abs a) * ||.f.|| = ||.(a * f).||
reconsider fz = f as VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)) ;
A27: a * f = a * fz
.= 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) by A26, RLVECT_1:10
.= 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ;
thus (abs a) * ||.f.|| = 0 * ||.f.|| by A26, ABSVALUE:2
.= ||.(a * f).|| by A27, Th18 ; ::_thesis: verum
end;
end;
end;
(BoundedFunctionsNorm (X,Y)) . (a * f) = upper_bound (PreNorms h1) by Th14;
hence ||.(a * f).|| = (abs a) * ||.f.|| by A17, A14, A18, XXREAL_0:1; ::_thesis: verum
end;
now__::_thesis:_(_||.f.||_=_0_implies_f_=_0._(R_NormSpace_of_BoundedFunctions_(X,Y))_)
reconsider g = f as bounded Function of X, the carrier of Y by Def5;
set z = X --> (0. Y);
reconsider z = X --> (0. Y) as Function of X, the carrier of Y ;
assume A28: ||.f.|| = 0 ; ::_thesis: f = 0. (R_NormSpace_of_BoundedFunctions (X,Y))
now__::_thesis:_for_t_being_Element_of_X_holds_g_._t_=_z_._t
let t be Element of X; ::_thesis: g . t = z . t
||.(g . t).|| <= ||.f.|| by Th16;
then ||.(g . t).|| = 0 by A28;
hence g . t = 0. Y by NORMSP_0:def_5
.= z . t by FUNCOP_1:7 ;
::_thesis: verum
end;
then g = z by FUNCT_2:63;
hence f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) by Th15; ::_thesis: verum
end;
hence ( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) by A1, A13, A9; ::_thesis: verum
end;
theorem Th22: :: RSSPACE4:22
for X being non empty set
for Y being RealNormSpace holds
( R_NormSpace_of_BoundedFunctions (X,Y) is reflexive & R_NormSpace_of_BoundedFunctions (X,Y) is discerning & R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace-like )
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace holds
( R_NormSpace_of_BoundedFunctions (X,Y) is reflexive & R_NormSpace_of_BoundedFunctions (X,Y) is discerning & R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace-like )
let Y be RealNormSpace; ::_thesis: ( R_NormSpace_of_BoundedFunctions (X,Y) is reflexive & R_NormSpace_of_BoundedFunctions (X,Y) is discerning & R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace-like )
thus ||.(0. (R_NormSpace_of_BoundedFunctions (X,Y))).|| = 0 by Th21; :: according to NORMSP_0:def_6 ::_thesis: ( R_NormSpace_of_BoundedFunctions (X,Y) is discerning & R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace-like )
for x, y being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ) & ( x = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th21;
hence ( R_NormSpace_of_BoundedFunctions (X,Y) is discerning & R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace-like ) by NORMSP_0:def_5, NORMSP_1:def_1; ::_thesis: verum
end;
theorem Th23: :: RSSPACE4:23
for X being non empty set
for Y being RealNormSpace holds R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace holds R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace
let Y be RealNormSpace; ::_thesis: R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace
RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is RealLinearSpace ;
hence R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace by Th22, RSSPACE3:2; ::_thesis: verum
end;
registration
let X be non empty set ;
let Y be RealNormSpace;
cluster R_NormSpace_of_BoundedFunctions (X,Y) -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;
coherence
( R_NormSpace_of_BoundedFunctions (X,Y) is reflexive & R_NormSpace_of_BoundedFunctions (X,Y) is discerning & R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace-like & R_NormSpace_of_BoundedFunctions (X,Y) is vector-distributive & R_NormSpace_of_BoundedFunctions (X,Y) is scalar-distributive & R_NormSpace_of_BoundedFunctions (X,Y) is scalar-associative & R_NormSpace_of_BoundedFunctions (X,Y) is scalar-unital & R_NormSpace_of_BoundedFunctions (X,Y) is Abelian & R_NormSpace_of_BoundedFunctions (X,Y) is add-associative & R_NormSpace_of_BoundedFunctions (X,Y) is right_zeroed & R_NormSpace_of_BoundedFunctions (X,Y) is right_complementable ) by Th23;
end;
theorem Th24: :: RSSPACE4:24
for X being non empty set
for Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )
let Y be RealNormSpace; ::_thesis: for f, g, h being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )
let f, g, h be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )
let f9, g9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & g9 = g & h9 = h implies ( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) ) )
assume A1: ( f9 = f & g9 = g & h9 = h ) ; ::_thesis: ( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )
A2: now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h9_._x_=_(f9_._x)_-_(g9_._x)_)_implies_f_-_g_=_h_)
assume A3: for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) ; ::_thesis: f - g = h
now__::_thesis:_for_x_being_Element_of_X_holds_(h9_._x)_+_(g9_._x)_=_f9_._x
let x be Element of X; ::_thesis: (h9 . x) + (g9 . x) = f9 . x
h9 . x = (f9 . x) - (g9 . x) by A3;
then (h9 . x) + (g9 . x) = (f9 . x) - ((g9 . x) - (g9 . x)) by RLVECT_1:29;
then (h9 . x) + (g9 . x) = (f9 . x) - (0. Y) by RLVECT_1:15;
hence (h9 . x) + (g9 . x) = f9 . x by RLVECT_1:13; ::_thesis: verum
end;
then f = h + g by A1, Th19;
then f - g = h + (g - g) by RLVECT_1:def_3;
then f - g = h + (0. (R_NormSpace_of_BoundedFunctions (X,Y))) by RLVECT_1:15;
hence f - g = h by RLVECT_1:4; ::_thesis: verum
end;
now__::_thesis:_(_h_=_f_-_g_implies_for_x_being_Element_of_X_holds_h9_._x_=_(f9_._x)_-_(g9_._x)_)
assume h = f - g ; ::_thesis: for x being Element of X holds h9 . x = (f9 . x) - (g9 . x)
then h + g = f - (g - g) by RLVECT_1:29;
then h + g = f - (0. (R_NormSpace_of_BoundedFunctions (X,Y))) by RLVECT_1:15;
then A4: h + g = f by RLVECT_1:13;
now__::_thesis:_for_x_being_Element_of_X_holds_(f9_._x)_-_(g9_._x)_=_h9_._x
let x be Element of X; ::_thesis: (f9 . x) - (g9 . x) = h9 . x
f9 . x = (h9 . x) + (g9 . x) by A1, A4, Th19;
then (f9 . x) - (g9 . x) = (h9 . x) + ((g9 . x) - (g9 . x)) by RLVECT_1:def_3;
then (f9 . x) - (g9 . x) = (h9 . x) + (0. Y) by RLVECT_1:15;
hence (f9 . x) - (g9 . x) = h9 . x by RLVECT_1:4; ::_thesis: verum
end;
hence for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) ; ::_thesis: verum
end;
hence ( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) ) by A2; ::_thesis: verum
end;
Lm7: for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e
proof
let e be Real; ::_thesis: for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e
let seq be Real_Sequence; ::_thesis: ( seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e implies lim seq <= e )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e ; ::_thesis: lim seq <= e
consider k being Element of NAT such that
A3: for i being Element of NAT st k <= i holds
seq . i <= e by A2;
reconsider cseq = NAT --> e as Real_Sequence ;
A4: lim cseq = cseq . 0 by SEQ_4:26
.= e by FUNCOP_1:7 ;
A5: now__::_thesis:_for_i_being_Element_of_NAT_holds_(seq_^\_k)_._i_<=_cseq_._i
let i be Element of NAT ; ::_thesis: (seq ^\ k) . i <= cseq . i
( (seq ^\ k) . i = seq . (k + i) & seq . (k + i) <= e ) by A3, NAT_1:11, NAT_1:def_3;
hence (seq ^\ k) . i <= cseq . i by FUNCOP_1:7; ::_thesis: verum
end;
lim (seq ^\ k) = lim seq by A1, SEQ_4:20;
hence lim seq <= e by A1, A5, A4, SEQ_2:18; ::_thesis: verum
end;
theorem Th25: :: RSSPACE4:25
for X being non empty set
for Y being RealNormSpace st Y is complete holds
for seq being sequence of (R_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
proof
let X be non empty set ; ::_thesis: for Y being RealNormSpace st Y is complete holds
for seq being sequence of (R_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
let Y be RealNormSpace; ::_thesis: ( Y is complete implies for seq being sequence of (R_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent )
assume A1: Y is complete ; ::_thesis: for seq being sequence of (R_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
let vseq be sequence of (R_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A2: vseq is Cauchy_sequence_by_Norm ; ::_thesis: vseq is convergent
defpred S1[ set , set ] means ex xseq being sequence of Y st
( ( for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X,Y)) . $1 ) & xseq is convergent & $2 = lim xseq );
A3: for x being Element of X ex y being Element of Y st S1[x,y]
proof
let x be Element of X; ::_thesis: ex y being Element of Y st S1[x,y]
deffunc H1( Element of NAT ) -> Element of the carrier of Y = (modetrans ((vseq . $1),X,Y)) . x;
consider xseq being sequence of Y such that
A4: for n being Element of NAT holds xseq . n = H1(n) from FUNCT_2:sch_4();
take lim xseq ; ::_thesis: S1[x, lim xseq]
A5: for m, k being Element of NAT holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||
proof
let m, k be Element of NAT ; ::_thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||
vseq . k is bounded Function of X, the carrier of Y by Def5;
then A6: modetrans ((vseq . k),X,Y) = vseq . k by Th13;
reconsider h1 = (vseq . m) - (vseq . k) as bounded Function of X, the carrier of Y by Def5;
vseq . m is bounded Function of X, the carrier of Y by Def5;
then A7: modetrans ((vseq . m),X,Y) = vseq . m by Th13;
( xseq . m = (modetrans ((vseq . m),X,Y)) . x & xseq . k = (modetrans ((vseq . k),X,Y)) . x ) by A4;
then (xseq . m) - (xseq . k) = h1 . x by A7, A6, Th24;
hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| by Th16; ::_thesis: verum
end;
now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((xseq_._n)_-_(xseq_._m)).||_<_e
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e )
assume A8: e > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e
thus ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e ::_thesis: verum
proof
consider k being Element of NAT such that
A9: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, A8, RSSPACE3:8;
take k ; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e
thus for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e ::_thesis: verum
proof
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((xseq . n) - (xseq . m)).|| < e )
assume ( n >= k & m >= k ) ; ::_thesis: ||.((xseq . n) - (xseq . m)).|| < e
then A10: ||.((vseq . n) - (vseq . m)).|| < e by A9;
||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| by A5;
hence ||.((xseq . n) - (xseq . m)).|| < e by A10, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
then xseq is Cauchy_sequence_by_Norm by RSSPACE3:8;
then xseq is convergent by A1, LOPBAN_1:def_15;
hence S1[x, lim xseq] by A4; ::_thesis: verum
end;
consider f being Function of X, the carrier of Y such that
A11: for x being Element of X holds S1[x,f . x] from FUNCT_2:sch_3(A3);
reconsider tseq = f as Function of X, the carrier of Y ;
now__::_thesis:_for_e1_being_real_number_st_e1_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_m_>=_k_holds_
abs_((||.vseq.||_._m)_-_(||.vseq.||_._k))_<_e1
let e1 be real number ; ::_thesis: ( e1 > 0 implies ex k being Element of NAT st
for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 )
assume A12: e1 > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
reconsider e = e1 as Real by XREAL_0:def_1;
consider k being Element of NAT such that
A13: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, A12, RSSPACE3:8;
take k = k; ::_thesis: for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
now__::_thesis:_for_m_being_Element_of_NAT_st_m_>=_k_holds_
abs_((||.vseq.||_._m)_-_(||.vseq.||_._k))_<_e1
let m be Element of NAT ; ::_thesis: ( m >= k implies abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 )
assume m >= k ; ::_thesis: abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
then A14: ( ||.(vseq . m).|| = ||.vseq.|| . m & ||.((vseq . m) - (vseq . k)).|| < e ) by A13, NORMSP_0:def_4;
( abs (||.(vseq . m).|| - ||.(vseq . k).||) <= ||.((vseq . m) - (vseq . k)).|| & ||.(vseq . k).|| = ||.vseq.|| . k ) by NORMSP_0:def_4, NORMSP_1:9;
hence abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 by A14, XXREAL_0:2; ::_thesis: verum
end;
hence for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 ; ::_thesis: verum
end;
then A15: ||.vseq.|| is convergent by SEQ_4:41;
A16: tseq is bounded
proof
take lim ||.vseq.|| ; :: according to RSSPACE4:def_4 ::_thesis: ( 0 <= lim ||.vseq.|| & ( for x being Element of X holds ||.(tseq . x).|| <= lim ||.vseq.|| ) )
A17: now__::_thesis:_for_x_being_Element_of_X_holds_||.(tseq_._x).||_<=_lim_||.vseq.||
let x be Element of X; ::_thesis: ||.(tseq . x).|| <= lim ||.vseq.||
consider xseq being sequence of Y such that
A18: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X,Y)) . x and
A19: ( xseq is convergent & tseq . x = lim xseq ) by A11;
A20: for m being Element of NAT holds ||.(xseq . m).|| <= ||.(vseq . m).||
proof
let m be Element of NAT ; ::_thesis: ||.(xseq . m).|| <= ||.(vseq . m).||
( vseq . m is bounded Function of X, the carrier of Y & xseq . m = (modetrans ((vseq . m),X,Y)) . x ) by A18, Def5;
hence ||.(xseq . m).|| <= ||.(vseq . m).|| by Th13, Th16; ::_thesis: verum
end;
A21: for n being Element of NAT holds ||.xseq.|| . n <= ||.vseq.|| . n
proof
let n be Element of NAT ; ::_thesis: ||.xseq.|| . n <= ||.vseq.|| . n
( ||.xseq.|| . n = ||.(xseq . n).|| & ||.(xseq . n).|| <= ||.(vseq . n).|| ) by A20, NORMSP_0:def_4;
hence ||.xseq.|| . n <= ||.vseq.|| . n by NORMSP_0:def_4; ::_thesis: verum
end;
( ||.xseq.|| is convergent & ||.(tseq . x).|| = lim ||.xseq.|| ) by A19, LOPBAN_1:41;
hence ||.(tseq . x).|| <= lim ||.vseq.|| by A15, A21, SEQ_2:18; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.vseq.||_._n_>=_0
let n be Element of NAT ; ::_thesis: ||.vseq.|| . n >= 0
||.(vseq . n).|| >= 0 ;
hence ||.vseq.|| . n >= 0 by NORMSP_0:def_4; ::_thesis: verum
end;
hence ( 0 <= lim ||.vseq.|| & ( for x being Element of X holds ||.(tseq . x).|| <= lim ||.vseq.|| ) ) by A15, A17, SEQ_2:17; ::_thesis: verum
end;
A22: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e
proof
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e )
assume e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e
then consider k being Element of NAT such that
A23: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, RSSPACE3:8;
take k ; ::_thesis: for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_
for_x_being_Element_of_X_holds_||.(((modetrans_((vseq_._n),X,Y))_._x)_-_(tseq_._x)).||_<=_e
let n be Element of NAT ; ::_thesis: ( n >= k implies for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e )
assume A24: n >= k ; ::_thesis: for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e
now__::_thesis:_for_x_being_Element_of_X_holds_||.(((modetrans_((vseq_._n),X,Y))_._x)_-_(tseq_._x)).||_<=_e
let x be Element of X; ::_thesis: ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e
consider xseq being sequence of Y such that
A25: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X,Y)) . x and
A26: ( xseq is convergent & tseq . x = lim xseq ) by A11;
A27: for m, k being Element of NAT holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||
proof
let m, k be Element of NAT ; ::_thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||
vseq . k is bounded Function of X, the carrier of Y by Def5;
then A28: modetrans ((vseq . k),X,Y) = vseq . k by Th13;
reconsider h1 = (vseq . m) - (vseq . k) as bounded Function of X, the carrier of Y by Def5;
vseq . m is bounded Function of X, the carrier of Y by Def5;
then A29: modetrans ((vseq . m),X,Y) = vseq . m by Th13;
( xseq . m = (modetrans ((vseq . m),X,Y)) . x & xseq . k = (modetrans ((vseq . k),X,Y)) . x ) by A25;
then (xseq . m) - (xseq . k) = h1 . x by A29, A28, Th24;
hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| by Th16; ::_thesis: verum
end;
A30: for m being Element of NAT st m >= k holds
||.((xseq . n) - (xseq . m)).|| <= e
proof
let m be Element of NAT ; ::_thesis: ( m >= k implies ||.((xseq . n) - (xseq . m)).|| <= e )
assume m >= k ; ::_thesis: ||.((xseq . n) - (xseq . m)).|| <= e
then A31: ||.((vseq . n) - (vseq . m)).|| < e by A23, A24;
||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| by A27;
hence ||.((xseq . n) - (xseq . m)).|| <= e by A31, XXREAL_0:2; ::_thesis: verum
end;
||.((xseq . n) - (tseq . x)).|| <= e
proof
deffunc H1( Element of NAT ) -> Element of REAL = ||.((xseq . $1) - (xseq . n)).||;
consider rseq being Real_Sequence such that
A32: for m being Element of NAT holds rseq . m = H1(m) from SEQ_1:sch_1();
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
rseq_._x_=_||.(xseq_-_(xseq_._n)).||_._x
let x be set ; ::_thesis: ( x in NAT implies rseq . x = ||.(xseq - (xseq . n)).|| . x )
assume x in NAT ; ::_thesis: rseq . x = ||.(xseq - (xseq . n)).|| . x
then reconsider k = x as Element of NAT ;
thus rseq . x = ||.((xseq . k) - (xseq . n)).|| by A32
.= ||.((xseq - (xseq . n)) . k).|| by NORMSP_1:def_4
.= ||.(xseq - (xseq . n)).|| . x by NORMSP_0:def_4 ; ::_thesis: verum
end;
then A33: rseq = ||.(xseq - (xseq . n)).|| by FUNCT_2:12;
A34: ( xseq - (xseq . n) is convergent & lim (xseq - (xseq . n)) = (tseq . x) - (xseq . n) ) by A26, NORMSP_1:21, NORMSP_1:27;
then A35: lim rseq = ||.((tseq . x) - (xseq . n)).|| by A33, LOPBAN_1:20;
for m being Element of NAT st m >= k holds
rseq . m <= e
proof
let m be Element of NAT ; ::_thesis: ( m >= k implies rseq . m <= e )
assume A36: m >= k ; ::_thesis: rseq . m <= e
rseq . m = ||.((xseq . m) - (xseq . n)).|| by A32
.= ||.((xseq . n) - (xseq . m)).|| by NORMSP_1:7 ;
hence rseq . m <= e by A30, A36; ::_thesis: verum
end;
then lim rseq <= e by A34, A33, Lm7, LOPBAN_1:20;
hence ||.((xseq . n) - (tseq . x)).|| <= e by A35, NORMSP_1:7; ::_thesis: verum
end;
hence ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e by A25; ::_thesis: verum
end;
hence for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e ; ::_thesis: verum
end;
hence for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e ; ::_thesis: verum
end;
reconsider tseq = tseq as bounded Function of X, the carrier of Y by A16;
reconsider tv = tseq as Point of (R_NormSpace_of_BoundedFunctions (X,Y)) by Def5;
A37: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e
proof
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e )
assume e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e
then consider k being Element of NAT such that
A38: for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e by A22;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_
||.((vseq_._n)_-_tv).||_<=_e
set g1 = tseq;
let n be Element of NAT ; ::_thesis: ( n >= k implies ||.((vseq . n) - tv).|| <= e )
assume A39: n >= k ; ::_thesis: ||.((vseq . n) - tv).|| <= e
reconsider h1 = (vseq . n) - tv as bounded Function of X, the carrier of Y by Def5;
set f1 = modetrans ((vseq . n),X,Y);
A40: now__::_thesis:_for_t_being_Element_of_X_holds_||.(h1_._t).||_<=_e
let t be Element of X; ::_thesis: ||.(h1 . t).|| <= e
vseq . n is bounded Function of X, the carrier of Y by Def5;
then modetrans ((vseq . n),X,Y) = vseq . n by Th13;
then ||.(h1 . t).|| = ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| by Th24;
hence ||.(h1 . t).|| <= e by A38, A39; ::_thesis: verum
end;
A41: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_
r_<=_e
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= e )
assume r in PreNorms h1 ; ::_thesis: r <= e
then ex t being Element of X st r = ||.(h1 . t).|| ;
hence r <= e by A40; ::_thesis: verum
end;
( ( for s being real number st s in PreNorms h1 holds
s <= e ) implies upper_bound (PreNorms h1) <= e ) by SEQ_4:45;
hence ||.((vseq . n) - tv).|| <= e by A41, Th14; ::_thesis: verum
end;
hence ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e ; ::_thesis: verum
end;
for e being Real st e > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
proof
let e be Real; ::_thesis: ( e > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e )
assume A42: e > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
consider m being Element of NAT such that
A43: for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| <= e / 2 by A37, A42, XREAL_1:215;
A44: e / 2 < e by A42, XREAL_1:216;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_
||.((vseq_._n)_-_tv).||_<_e
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume n >= m ; ::_thesis: ||.((vseq . n) - tv).|| < e
then ||.((vseq . n) - tv).|| <= e / 2 by A43;
hence ||.((vseq . n) - tv).|| < e by A44, XXREAL_0:2; ::_thesis: verum
end;
hence ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e ; ::_thesis: verum
end;
hence vseq is convergent by NORMSP_1:def_6; ::_thesis: verum
end;
theorem Th26: :: RSSPACE4:26
for X being non empty set
for Y being RealBanachSpace holds R_NormSpace_of_BoundedFunctions (X,Y) is RealBanachSpace
proof
let X be non empty set ; ::_thesis: for Y being RealBanachSpace holds R_NormSpace_of_BoundedFunctions (X,Y) is RealBanachSpace
let Y be RealBanachSpace; ::_thesis: R_NormSpace_of_BoundedFunctions (X,Y) is RealBanachSpace
for seq being sequence of (R_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent by Th25;
hence R_NormSpace_of_BoundedFunctions (X,Y) is RealBanachSpace by LOPBAN_1:def_15; ::_thesis: verum
end;
registration
let X be non empty set ;
let Y be RealBanachSpace;
cluster R_NormSpace_of_BoundedFunctions (X,Y) -> non empty complete ;
coherence
R_NormSpace_of_BoundedFunctions (X,Y) is complete by Th26;
end;