NORMSP

:: NORMSP_0 semantic presentation

definition

attr c₁ is strict ;
struct N-Str -> ( ( ) ( ) 1-sorted ) ;
aggr N-Str(# carrier, normF #) -> ( ( strict ) ( strict ) N-Str ) ;
sel normF c₁ -> ( ( Function-like V18( the carrier of c₁ : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V28() ) set ) ) ) ( Relation-like the carrier of c₁ : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V28() ) set ) -valued Function-like total V18( the carrier of c₁ : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V28() ) set ) ) ) Function of the carrier of c₁ : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V28() ) set ) ) ;

end;

registration

cluster non empty strict for ( ( ) ( ) N-Str ) ;

end;

definition

let X be ( ( non empty ) ( non empty ) N-Str ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

func ||.x.|| -> ( ( ) ( complex ) Real) equals :: NORMSP_0:def 1
the normF of X : ( ( ) ( ) 2-sorted ) : ( ( Function-like V18( the carrier of X : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V28() ) set ) ) ) ( Relation-like the carrier of X : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V28() ) set ) -valued Function-like total V18( the carrier of X : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V28() ) set ) ) ) Function of the carrier of X : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V28() ) set ) ) . x : ( ( ) ( ) set ) : ( ( ) ( complex ) Element of REAL : ( ( ) ( non empty V28() ) set ) ) ;

end;

definition

let X be ( ( non empty ) ( non empty ) N-Str ) ;
let f be ( ( Relation-like the carrier of X : ( ( non empty ) ( non empty ) N-Str ) : ( ( ) ( non empty ) set ) -valued Function-like ) ( Relation-like the carrier of X : ( ( non empty ) ( non empty ) N-Str ) : ( ( ) ( non empty ) set ) -valued Function-like ) Function) ;

func ||.f.|| -> ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) means :: NORMSP_0:def 2
( dom it : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : ( ( ) ( ) set ) = dom f : ( ( ) ( ) set ) : ( ( ) ( ) set ) & ( for e being ( ( ) ( ) set ) st e : ( ( ) ( ) set ) in dom it : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : ( ( ) ( ) set ) holds
it : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) . e : ( ( ) ( ) set ) : ( ( ) ( ) set ) = ||.(f : ( ( ) ( ) set ) /. e : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( complex ) Real) ) );

end;

registration

cluster ||.f : ( ( Relation-like the carrier of X : ( ( non empty ) ( non empty ) N-Str ) : ( ( ) ( non empty ) set ) -valued Function-like ) ( Relation-like the carrier of X : ( ( non empty ) ( non empty ) N-Str ) : ( ( ) ( non empty ) set ) -valued Function-like ) set ) .|| : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) -> Relation-like REAL : ( ( ) ( non empty V28() ) set ) -valued Function-like ;

end;

definition

