:: by Takao Inou\'e , Adam Naumowicz , Noboru Endou and Yasunari Shidama

::

:: Received October 13, 2010

:: Copyright (c) 2010-2016 Association of Mizar Users

theorem Th1: :: PDIFF_8:1

for n, i being Element of NAT

for q being Element of REAL n

for p being Point of (TOP-REAL n) st i in Seg n & q = p holds

|.(p /. i).| <= |.q.|

for q being Element of REAL n

for p being Point of (TOP-REAL n) st i in Seg n & q = p holds

|.(p /. i).| <= |.q.|

proof end;

theorem Th3: :: PDIFF_8:3

for n being non zero Element of NAT

for x being Point of (REAL-NS n)

for i being Nat st 1 <= i & i <= n holds

||.((Proj (i,n)) . x).|| <= ||.x.||

for x being Point of (REAL-NS n)

for i being Nat st 1 <= i & i <= n holds

||.((Proj (i,n)) . x).|| <= ||.x.||

proof end;

theorem Th4: :: PDIFF_8:4

for n being non zero Element of NAT

for x being Element of (REAL-NS n)

for i being Element of NAT holds ||.((Proj (i,n)) . x).|| = |.((proj (i,n)) . x).|

for x being Element of (REAL-NS n)

for i being Element of NAT holds ||.((Proj (i,n)) . x).|| = |.((proj (i,n)) . x).|

proof end;

theorem :: PDIFF_8:5

for n being non zero Element of NAT

for x being Element of REAL n

for i being Element of NAT st 1 <= i & i <= n holds

|.((proj (i,n)) . x).| <= |.x.|

for x being Element of REAL n

for i being Element of NAT st 1 <= i & i <= n holds

|.((proj (i,n)) . x).| <= |.x.|

proof end;

theorem Th6: :: PDIFF_8:6

for m, n being non zero Element of NAT

for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))

for i being Nat st 1 <= i & i <= n holds

( Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) & (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1 )

for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))

for i being Nat st 1 <= i & i <= n holds

( Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) & (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1 )

proof end;

theorem Th7: :: PDIFF_8:7

for m, n being non zero Element of NAT

for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))

for i being Nat st 1 <= i & i <= n holds

( (Proj (i,n)) * s is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) & (BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS 1))) . ((Proj (i,n)) * s) <= ((BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n))) * ((BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS n))) . s) )

for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))

for i being Nat st 1 <= i & i <= n holds

( (Proj (i,n)) * s is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) & (BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS 1))) . ((Proj (i,n)) * s) <= ((BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n))) * ((BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS n))) . s) )

proof end;

theorem :: PDIFF_8:9

for n being non zero Element of NAT

for x being Element of REAL n

for r being Real

for i being Element of NAT holds (proj (i,n)) . (r * x) = r * ((proj (i,n)) . x)

for x being Element of REAL n

for r being Real

for i being Element of NAT holds (proj (i,n)) . (r * x) = r * ((proj (i,n)) . x)

proof end;

theorem :: PDIFF_8:10

for n being non zero Element of NAT

for x, y being Element of REAL n

for i being Element of NAT holds (proj (i,n)) . (x + y) = ((proj (i,n)) . x) + ((proj (i,n)) . y)

for x, y being Element of REAL n

for i being Element of NAT holds (proj (i,n)) . (x + y) = ((proj (i,n)) . x) + ((proj (i,n)) . y)

proof end;

theorem Th11: :: PDIFF_8:11

for n being non zero Element of NAT

for x, y being Point of (REAL-NS n)

for i being Nat holds (Proj (i,n)) . (x - y) = ((Proj (i,n)) . x) - ((Proj (i,n)) . y)

for x, y being Point of (REAL-NS n)

for i being Nat holds (Proj (i,n)) . (x - y) = ((Proj (i,n)) . x) - ((Proj (i,n)) . y)

proof end;

theorem :: PDIFF_8:12

for n being non zero Element of NAT

for x, y being Element of REAL n

for i being Element of NAT holds (proj (i,n)) . (x - y) = ((proj (i,n)) . x) - ((proj (i,n)) . y)

for x, y being Element of REAL n

for i being Element of NAT holds (proj (i,n)) . (x - y) = ((proj (i,n)) . x) - ((proj (i,n)) . y)

proof end;

Lm1: for m, n being non zero Element of NAT

