:: by Andrzej Trybulec

::

:: Received March 23, 2010

:: Copyright (c) 2010-2017 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

end;
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;

definition

attr c_{1} is strict ;

struct N-Str -> 1-sorted ;

aggr N-Str(# carrier, normF #) -> N-Str ;

sel normF c_{1} -> Function of the carrier of c_{1},REAL;

end;
struct N-Str -> 1-sorted ;

aggr N-Str(# carrier, normF #) -> N-Str ;

sel normF c

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
end;

definition
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;

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;

ex b_{1} being Function st

( dom b_{1} = dom f & ( for e being set st e in dom b_{1} holds

b_{1} . e = ||.(f /. e).|| ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for e being set st e in dom b_{1} holds

b_{1} . e = ||.(f /. e).|| ) & dom b_{2} = dom f & ( for e being set st e in dom b_{2} holds

b_{2} . e = ||.(f /. e).|| ) holds

b_{1} = b_{2}

end;
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 ( dom it = dom f & ( for e being set st e in dom it holds

it . e = ||.(f /. e).|| ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines ||. NORMSP_0:def 2 :

for X being non empty N-Str

for f being the carrier of b_{1} -valued Function

for b_{3} being Function holds

( b_{3} = ||.f.|| iff ( dom b_{3} = dom f & ( for e being set st e in dom b_{3} holds

b_{3} . e = ||.(f /. e).|| ) ) );

for X being non empty N-Str

for f being the carrier of b

for b

( b

b

registration

let X be non empty N-Str ;

let f be the carrier of X -valued Function;

coherence

||.f.|| is REAL -valued

end;
let f be the carrier of X -valued Function;

coherence

||.f.|| is REAL -valued

proof 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;

||.f.|| is PartFunc of C,REAL

for b_{1} being PartFunc of C,REAL holds

( b_{1} = ||.f.|| iff ( dom b_{1} = dom f & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = ||.(f /. c).|| ) ) )

end;
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 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).|| ) );

||.f.|| is PartFunc of C,REAL

proof end;

compatibility for b

( b

b

proof 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_{4} being PartFunc of C,REAL holds

( b_{4} = ||.f.|| iff ( dom b_{4} = dom f & ( for c being Element of C st c in dom b_{4} holds

b_{4} . c = ||.(f /. c).|| ) ) );

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

( b

b

definition

let X be non empty N-Str ;

let s be sequence of X;

||.s.|| is Real_Sequence

for b_{1} being Real_Sequence holds

( b_{1} = ||.s.|| iff for n being Nat holds b_{1} . n = ||.(s . n).|| )

end;
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 redefine func ||.s.|| -> Real_Sequence means :: NORMSP_0:def 4

for n being Nat holds it . n = ||.(s . n).||;

||.s.|| is Real_Sequence

proof end;

compatibility for b

( b

proof end;

:: deftheorem defines ||. NORMSP_0:def 4 :

for X being non empty N-Str

for s being sequence of X

for b_{3} being Real_Sequence holds

( b_{3} = ||.s.|| iff for n being Nat holds b_{3} . n = ||.(s . n).|| );

for X being non empty N-Str

for s being sequence of X

for b

( b

definition

attr c_{1} is strict ;

struct N-ZeroStr -> N-Str , ZeroStr ;

aggr N-ZeroStr(# carrier, ZeroF, normF #) -> N-ZeroStr ;

end;
struct N-ZeroStr -> N-Str , ZeroStr ;

aggr N-ZeroStr(# carrier, ZeroF, normF #) -> N-ZeroStr ;

registration
end;

definition

let X be non empty N-ZeroStr ;

end;
attr X is discerning means :: NORMSP_0:def 5

for x being Element of X st ||.x.|| = 0 holds

x = 0. X;

for x being Element of X st ||.x.|| = 0 holds

x = 0. X;

:: 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 );

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 );

for X being non empty N-ZeroStr holds

( X is reflexive iff ||.(0. X).|| = 0 );

registration

existence

ex b_{1} being non empty strict N-ZeroStr st

( b_{1} is reflexive & b_{1} is discerning )

end;
ex b

( b

proof end;

registration

let X be non empty reflexive N-ZeroStr ;

let x be zero Element of X;

coherence

||.x.|| is zero

end;
let x be zero Element of X;

coherence

||.x.|| is zero

proof end;