:: Partial Differentiation, Differentiation and Continuity on $n$-Dimensional Real Normed Linear Spaces
:: by Takao Inou\'e , Adam Naumowicz , Noboru Endou and Yasunari Shidama
::
:: Copyright (c) 2010-2021 Association of Mizar Users

:: Some properties of partial differentiation
:: of PartFunc of REAL-NS m,REAL-NS n
theorem Th1: :: PDIFF_8:1
for n, i being Element of NAT
for q being Element of REAL n
for p being Point of () st i in Seg n & q = p holds
|.(p /. i).| <= |.q.|
proof end;

theorem Th2: :: PDIFF_8:2
for x being Real
for vx being Element of () st vx = <*x*> holds
||.vx.|| = |.x.|
proof end;

theorem Th3: :: PDIFF_8:3
for n being non zero Element of NAT
for x being Point of ()
for i being Nat st 1 <= i & i <= n holds
||.((Proj (i,n)) . x).|| <=
proof end;

theorem Th4: :: PDIFF_8:4
for n being non zero Element of NAT
for x being Element of ()
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.|
proof end;

theorem Th6: :: PDIFF_8:6
for m, n being non zero Element of NAT
for s being Point of ()
for i being Nat st 1 <= i & i <= n holds
( Proj (i,n) is Lipschitzian LinearOperator of (),() & (BoundedLinearOperatorsNorm ((),())) . (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 ()
for i being Nat st 1 <= i & i <= n holds
( (Proj (i,n)) * s is Point of () & (BoundedLinearOperatorsNorm ((),())) . ((Proj (i,n)) * s) <= ((BoundedLinearOperatorsNorm ((),())) . (Proj (i,n))) * ((BoundedLinearOperatorsNorm ((),())) . s) )
proof end;

theorem :: PDIFF_8:8
for n being non zero Element of NAT
for i being Element of NAT holds Proj (i,n) is homogeneous
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)
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)
proof end;

theorem Th11: :: PDIFF_8:11
for n being non zero Element of NAT
for x, y being Point of ()
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)
proof end;

Lm1: for m, n being non zero Element of NAT
for s, t being Point of ()
for i being Nat
for si, ti being Point of () 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 ()
for i being Nat
for si being Point of () st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <=
proof end;

theorem Th14: :: PDIFF_8:14
for m, n being non zero Element of NAT
for s, t being Point of ()
for si, ti being Point of ()
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
proof end;

theorem Th16: :: PDIFF_8:16
for K being Real
for n being non zero Element of NAT
for s being Element of () st ( for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . s).|| <= K ) holds
<= 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
proof end;

theorem Th18: :: PDIFF_8:18
for m, n being non zero Element of NAT
for s being Point of ()
for K being Real st ( for i being Element of NAT
for si being Point of () st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ) holds
<= n * K
proof end;

theorem Th19: :: PDIFF_8:19
for m, n being non zero Element of NAT
for s, t being Point of ()
for K being Real st ( for i being Element of NAT
for si, ti being Point of () 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 (),()
for X being Subset of ()
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 (),()
for X being Subset of () 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 (),()
for X being Subset of () 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;