environ
vocabularies HIDDEN, NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1, FUNCT_4, NAT_1, FDIFF_1, SUBSET_1, SEQ_4, RELAT_1, LOPBAN_1, RCOMP_1, TARSKI, ARYTM_3, FUNCT_7, VALUED_1, FUNCT_2, ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1, STRUCT_0, CARD_1, VALUED_0, XXREAL_0, GROUP_2, FUNCOP_1, XBOOLE_0, CARD_3, FINSEQ_1, RLVECT_1, PDIFF_1, PRVECT_1, PRVECT_2, CFCONT_1, VECTMETR, NDIFF_7, MCART_1;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, FUNCT_4, CARD_1, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, MEMBERED, VALUED_0, COMPLEX1, NAT_D, XXREAL_2, FINSEQ_1, FINSEQ_2, VALUED_1, SEQ_2, RVSUM_1, RFINSEQ, SEQ_4, RCOMP_1, FCONT_1, FDIFF_1, RFINSEQ2, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, NORMSP_0, NORMSP_1, VFUNCT_1, MONOID_0, RLTOPSP1, EUCLID, LOPBAN_1, PRVECT_1, NFCONT_1, NDIFF_1, MAZURULM, NDIFF_2, PRVECT_2, NFCONT_3, PRVECT_3, NDIFF_3, FUNCT_7, NDIFF_5;
definitions ;
theorems TARSKI, XBOOLE_0, XBOOLE_1, RLVECT_1, ZFMISC_1, RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2, ORDINAL1, FINSEQ_1, FUNCT_4, LOPBAN_1, PARTFUN1, PARTFUN2, NFCONT_1, NDIFF_1, FUNCOP_1, VALUED_0, VECTSP_1, XREAL_0, BINOP_1, PRVECT_2, NDIFF_2, PRVECT_3, FUNCT_7, NDIFF_5, SUBSET_1;
schemes FUNCT_2, SEQ_1;
registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, NDIFF_1, FUNCT_2, NUMBERS, XBOOLE_0, PRVECT_2, FINSEQ_1, RELAT_1, MAZURULM, LOPBAN_1, PRVECT_3, FUNCOP_1, VALUED_1, XTUPLE_0, FUNCT_7;
constructors HIDDEN, REAL_1, SQUARE_1, SEQ_2, FDIFF_1, NFCONT_1, RSSPACE, VFUNCT_1, NDIFF_1, RELSET_1, FINSEQ_7, NAT_D, RFINSEQ2, SEQ_4, FCONT_1, NFCONT_3, NDIFF_3, FUNCT_4, NDIFF_5, PRVECT_3, NDIFF_2, MAZURULM, LOPBAN_1, DOMAIN_1, RCOMP_1;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities MAZURULM, RLVECT_1, LOPBAN_1, FINSEQ_1, NDIFF_2, NORMSP_0, BINOP_1, SUBSET_1, PRVECT_3, NDIFF_5;
expansions MAZURULM, TARSKI, FUNCT_2, LOPBAN_1, NDIFF_1, NDIFF_5;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
definition
let X,
Y be
RealNormSpace;
let x be
Element of
[:X,Y:];
existence
ex b1 being Function of X,[:X,Y:] st
for r being Element of X holds b1 . r = [r,(x `2)]
uniqueness
for b1, b2 being Function of X,[:X,Y:] st ( for r being Element of X holds b1 . r = [r,(x `2)] ) & ( for r being Element of X holds b2 . r = [r,(x `2)] ) holds
b1 = b2
existence
ex b1 being Function of Y,[:X,Y:] st
for r being Element of Y holds b1 . r = [(x `1),r]
uniqueness
for b1, b2 being Function of Y,[:X,Y:] st ( for r being Element of Y holds b1 . r = [(x `1),r] ) & ( for r being Element of Y holds b2 . r = [(x `1),r] ) holds
b1 = b2
end;
LM023:
for S, T being RealNormSpace
for I being LinearOperator of S,T
for Z being Subset of S st I is one-to-one & I is onto & I is isometric & Z is closed holds
I .: Z is closed
LM026:
for S, T being RealNormSpace
for I being LinearOperator of S,T
for Z being Subset of S st I is isometric & Z is compact holds
I .: Z is compact
definition
let X,
Y be
RealNormSpace;
existence
ex b1 being LinearOperator of [:X,Y:],(product <*X,Y*>) st
for x being Point of X
for y being Point of Y holds b1 . (x,y) = <*x,y*>
uniqueness
for b1, b2 being LinearOperator of [:X,Y:],(product <*X,Y*>) st ( for x being Point of X
for y being Point of Y holds b1 . (x,y) = <*x,y*> ) & ( for x being Point of X
for y being Point of Y holds b2 . (x,y) = <*x,y*> ) holds
b1 = b2
end;
registration
let X,
Y be
RealNormSpace;
cluster Relation-like the
carrier of
[:X,Y:] -defined the
carrier of
(product <*X,Y*>) -valued non
empty Function-like one-to-one total quasi_total onto V152(
[:X,Y:],
product <*X,Y*>)
V153(
[:X,Y:],
product <*X,Y*>)
isometric for
Element of
bool [: the carrier of [:X,Y:], the carrier of (product <*X,Y*>):];
correctness
existence
ex b1 being LinearOperator of [:X,Y:],(product <*X,Y*>) st
( b1 is one-to-one & b1 is onto & b1 is isometric );
end;
definition
let X,
Y be
RealNormSpace;
let f be
one-to-one onto isometric LinearOperator of
[:X,Y:],
(product <*X,Y*>);
"redefine func f " -> LinearOperator of
(product <*X,Y*>),
[:X,Y:];
correctness
coherence
f " is LinearOperator of (product <*X,Y*>),[:X,Y:];
end;
registration
let X,
Y be
RealNormSpace;
cluster Relation-like the
carrier of
(product <*X,Y*>) -defined the
carrier of
[:X,Y:] -valued non
empty Function-like one-to-one total quasi_total onto V152(
product <*X,Y*>,
[:X,Y:])
V153(
product <*X,Y*>,
[:X,Y:])
isometric for
Element of
bool [: the carrier of (product <*X,Y*>), the carrier of [:X,Y:]:];
correctness
existence
ex b1 being LinearOperator of (product <*X,Y*>),[:X,Y:] st
( b1 is one-to-one & b1 is onto & b1 is isometric );
end;
theorem
for
W,
X,
Y being
RealNormSpace for
f being
PartFunc of
(product <*X,Y*>),
W for
D being
Subset of
(product <*X,Y*>) st
f is_differentiable_on D holds
for
z being
Point of
(product <*X,Y*>) st
z in dom (f `| D) holds
(f `| D) . z = (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. (((IsoCPNrSP (X,Y)) ") . z)) * ((IsoCPNrSP (X,Y)) ")
theorem LM166:
for
W,
X,
Y being
RealNormSpace for
f being
PartFunc of
[:X,Y:],
W for
D being
Subset of
[:X,Y:] st
f is_differentiable_on D holds
for
z being
Point of
[:X,Y:] st
z in dom (f `| D) holds
(f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ")
theorem LM180:
for
X,
Y being
RealNormSpace for
z being
Point of
[:X,Y:] holds
(
reproj1 z = ((IsoCPNrSP (X,Y)) ") * (reproj ((In (1,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z))) &
reproj2 z = ((IsoCPNrSP (X,Y)) ") * (reproj ((In (2,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z))) )
theorem LM200:
for
X,
Y,
W being
RealNormSpace for
z being
Point of
[:X,Y:] for
f being
PartFunc of
[:X,Y:],
W holds
( (
f is_partial_differentiable_in`1 z implies
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 ) & (
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 implies
f is_partial_differentiable_in`1 z ) & (
f is_partial_differentiable_in`2 z implies
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 ) & (
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 implies
f is_partial_differentiable_in`2 z ) )
theorem LM210:
for
X,
Y,
W being
RealNormSpace for
z being
Point of
[:X,Y:] for
f being
PartFunc of
[:X,Y:],
W holds
(
partdiff`1 (
f,
z)
= partdiff (
(f * ((IsoCPNrSP (X,Y)) ")),
((IsoCPNrSP (X,Y)) . z),1) &
partdiff`2 (
f,
z)
= partdiff (
(f * ((IsoCPNrSP (X,Y)) ")),
((IsoCPNrSP (X,Y)) . z),2) )
theorem LM215:
for
X,
Y,
W being
RealNormSpace for
z being
Point of
[:X,Y:] for
f1,
f2 being
PartFunc of
[:X,Y:],
W st
f1 is_partial_differentiable_in`1 z &
f2 is_partial_differentiable_in`1 z holds
(
f1 + f2 is_partial_differentiable_in`1 z &
partdiff`1 (
(f1 + f2),
z)
= (partdiff`1 (f1,z)) + (partdiff`1 (f2,z)) &
f1 - f2 is_partial_differentiable_in`1 z &
partdiff`1 (
(f1 - f2),
z)
= (partdiff`1 (f1,z)) - (partdiff`1 (f2,z)) )
theorem LM216:
for
X,
Y,
W being
RealNormSpace for
z being
Point of
[:X,Y:] for
f1,
f2 being
PartFunc of
[:X,Y:],
W st
f1 is_partial_differentiable_in`2 z &
f2 is_partial_differentiable_in`2 z holds
(
f1 + f2 is_partial_differentiable_in`2 z &
partdiff`2 (
(f1 + f2),
z)
= (partdiff`2 (f1,z)) + (partdiff`2 (f2,z)) &
f1 - f2 is_partial_differentiable_in`2 z &
partdiff`2 (
(f1 - f2),
z)
= (partdiff`2 (f1,z)) - (partdiff`2 (f2,z)) )
theorem LM300:
for
X,
Y,
W being
RealNormSpace for
Z being
Subset of
[:X,Y:] for
f being
PartFunc of
[:X,Y:],
W holds
( (
f is_partial_differentiable_on`1 Z implies
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 ) & (
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 implies
f is_partial_differentiable_on`1 Z ) & (
f is_partial_differentiable_on`2 Z implies
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 ) & (
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 implies
f is_partial_differentiable_on`2 Z ) )
definition
let X,
Y,
W be
RealNormSpace;
let Z be
set ;
let f be
PartFunc of
[:X,Y:],
W;
assume A2:
f is_partial_differentiable_on`1 Z
;
existence
ex b1 being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)) st
( dom b1 = Z & ( for z being Point of [:X,Y:] st z in Z holds
b1 /. z = partdiff`1 (f,z) ) )
uniqueness
for b1, b2 being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)) st dom b1 = Z & ( for z being Point of [:X,Y:] st z in Z holds
b1 /. z = partdiff`1 (f,z) ) & dom b2 = Z & ( for z being Point of [:X,Y:] st z in Z holds
b2 /. z = partdiff`1 (f,z) ) holds
b1 = b2
end;
definition
let X,
Y,
W be
RealNormSpace;
let Z be
set ;
let f be
PartFunc of
[:X,Y:],
W;
assume A2:
f is_partial_differentiable_on`2 Z
;
existence
ex b1 being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (Y,W)) st
( dom b1 = Z & ( for z being Point of [:X,Y:] st z in Z holds
b1 /. z = partdiff`2 (f,z) ) )
uniqueness
for b1, b2 being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (Y,W)) st dom b1 = Z & ( for z being Point of [:X,Y:] st z in Z holds
b1 /. z = partdiff`2 (f,z) ) & dom b2 = Z & ( for z being Point of [:X,Y:] st z in Z holds
b2 /. z = partdiff`2 (f,z) ) holds
b1 = b2
end;