for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))

for i being Nat

for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds

si - ti = (Proj (i,n)) * (s - t)

proof end;

theorem Th13: :: PDIFF_8:13

for m, n being non zero Element of NAT

for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))

for i being Nat

for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds

||.si.|| <= ||.s.||

for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))

for i being Nat

for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds

||.si.|| <= ||.s.||

proof end;

theorem Th14: :: PDIFF_8:14

for m, n being non zero Element of NAT

for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))

for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1)))

for i being Nat st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds

||.(si - ti).|| <= ||.(s - t).||

for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))

for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1)))

for i being Nat st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds

||.(si - ti).|| <= ||.(s - t).||

proof end;

theorem Th15: :: PDIFF_8:15

for K being Real

for n being Nat

for s being Element of REAL n st ( for i being Element of NAT st 1 <= i & i <= n holds

|.(s . i).| <= K ) holds

|.s.| <= n * K

for n being Nat

for s being Element of REAL n st ( for i being Element of NAT st 1 <= i & i <= n holds

|.(s . i).| <= K ) holds

|.s.| <= n * K

proof end;

theorem Th16: :: PDIFF_8:16

for K being Real

for n being non zero Element of NAT

for s being Element of (REAL-NS n) st ( for i being Element of NAT st 1 <= i & i <= n holds

||.((Proj (i,n)) . s).|| <= K ) holds

||.s.|| <= n * K

for n being non zero Element of NAT

for s being Element of (REAL-NS n) st ( for i being Element of NAT st 1 <= i & i <= n holds

||.((Proj (i,n)) . s).|| <= K ) holds

||.s.|| <= n * K

proof end;

theorem :: PDIFF_8:17

for K being Real

for n being non zero Element of NAT

for s being Element of REAL n st ( for i being Element of NAT st 1 <= i & i <= n holds

|.((proj (i,n)) . s).| <= K ) holds

|.s.| <= n * K

for n being non zero Element of NAT

for s being Element of REAL n st ( for i being Element of NAT st 1 <= i & i <= n holds

|.((proj (i,n)) . s).| <= K ) holds

|.s.| <= n * K

proof end;

theorem Th18: :: PDIFF_8:18

for m, n being non zero Element of NAT

for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))

for K being Real st ( for i being Element of NAT

for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds

||.si.|| <= K ) holds

||.s.|| <= n * K

for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))

for K being Real st ( for i being Element of NAT

for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds

||.si.|| <= K ) holds

||.s.|| <= n * K

proof end;

theorem Th19: :: PDIFF_8:19

for m, n being non zero Element of NAT

for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))

for K being Real st ( for i being Element of NAT

for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds

||.(si - ti).|| <= K ) holds

||.(s - t).|| <= n * K

for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))

for K being Real st ( for i being Element of NAT

for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds

||.(si - ti).|| <= K ) holds

||.(s - t).|| <= n * K

proof end;

theorem Th20: :: PDIFF_8:20

for m, n being non zero Element of NAT

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for X being Subset of (REAL-NS m)

for i being Nat st 1 <= i & i <= m & X is open holds

( ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) iff for j being Nat st 1 <= j & j <= n holds

( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for X being Subset of (REAL-NS m)

for i being Nat st 1 <= i & i <= m & X is open holds

( ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) iff for j being Nat st 1 <= j & j <= n holds

( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )

proof end;

theorem Th21: :: PDIFF_8:21

for m, n being non zero Element of NAT

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for X being Subset of (REAL-NS m) st X is open holds

( ( f is_differentiable_on X & f `| X is_continuous_on X ) iff for j being Nat st 1 <= j & j <= n holds

( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) )

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for X being Subset of (REAL-NS m) st X is open holds

( ( f is_differentiable_on X & f `| X is_continuous_on X ) iff for j being Nat st 1 <= j & j <= n holds

( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) )

proof end;

theorem :: PDIFF_8:22

for m, n being non zero Element of NAT

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for X being Subset of (REAL-NS m) st X is open holds

( ( for i being Nat st 1 <= i & i <= m holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & f `| X is_continuous_on X ) )

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for X being Subset of (REAL-NS m) st X is open holds

( ( for i being Nat st 1 <= i & i <= m holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & f `| X is_continuous_on X ) )

proof end;

:: of PartFunc of REAL-NS m,REAL-NS n