:: Preliminaries to Normed Spaces
:: by Andrzej Trybulec
::
:: Received March 23, 2010
:: Copyright (c) 2010 Association of Mizar Users


begin

definition
attr c1 is strict ;
struct N-Str -> 1-sorted ;
aggr N-Str(# carrier, normF #) -> N-Str ;
sel normF c1 -> Function of the carrier of c1,REAL;
end;

op1 = 1 --> 0
by CARD_1:87;

then reconsider f = op1 as Function of 1,REAL by FUNCOP_1:58;

reconsider z = 0 as Element of 1 by CARD_1:87, TARSKI:def 1;

registration
cluster non empty strict N-Str ;
existence
ex b1 being N-Str st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let X be non empty N-Str ;
let x be Element of X;
func ||.x.|| -> Real equals :: NORMSP_0:def 1
 the normF of X . x;
coherence
the normF of X . x is Real ;
end;

:: deftheorem defines ||. NORMSP_0:def 1 :
for X being non empty N-Str
for x being Element of X holds ||.x.|| = the normF of X . x;

definition
let X be non empty N-Str ;
let f be the carrier of X -valued Function;
func ||.f.|| -> Function means :Def2: :: NORMSP_0:def 2
( dom it = dom f & ( for e being set st e in dom it holds
it . e = ||.(f /. e).|| ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for e being set st e in dom b1 holds
b1 . e = ||.(f /. e).|| ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for e being set st e in dom b1 holds
b1 . e = ||.(f /. e).|| ) & dom b2 = dom f & ( for e being set st e in dom b2 holds
b2 . e = ||.(f /. e).|| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ||. NORMSP_0:def 2 :
for X being non empty N-Str
for f being the carrier of b1 -valued Function
for b3 being Function holds
( b3 = ||.f.|| iff ( dom b3 = dom f & ( for e being set st e in dom b3 holds
b3 . e = ||.(f /. e).|| ) ) );

registration
let X be non empty N-Str ;
let f be the carrier of X -valued Function;
cluster ||.f.|| -> REAL -valued ;
coherence
||.f.|| is REAL -valued
proof end;
end;

definition
let C be non empty set ;
let X be non empty N-Str ;
let f be PartFunc of C, the carrier of X;
:: original: ||.
redefine func ||.f.|| -> PartFunc of C,REAL means :: NORMSP_0:def 3
( dom it = dom f & ( for c being Element of C st c in dom it holds
it . c = ||.(f /. c).|| ) );
coherence
||.f.|| is PartFunc of C,REAL
proof end;
compatibility
for b1 being PartFunc of C,REAL holds
( b1 = ||.f.|| iff ( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 . c = ||.(f /. c).|| ) ) )
proof end;
end;

:: deftheorem defines ||. NORMSP_0:def 3 :
for C being non empty set
for X being non empty N-Str
for f being PartFunc of C, the carrier of X
for b4 being PartFunc of C,REAL holds
( b4 = ||.f.|| iff ( dom b4 = dom f & ( for c being Element of C st c in dom b4 holds
b4 . c = ||.(f /. c).|| ) ) );

definition
let X be non empty N-Str ;
let s be sequence of X;
:: original: ||.
redefine func ||.s.|| -> Real_Sequence means :: NORMSP_0:def 4
 for n being Element of NAT holds it . n = ||.(s . n).||;
coherence
||.s.|| is Real_Sequence
proof end;
compatibility
for b1 being Real_Sequence holds
( b1 = ||.s.|| iff for n being Element of NAT holds b1 . n = ||.(s . n).|| )
proof end;
end;

:: deftheorem defines ||. NORMSP_0:def 4 :
for X being non empty N-Str
for s being sequence of X
for b3 being Real_Sequence holds
( b3 = ||.s.|| iff for n being Element of NAT holds b3 . n = ||.(s . n).|| );

definition
attr c1 is strict ;
struct N-ZeroStr -> N-Str , ZeroStr ;
aggr N-ZeroStr(# carrier, ZeroF, normF #) -> N-ZeroStr ;
end;

registration
cluster non empty strict N-ZeroStr ;
existence
ex b1 being N-ZeroStr st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let X be non empty N-ZeroStr ;
attr X is discerning means :: NORMSP_0:def 5
 for x being Element of X st ||.x.|| = 0 holds
x = 0. X;
attr X is reflexive means :Def6: :: NORMSP_0:def 6
||.(0. X).|| = 0 ;
end;

:: deftheorem defines discerning NORMSP_0:def 5 :
for X being non empty N-ZeroStr holds
( X is discerning iff for x being Element of X st ||.x.|| = 0 holds
x = 0. X );

:: deftheorem Def6 defines reflexive NORMSP_0:def 6 :
for X being non empty N-ZeroStr holds
( X is reflexive iff ||.(0. X).|| = 0 );

registration
cluster non empty strict discerning reflexive N-ZeroStr ;
existence
ex b1 being non empty strict N-ZeroStr st
( b1 is reflexive & b1 is discerning )
proof end;
end;

registration
let X be non empty reflexive N-ZeroStr ;
cluster ||.(0. X).|| -> zero ;
coherence
||.(0. X).|| is empty by Def6;
end;