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

definition

let RNS be non empty 1-sorted ;
let s be sequence of RNS;
let n be Nat;
:: original: .
redefine func s . n -> Element of RNS;
coherence
s . n is Element of RNS

proof end;

end;

definition

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

end;

0 in REAL
by XREAL_0:def 1;

then reconsider f = op1 as Function of {0},REAL by FUNCOP_1:46;

reconsider z = 0 as Element of {0} by TARSKI:def 1;

registration

cluster non empty strict for N-Str ;

existence
ex b₁ being N-Str st
( not b₁ is empty & b₁ 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 b₁ being Function st
( dom b₁ = dom f & ( for e being set st e in dom b₁ holds
b₁ . e = ||.(f /. e).|| ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = dom f & ( for e being set st e in dom b₁ holds
b₁ . e = ||.(f /. e).|| ) & dom b₂ = dom f & ( for e being set st e in dom b₂ holds
b₂ . e = ||.(f /. e).|| ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines ||. NORMSP_0:def 2 :
for X being non empty N-Str
for f being the carrier of b₁ -valued Function
for b₃ being Function holds
( b₃ = ||.f.|| iff ( dom b₃ = dom f & ( for e being set st e in dom b₃ holds
b₃ . 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 b₁ being PartFunc of C,REAL holds
( b₁ = ||.f.|| iff ( dom b₁ = dom f & ( for c being Element of C st c in dom b₁ holds
b₁ . 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 b₄ being PartFunc of C,REAL holds
( b₄ = ||.f.|| iff ( dom b₄ = dom f & ( for c being Element of C st c in dom b₄ holds
b₄ . 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 Nat holds it . n = ||.(s . n).||;

coherence
||.s.|| is Real_Sequence

proof end;

compatibility
for b₁ being Real_Sequence holds
( b₁ = ||.s.|| iff for n being Nat holds b₁ . 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 b₃ being Real_Sequence holds
( b₃ = ||.s.|| iff for n being Nat holds b₃ . n = ||.(s . n).|| );

definition

attr c₁ is strict ;
struct N-ZeroStr -> N-Str , ZeroStr ;
aggr N-ZeroStr(# carrier, ZeroF, normF #) -> N-ZeroStr ;

end;

registration

cluster non empty strict for N-ZeroStr ;

existence
ex b₁ being N-ZeroStr st
( not b₁ is empty & b₁ 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 for N-ZeroStr ;

existence
ex b₁ being non empty strict N-ZeroStr st
( b₁ is reflexive & b₁ is discerning )

proof end;

end;

registration

let X be non empty reflexive N-ZeroStr ;
let x be zero Element of X;

cluster ||.x.|| -> zero ;

coherence
||.x.|| is zero

proof end;

end;