:: by Jan Popio{\l}ek

::

:: Received September 20, 1990

:: Copyright (c) 1990-2019 Association of Mizar Users

definition

attr c_{1} is strict ;

struct NORMSTR -> RLSStruct , N-ZeroStr ;

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

end;
struct NORMSTR -> RLSStruct , N-ZeroStr ;

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

registration
end;

deffunc H

set V = the RealLinearSpace;

Lm1: the carrier of ((0). the RealLinearSpace) = {(0. the RealLinearSpace)}

by RLSUB_1:def 3;

reconsider niltonil = the carrier of ((0). the RealLinearSpace) --> (In (0,REAL)) as Function of the carrier of ((0). the RealLinearSpace),REAL ;

0. the RealLinearSpace is VECTOR of ((0). the RealLinearSpace)

by Lm1, TARSKI:def 1;

then Lm2: niltonil . (0. the RealLinearSpace) = 0

by FUNCOP_1:7;

Lm3: for u being VECTOR of ((0). the RealLinearSpace)

for a being Real holds niltonil . (a * u) = |.a.| * (niltonil . u)

proof end;

Lm4: for u, v being VECTOR of ((0). the RealLinearSpace) holds niltonil . (u + v) <= (niltonil . u) + (niltonil . v)

proof end;

reconsider X = NORMSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),niltonil #) as non empty NORMSTR ;

Lm5: now :: thesis: for x, y being Point of X

for a being Real holds