let C be ( ( non empty ) ( non empty ) set ) ;
let X be ( ( non empty ) ( non empty ) N-Str ) ;
let f be ( ( Function-like ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined the carrier of X : ( ( non empty ) ( non empty ) N-Str ) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ;

:: original: ||.
redefine func ||.f.|| -> ( ( Function-like ) ( Relation-like C : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V28() ) set ) -valued Function-like ) PartFunc of ,) means :: NORMSP_0:def 3
( dom it : ( ( Function-like V18(C : ( ( ) ( ) set ) ,K78(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty ) M4(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) )) ) ) ( Relation-like C : ( ( ) ( ) set ) -defined K78(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty ) M4(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) )) -valued Function-like non empty total V18(C : ( ( ) ( ) set ) ,K78(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty ) M4(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) )) ) Function-yielding V52() ) Element of K19(K20(C : ( ( ) ( ) set ) ,K78(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty ) M4(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = dom f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) & ( for c being ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) st c : ( ( ) ( ) Element of C : ( ( non empty ) ( non empty ) set ) ) in dom it : ( ( Function-like V18(C : ( ( ) ( ) set ) ,K78(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty ) M4(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) )) ) ) ( Relation-like C : ( ( ) ( ) set ) -defined K78(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty ) M4(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) )) -valued Function-like non empty total V18(C : ( ( ) ( ) set ) ,K78(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty ) M4(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) )) ) Function-yielding V52() ) Element of K19(K20(C : ( ( ) ( ) set ) ,K78(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty ) M4(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) holds
it : ( ( Function-like V18(C : ( ( ) ( ) set ) ,K78(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty ) M4(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) )) ) ) ( Relation-like C : ( ( ) ( ) set ) -defined K78(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty ) M4(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) )) -valued Function-like non empty total V18(C : ( ( ) ( ) set ) ,K78(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty ) M4(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) )) ) Function-yielding V52() ) Element of K19(K20(C : ( ( ) ( ) set ) ,K78(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) ) : ( ( ) ( functional non empty ) M4(X : ( ( ) ( ) set ) ,f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . c : ( ( ) ( ) Element of C : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( Relation-like Function-like ) set ) = ||.(f : ( ( ) ( ) Element of C : ( ( ) ( ) set ) ) /. c : ( ( ) ( ) Element of C : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( complex ) Real) ) );

end;

definition

let X be ( ( non empty ) ( non empty ) N-Str ) ;
let s be ( ( Function-like V18( NAT : ( ( ) ( non empty V21() V22() V23() ) Element of K19(REAL : ( ( ) ( non empty V28() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty ) ( non empty ) N-Str ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty V21() V22() V23() ) Element of K19(REAL : ( ( ) ( non empty V28() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of X : ( ( non empty ) ( non empty ) N-Str ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty V21() V22() V23() ) Element of K19(REAL : ( ( ) ( non empty V28() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty ) ( non empty ) N-Str ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;

:: original: ||.
redefine func ||.s.|| -> ( ( Function-like V18( NAT : ( ( ) ( non empty V21() V22() V23() ) Element of K19(REAL : ( ( ) ( non empty V28() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V28() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty V21() V22() V23() ) Element of K19(REAL : ( ( ) ( non empty V28() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V28() ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty V21() V22() V23() ) Element of K19(REAL : ( ( ) ( non empty V28() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V28() ) set ) ) ) Real_Sequence) means :: NORMSP_0:def 4
for n being ( ( ) ( V21() V22() V23() V27() complex ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of K19(REAL : ( ( ) ( non empty V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds it : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . n : ( ( ) ( V21() V22() V23() V27() complex ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of K19(REAL : ( ( ) ( non empty V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of REAL : ( ( ) ( non empty V28() ) set ) ) = ||.(s : ( ( ) ( ) set ) . n : ( ( ) ( V21() V22() V23() V27() complex ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of K19(REAL : ( ( ) ( non empty V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( complex ) Real) ;

end;

definition

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

end;

registration

cluster non empty strict for ( ( ) ( ) N-ZeroStr ) ;

end;

definition

let X be ( ( non empty ) ( non empty ) N-ZeroStr ) ;

attr X is discerning means :: NORMSP_0:def 5
for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st ||.x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex ) Real) = 0 : ( ( ) ( Function-like functional empty V21() V22() V23() V25() V26() V27() complex ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of K19(REAL : ( ( ) ( non empty V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. X : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

attr X is reflexive means :: NORMSP_0:def 6
||.(0. X : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( complex ) Real) = 0 : ( ( ) ( Function-like functional empty V21() V22() V23() V25() V26() V27() complex ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of K19(REAL : ( ( ) ( non empty V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;

end;

registration

cluster non empty strict discerning reflexive for ( ( ) ( ) N-ZeroStr ) ;

end;

registration

let X be ( ( non empty reflexive ) ( non empty reflexive ) N-ZeroStr ) ;

cluster ||.(0. X : ( ( non empty reflexive ) ( non empty reflexive ) N-ZeroStr ) ) : ( ( ) ( zero ) Element of the carrier of X : ( ( non empty reflexive ) ( non empty reflexive ) N-ZeroStr ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( complex ) Real) -> zero ;

end;