:: NORMSP_1 semantic presentation

definition

attr a₁ is strict;
struct NORMSTR -> RLSStruct ;
aggr NORMSTR(# carrier, Zero, add, Mult, norm #) -> NORMSTR ;
sel norm c₁ -> Function of the carrier of a₁, REAL ;

end;

registration

cluster non empty NORMSTR ;
existence

proof end;

end;

deffunc H₁( NORMSTR ) -> Element of the carrier of a₁ = 0. a₁;

definition

let c₁ be non empty NORMSTR ;
let c₂ be Point of c₁;
func ||.c₂.|| -> Real equals :: NORMSP_1:def 1
the norm of a₁ . a₂;
coherence ;

end;

:: deftheorem Def1 defines ||. NORMSP_1:def 1 :

consider c₁ being RealLinearSpace;

Lemma1: the carrier of ((0). c₁) = {(0. c₁)}
by RLSUB_1:def 3;

reconsider c₂ = the carrier of ((0). c₁) --> 0 as Function of the carrier of ((0). c₁), REAL by FUNCOP_1:57;

Lemma2: for b₁ being VECTOR of ((0). c₁) holds c₂ . b₁ = 0
by FUNCOP_1:13;

0. c₁ is VECTOR of ((0). c₁)
by Lemma1, TARSKI:def 1;

then Lemma3: c₂ . (0. c₁) = 0
by Lemma2;

Lemma4: for b₁ being VECTOR of ((0). c₁)
for b₂ being Real holds c₂ . (b₂ * b₁) = (abs b₂) * (c₂ . b₁)

proof end;

Lemma5: for b₁, b₂ being VECTOR of ((0). c₁) holds c₂ . (b₁ + b₂) <= (c₂ . b₁) + (c₂ . b₂)

proof end;

reconsider c₃ = NORMSTR(# the carrier of ((0). c₁),the Zero of ((0). c₁),the add of ((0). c₁),the Mult of ((0). c₁),c₂ #) as non empty NORMSTR by STRUCT_0:def 1;

E6: now

let c₄, c₅ be Point of c₃;
let c₆ be Real;
reconsider c₇ = c₄, c₈ = c₅ as VECTOR of ((0). c₁) ;
thus ( ||.c₄.|| = 0 iff c₄ = H₁(c₃) )

proof

H₁(c₃) = the Zero of c₃
.= 0. ((0). c₁)
.= 0. c₁ by RLSUB_1:19 ;
hence ( ||.c₄.|| = 0 iff c₄ = H₁(c₃) ) by Lemma1, Lemma3, TARSKI:def 1;

end;

c₆ * c₄ = the Mult of c₃ . [c₆,c₇]
.= c₆ * c₇ ;
hence ||.(c₆ * c₄).|| = (abs c₆) * ||.c₄.|| by Lemma4;
c₄ + c₅ = the add of c₃ . [c₄,c₅]
.= c₇ + c₈ ;
hence ||.(c₄ + c₅).|| <= ||.c₄.|| + ||.c₅.|| by Lemma5;

end;

definition

let c₄ be non empty NORMSTR ;
attr a₁ is RealNormSpace-like means :Def2: :: NORMSP_1:def 2
for b₁, b₂ being Point of a₁
for b₃ being Real holds
( ( ||.b₁.|| = 0 implies b₁ = 0. a₁ ) & ( b₁ = 0. a₁ implies ||.b₁.|| = 0 ) & ||.(b₃ * b₁).|| = (abs b₃) * ||.b₁.|| & ||.(b₁ + b₂).|| <= ||.b₁.|| + ||.b₂.|| );

end;

:: deftheorem Def2 defines RealNormSpace-like NORMSP_1:def 2 :

registration

cluster non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like strict RealNormSpace-like NORMSTR ;
existence

proof end;

end;

definition

mode RealNormSpace is non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like RealNormSpace-like NORMSTR ;

end;

theorem Th1: :: NORMSP_1:1

canceled;

theorem Th2: :: NORMSP_1:2

canceled;

theorem Th3: :: NORMSP_1:3

canceled;

theorem Th4: :: NORMSP_1:4

canceled;

theorem Th5: :: NORMSP_1:5

for b₁ being RealNormSpace holds ||.(0. b₁).|| = 0 by Def2;

theorem Th6: :: NORMSP_1:6

for b₁ being RealNormSpace
for b₂ being Point of b₁ holds ||.(- b₂).|| = ||.b₂.||

proof end;

theorem Th7: :: NORMSP_1:7

for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ holds ||.(b₂ - b₃).|| <= ||.b₂.|| + ||.b₃.||

proof end;

theorem Th8: :: NORMSP_1:8

for b₁ being RealNormSpace
for b₂ being Point of b₁ holds 0 <= ||.b₂.||

proof end;

theorem Th9: :: NORMSP_1:9

for b₁, b₂ being Real
for b₃ being RealNormSpace
for b₄, b₅ being Point of b₃ holds ||.((b₁ * b₄) + (b₂ * b₅)).|| <= ((abs b₁) * ||.b₄.||) + ((abs b₂) * ||.b₅.||)

proof end;

theorem Th10: :: NORMSP_1:10

for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ holds
( ||.(b₂ - b₃).|| = 0 iff b₂ = b₃ )

proof end;

theorem Th11: :: NORMSP_1:11

for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ holds ||.(b₂ - b₃).|| = ||.(b₃ - b₂).||

proof end;

theorem Th12: :: NORMSP_1:12

for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ holds ||.b₂.|| - ||.b₃.|| <= ||.(b₂ - b₃).||

proof end;

theorem Th13: :: NORMSP_1:13

for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ holds abs (||.b₂.|| - ||.b₃.||) <= ||.(b₂ - b₃).||

proof end;

theorem Th14: :: NORMSP_1:14

for b₁ being RealNormSpace
for b₂, b₃, b₄ being Point of b₁ holds ||.(b₂ - b₃).|| <= ||.(b₂ - b₄).|| + ||.(b₄ - b₃).||

proof end;

theorem Th15: :: NORMSP_1:15

for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ st b₂ <> b₃ holds
||.(b₂ - b₃).|| <> 0 by Th10;

definition

let c₄ be 1-sorted ;
mode sequence of a₁ is Function of NAT ,the carrier of a₁;

end;

theorem Th16: :: NORMSP_1:16

canceled;

theorem Th17: :: NORMSP_1:17

for b₁ being Function
for b₂ being non empty 1-sorted
for b₃ being Element of b₂ holds
( b₁ is sequence of b₂ iff ( dom b₁ = NAT & ( for b₄ being set st b₄ in NAT holds
b₁ . b₄ is Element of b₂ ) ) )

proof end;

theorem Th18: :: NORMSP_1:18

canceled;

theorem Th19: :: NORMSP_1:19

for b₁ being non empty 1-sorted
for b₂ being Element of b₁ ex b₃ being sequence of b₁ st rng b₃ = {b₂}

proof end;

theorem Th20: :: NORMSP_1:20

for b₁ being non empty 1-sorted
for b₂ being sequence of b₁ st ex b₃ being Element of b₁ st
for b₄ being Nat holds b₂ . b₄ = b₃ holds
ex b₃ being Element of b₁ st rng b₂ = {b₃}

proof end;

theorem Th21: :: NORMSP_1:21

for b₁ being non empty 1-sorted
for b₂ being sequence of b₁ st ex b₃ being Element of b₁ st rng b₂ = {b₃} holds
for b₃ being Nat holds b₂ . b₃ = b₂ . (b₃ + 1)

proof end;

theorem Th22: :: NORMSP_1:22

for b₁ being non empty 1-sorted
for b₂ being sequence of b₁ st ( for b₃ being Nat holds b₂ . b₃ = b₂ . (b₃ + 1) ) holds
for b₃, b₄ being Nat holds b₂ . b₃ = b₂ . (b₃ + b₄)

proof end;

theorem Th23: :: NORMSP_1:23

for b₁ being non empty 1-sorted
for b₂ being sequence of b₁ st ( for b₃, b₄ being Nat holds b₂ . b₃ = b₂ . (b₃ + b₄) ) holds
for b₃, b₄ being Nat holds b₂ . b₃ = b₂ . b₄

proof end;

theorem Th24: :: NORMSP_1:24

for b₁ being non empty 1-sorted
for b₂ being sequence of b₁ st ( for b₃, b₄ being Nat holds b₂ . b₃ = b₂ . b₄ ) holds
ex b₃ being Element of b₁ st
for b₄ being Nat holds b₂ . b₄ = b₃

proof end;

theorem Th25: :: NORMSP_1:25

for b₁ being RealNormSpace ex b₂ being sequence of b₁ st rng b₂ = {(0. b₁)} by Th19;

definition

let c₄ be non empty 1-sorted ;
let c₅ be sequence of c₄;
canceled;
redefine attr constant as a₂ is constant means :Def4: :: NORMSP_1:def 4
ex b₁ being Element of a₁ st
for b₂ being Nat holds a₂ . b₂ = b₁;
compatibility

proof end;

end;

:: deftheorem Def3 NORMSP_1:def 3 :

:: deftheorem Def4 defines constant NORMSP_1:def 4 :

theorem Th26: :: NORMSP_1:26

canceled;

theorem Th27: :: NORMSP_1:27

for b₁ being non empty 1-sorted
for b₂ being sequence of b₁ holds
( b₂ is constant iff ex b₃ being Element of b₁ st rng b₂ = {b₃} )

proof end;

Lemma23: for b₁ being non empty 1-sorted
for b₂ being sequence of b₁
for b₃ being Nat holds b₂ . b₃ is Element of b₁
;

definition

let c₄ be non empty 1-sorted ;
let c₅ be sequence of c₄;
let c₆ be Nat;
redefine func . as c₂ . c₃ -> Element of a₁;
coherence by Lemma23;

end;

definition

let c₄ be RealLinearSpace;
let c₅, c₆ be sequence of c₄;
func c₂ + c₃ -> sequence of a₁ means :Def5: :: NORMSP_1:def 5
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) + (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines + NORMSP_1:def 5 :

definition

let c₄ be RealLinearSpace;
let c₅, c₆ be sequence of c₄;
func c₂ - c₃ -> sequence of a₁ means :Def6: :: NORMSP_1:def 6
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) - (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines - NORMSP_1:def 6 :

definition

let c₄ be RealLinearSpace;
let c₅ be sequence of c₄;
let c₆ be Element of c₄;
func c₂ - c₃ -> sequence of a₁ means :Def7: :: NORMSP_1:def 7
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) - a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines - NORMSP_1:def 7 :

definition

let c₄ be RealLinearSpace;
let c₅ be sequence of c₄;
let c₆ be Real;
func c₃ * c₂ -> sequence of a₁ means :Def8: :: NORMSP_1:def 8
for b₁ being Nat holds a₄ . b₁ = a₃ * (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines * NORMSP_1:def 8 :

definition

let c₄ be RealNormSpace;
let c₅ be sequence of c₄;
attr a₂ is convergent means :Def9: :: NORMSP_1:def 9
ex b₁ being Point of a₁ st
for b₂ being Real st 0 < b₂ holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
||.((a₂ . b₄) - b₁).|| < b₂;

end;

:: deftheorem Def9 defines convergent NORMSP_1:def 9 :

theorem Th28: :: NORMSP_1:28

canceled;

theorem Th29: :: NORMSP_1:29

canceled;

theorem Th30: :: NORMSP_1:30

canceled;

theorem Th31: :: NORMSP_1:31

canceled;

theorem Th32: :: NORMSP_1:32

canceled;

theorem Th33: :: NORMSP_1:33

canceled;

theorem Th34: :: NORMSP_1:34

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
b₂ + b₃ is convergent

proof end;

theorem Th35: :: NORMSP_1:35

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
b₂ - b₃ is convergent

proof end;

theorem Th36: :: NORMSP_1:36

for b₁ being RealNormSpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
b₃ - b₂ is convergent

proof end;

theorem Th37: :: NORMSP_1:37

for b₁ being Real
for b₂ being RealNormSpace
for b₃ being sequence of b₂ st b₃ is convergent holds
b₁ * b₃ is convergent

proof end;

definition

let c₄ be RealNormSpace;
let c₅ be sequence of c₄;
func ||.c₂.|| -> Real_Sequence means :Def10: :: NORMSP_1:def 10
for b₁ being Nat holds a₃ . b₁ = ||.(a₂ . b₁).||;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines ||. NORMSP_1:def 10 :

theorem Th38: :: NORMSP_1:38

canceled;

theorem Th39: :: NORMSP_1:39

for b₁ being RealNormSpace
for b₂ being sequence of b₁ st b₂ is convergent holds
||.b₂.|| is convergent

proof end;

definition

let c₄ be RealNormSpace;
let c₅ be sequence of c₄;
assume E35: c₅ is convergent ;
func lim c₂ -> Point of a₁ means :Def11: :: NORMSP_1:def 11
for b₁ being Real st 0 < b₁ holds
ex b₂ being Nat st
for b₃ being Nat st b₂ <= b₃ holds
||.((a₂ . b₃) - a₃).|| < b₁;
existence by E35, Def9;
uniqueness

proof end;

end;

:: deftheorem Def11 defines lim NORMSP_1:def 11 :

theorem Th40: :: NORMSP_1:40

canceled;

theorem Th41: :: NORMSP_1:41

for b₁ being RealNormSpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ holds
( ||.(b₃ - b₂).|| is convergent & lim ||.(b₃ - b₂).|| = 0 )

proof end;

theorem Th42: :: NORMSP_1:42

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
lim (b₂ + b₃) = (lim b₂) + (lim b₃)

proof end;

theorem Th43: :: NORMSP_1:43

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
lim (b₂ - b₃) = (lim b₂) - (lim b₃)

proof end;

theorem Th44: :: NORMSP_1:44

for b₁ being RealNormSpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
lim (b₃ - b₂) = (lim b₃) - b₂

proof end;

theorem Th45: :: NORMSP_1:45

for b₁ being Real
for b₂ being RealNormSpace
for b₃ being sequence of b₂ st b₃ is convergent holds
lim (b₁ * b₃) = b₁ * (lim b₃)

proof end;