( ( ||.x.|| = 0 implies x = H_{1}(X) ) & ( x = H_{1}(X) implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

for a being Real holds

( ( ||.x.|| = 0 implies x = H

let x, y be Point of X; :: thesis: for a being Real holds

( ( ||.x.|| = 0 implies x = H_{1}(X) ) & ( x = H_{1}(X) implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

let a be Real; :: thesis: ( ( ||.x.|| = 0 implies x = H_{1}(X) ) & ( x = H_{1}(X) implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

reconsider u = x, w = y as VECTOR of ((0). the RealLinearSpace) ;

H_{1}(X) = 0. the RealLinearSpace
by RLSUB_1:11;

hence ( ||.x.|| = 0 iff x = H_{1}(X) )
by Lm1, FUNCOP_1:7, TARSKI:def 1; :: thesis: ( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

a * x = a * u ;

hence ||.(a * x).|| = |.a.| * ||.x.|| by Lm3; :: thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||

x + y = u + w ;

hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by Lm4; :: thesis: verum

end;
( ( ||.x.|| = 0 implies x = H

let a be Real; :: thesis: ( ( ||.x.|| = 0 implies x = H

reconsider u = x, w = y as VECTOR of ((0). the RealLinearSpace) ;

H

hence ( ||.x.|| = 0 iff x = H

a * x = a * u ;

hence ||.(a * x).|| = |.a.| * ||.x.|| by Lm3; :: thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||

x + y = u + w ;

hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by Lm4; :: thesis: verum

:: deftheorem Def1 defines RealNormSpace-like NORMSP_1:def 1 :

for IT being non empty NORMSTR holds

( IT is RealNormSpace-like iff for x, y being Point of IT

for a being Real holds

( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) );

for IT being non empty NORMSTR holds

( IT is RealNormSpace-like iff for x, y being Point of IT

for a being Real holds

( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) );

registration

ex b_{1} being non empty NORMSTR st

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

cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like for NORMSTR ;

existence ex b

( b

proof end;

definition

mode RealNormSpace is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR ;

end;
registration
end;

theorem :: NORMSP_1:5

for a, b being Real

for RNS being RealNormSpace

for x, y being Point of RNS holds ||.((a * x) + (b * y)).|| <= (|.a.| * ||.x.||) + (|.b.| * ||.y.||)

for RNS being RealNormSpace

for x, y being Point of RNS holds ||.((a * x) + (b * y)).|| <= (|.a.| * ||.x.||) + (|.b.| * ||.y.||)

proof end;

theorem Th9: :: NORMSP_1:9

for RNS being RealNormSpace

for x, y being Point of RNS holds |.(||.x.|| - ||.y.||).| <= ||.(x - y).||

for x, y being Point of RNS holds |.(||.x.|| - ||.y.||).| <= ||.(x - y).||

proof end;

theorem Th10: :: NORMSP_1:10

for RNS being RealNormSpace

for x, y, z being Point of RNS holds ||.(x - z).|| <= ||.(x - y).|| + ||.(y - z).||

for x, y, z being Point of RNS holds ||.(x - z).|| <= ||.(x - y).|| + ||.(y - z).||

proof end;

theorem :: NORMSP_1:11

theorem :: NORMSP_1:12

for f being Function

for RNS being non empty 1-sorted

for x being Element of RNS holds

( f is sequence of RNS iff ( dom f = NAT & ( for d being set st d in NAT holds

f . d is Element of RNS ) ) )

for RNS being non empty 1-sorted

for x being Element of RNS holds

( f is sequence of RNS iff ( dom f = NAT & ( for d being set st d in NAT holds

f . d is Element of RNS ) ) )

proof end;

theorem :: NORMSP_1:13

for RNS being non empty 1-sorted

for x being Element of RNS ex S being sequence of RNS st rng S = {x}

for x being Element of RNS ex S being sequence of RNS st rng S = {x}

proof end;

theorem :: NORMSP_1:14

for RNS being non empty 1-sorted

for S being sequence of RNS st ex x being Element of RNS st

for n being Nat holds S . n = x holds

ex x being Element of RNS st rng S = {x}

for S being sequence of RNS st ex x being Element of RNS st

for n being Nat holds S . n = x holds

ex x being Element of RNS st rng S = {x}

proof end;

theorem :: NORMSP_1:15

for RNS being non empty 1-sorted

for S being sequence of RNS st ex x being Element of RNS st rng S = {x} holds

for n being Nat holds S . n = S . (n + 1)

for S being sequence of RNS st ex x being Element of RNS st rng S = {x} holds

for n being Nat holds S . n = S . (n + 1)

proof end;

theorem :: NORMSP_1:16

for RNS being non empty 1-sorted

for S being sequence of RNS st ( for n being Nat holds S . n = S . (n + 1) ) holds

for n, k being Nat holds S . n = S . (n + k)

for S being sequence of RNS st ( for n being Nat holds S . n = S . (n + 1) ) holds

for n, k being Nat holds S . n = S . (n + k)

proof end;

theorem :: NORMSP_1:17

for RNS being non empty 1-sorted

for S being sequence of RNS st ( for n, k being Nat holds S . n = S . (n + k) ) holds

for n, m being Nat holds S . n = S . m

for S being sequence of RNS st ( for n, k being Nat holds S . n = S . (n + k) ) holds

for n, m being Nat holds S . n = S . m

proof end;

theorem :: NORMSP_1:18

for RNS being non empty 1-sorted

for S being sequence of RNS st ( for n, m being Nat holds S . n = S . m ) holds

ex x being Element of RNS st

for n being Nat holds S . n = x

for S being sequence of RNS st ( for n, m being Nat holds S . n = S . m ) holds

ex x being Element of RNS st

for n being Nat holds S . n = x

proof end;

definition

let RNS be non empty addLoopStr ;

let S1, S2 be sequence of RNS;

ex b_{1} being sequence of RNS st

for n being Nat holds b_{1} . n = (S1 . n) + (S2 . n)

for b_{1}, b_{2} being sequence of RNS st ( for n being Nat holds b_{1} . n = (S1 . n) + (S2 . n) ) & ( for n being Nat holds b_{2} . n = (S1 . n) + (S2 . n) ) holds

b_{1} = b_{2}

end;
let S1, S2 be sequence of RNS;

func S1 + S2 -> sequence of RNS means :Def2: :: NORMSP_1:def 2

for n being Nat holds it . n = (S1 . n) + (S2 . n);

existence for n being Nat holds it . n = (S1 . n) + (S2 . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines + NORMSP_1:def 2 :

for RNS being non empty addLoopStr

for S1, S2, b_{4} being sequence of RNS holds

( b_{4} = S1 + S2 iff for n being Nat holds b_{4} . n = (S1 . n) + (S2 . n) );

for RNS being non empty addLoopStr

for S1, S2, b

( b

definition

let RNS be non empty addLoopStr ;

let S1, S2 be sequence of RNS;

ex b_{1} being sequence of RNS st

for n being Nat holds b_{1} . n = (S1 . n) - (S2 . n)

for b_{1}, b_{2} being sequence of RNS st ( for n being Nat holds b_{1} . n = (S1 . n) - (S2 . n) ) & ( for n being Nat holds b_{2} . n = (S1 . n) - (S2 . n) ) holds

b_{1} = b_{2}

end;
let S1, S2 be sequence of RNS;

func S1 - S2 -> sequence of RNS means :Def3: :: NORMSP_1:def 3

for n being Nat holds it . n = (S1 . n) - (S2 . n);

existence for n being Nat holds it . n = (S1 . n) - (S2 . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines - NORMSP_1:def 3 :

for RNS being non empty addLoopStr

for S1, S2, b_{4} being sequence of RNS holds

( b_{4} = S1 - S2 iff for n being Nat holds b_{4} . n = (S1 . n) - (S2 . n) );

for RNS being non empty addLoopStr

for S1, S2, b

( b

definition

let RNS be non empty addLoopStr ;

let S be sequence of RNS;

let x be Element of RNS;

ex b_{1} being sequence of RNS st

for n being Nat holds b_{1} . n = (S . n) - x

for b_{1}, b_{2} being sequence of RNS st ( for n being Nat holds b_{1} . n = (S . n) - x ) & ( for n being Nat holds b_{2} . n = (S . n) - x ) holds

b_{1} = b_{2}

end;
let S be sequence of RNS;

let x be Element of RNS;

func S - x -> sequence of RNS means :Def4: :: NORMSP_1:def 4

for n being Nat holds it . n = (S . n) - x;

existence for n being Nat holds it . n = (S . n) - x;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines - NORMSP_1:def 4 :

for RNS being non empty addLoopStr

for S being sequence of RNS

for x being Element of RNS

for b_{4} being sequence of RNS holds

( b_{4} = S - x iff for n being Nat holds b_{4} . n = (S . n) - x );

for RNS being non empty addLoopStr

for S being sequence of RNS

for x being Element of RNS

for b

( b

definition

let RNS be non empty RLSStruct ;

let S be sequence of RNS;

let a be Real;

ex b_{1} being sequence of RNS st

for n being Nat holds b_{1} . n = a * (S . n)

for b_{1}, b_{2} being sequence of RNS st ( for n being Nat holds b_{1} . n = a * (S . n) ) & ( for n being Nat holds b_{2} . n = a * (S . n) ) holds

b_{1} = b_{2}

end;
let S be sequence of RNS;

let a be Real;

func a * S -> sequence of RNS means :Def5: :: NORMSP_1:def 5

for n being Nat holds it . n = a * (S . n);

existence for n being Nat holds it . n = a * (S . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines * NORMSP_1:def 5 :

for RNS being non empty RLSStruct

for S being sequence of RNS

for a being Real

for b_{4} being sequence of RNS holds

( b_{4} = a * S iff for n being Nat holds b_{4} . n = a * (S . n) );

for RNS being non empty RLSStruct

for S being sequence of RNS

for a being Real

for b

( b

:: deftheorem defines convergent NORMSP_1:def 6 :

for RNS being RealNormSpace

for S being sequence of RNS holds

( S is convergent iff ex g being Point of RNS st

for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - g).|| < r );

for RNS being RealNormSpace

for S being sequence of RNS holds

( S is convergent iff ex g being Point of RNS st

for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - g).|| < r );

theorem Th19: :: NORMSP_1:19

for RNS being RealNormSpace

for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds

S1 + S2 is convergent

for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds

S1 + S2 is convergent

proof end;

theorem Th20: :: NORMSP_1:20

for RNS being RealNormSpace

for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds

S1 - S2 is convergent

for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds

S1 - S2 is convergent

proof end;

theorem Th21: :: NORMSP_1:21

for RNS being RealNormSpace

for x being Point of RNS

for S being sequence of RNS st S is convergent holds

S - x is convergent

for x being Point of RNS

for S being sequence of RNS st S is convergent holds

S - x is convergent

proof end;

theorem Th22: :: NORMSP_1:22

for a being Real

for RNS being RealNormSpace

for S being sequence of RNS st S is convergent holds

a * S is convergent

for RNS being RealNormSpace

for S being sequence of RNS st S is convergent holds

a * S is convergent

proof end;

theorem Th23: :: NORMSP_1:23

for RNS being RealNormSpace

for S being sequence of RNS st S is convergent holds

||.S.|| is convergent

for S being sequence of RNS st S is convergent holds

||.S.|| is convergent

proof end;

definition

let RNS be RealNormSpace;

let S be sequence of RNS;

assume A1: S is convergent ;

ex b_{1} being Point of RNS st

for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - b_{1}).|| < r
by A1;

uniqueness

for b_{1}, b_{2} being Point of RNS st ( for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - b_{1}).|| < r ) & ( for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - b_{2}).|| < r ) holds

b_{1} = b_{2}

end;
let S be sequence of RNS;

assume A1: S is convergent ;

func lim S -> Point of RNS means :Def7: :: NORMSP_1:def 7

for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - it).|| < r;

existence for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - it).|| < r;

ex b

for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - b

uniqueness

for b

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - b

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - b

b

proof end;

:: deftheorem Def7 defines lim NORMSP_1:def 7 :

for RNS being RealNormSpace

for S being sequence of RNS st S is convergent holds

for b_{3} being Point of RNS holds

( b_{3} = lim S iff for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - b_{3}).|| < r );

for RNS being RealNormSpace

for S being sequence of RNS st S is convergent holds

for b

( b

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - b

theorem :: NORMSP_1:24

for RNS being RealNormSpace

for g being Point of RNS

for S being sequence of RNS st S is convergent & lim S = g holds

( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )

for g being Point of RNS

for S being sequence of RNS st S is convergent & lim S = g holds

( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )

proof end;

theorem :: NORMSP_1:25

for RNS being RealNormSpace

for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds

lim (S1 + S2) = (lim S1) + (lim S2)

for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds

lim (S1 + S2) = (lim S1) + (lim S2)

proof end;

theorem :: NORMSP_1:26

for RNS being RealNormSpace

for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds

lim (S1 - S2) = (lim S1) - (lim S2)

for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds

lim (S1 - S2) = (lim S1) - (lim S2)

proof end;

theorem :: NORMSP_1:27

for RNS being RealNormSpace

for x being Point of RNS

for S being sequence of RNS st S is convergent holds

lim (S - x) = (lim S) - x

for x being Point of RNS

for S being sequence of RNS st S is convergent holds

lim (S - x) = (lim S) - x

proof end;

theorem :: NORMSP_1:28

for a being Real

for RNS being RealNormSpace

for S being sequence of RNS st S is convergent holds

lim (a * S) = a * (lim S)

for RNS being RealNormSpace

for S being sequence of RNS st S is convergent holds

lim (a * S) = a * (lim S)

proof end;