let m be non zero Element of NAT ; for I being non empty FinSequence of NAT
for X being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for d being Real st X is open & f = X --> d & rng I c= Seg m holds
( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X )
let I be non empty FinSequence of NAT ; for X being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for d being Real st X is open & f = X --> d & rng I c= Seg m holds
( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X )
let X be non empty Subset of (REAL m); for f being PartFunc of (REAL m),REAL
for d being Real st X is open & f = X --> d & rng I c= Seg m holds
( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X )
let f be PartFunc of (REAL m),REAL; for d being Real st X is open & f = X --> d & rng I c= Seg m holds
( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X )
let d be Real; ( X is open & f = X --> d & rng I c= Seg m implies ( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X ) )
assume A1:
( X is open & f = X --> d & rng I c= Seg m )
; ( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X )
for i being Element of NAT st i <= (len I) - 1 holds
(PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1)
proof
let i be
Element of
NAT ;
( i <= (len I) - 1 implies (PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1) )
assume A2:
i <= (len I) - 1
;
(PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1)
(len I) - 1
<= (len I) - 0
by XREAL_1:10;
then A3:
i <= len I
by A2, XXREAL_0:2;
per cases
( i = 0 or i <> 0 )
;
suppose
i = 0
;
(PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1)then A4:
(PartDiffSeq (f,X,I)) . i = X --> d
by A1, Th17;
( 1
<= I /. (i + 1) &
I /. (i + 1) <= m )
by Lm1, A1, A2;
hence
(PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,
I /. (i + 1)
by A4, A1, Th15;
verum end; suppose
i <> 0
;
(PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1)then
1
<= i
by NAT_1:14;
then A5:
(PartDiffSeq (f,X,I)) . i = X --> 0
by A1, A3, Th17;
( 1
<= I /. (i + 1) &
I /. (i + 1) <= m )
by Lm1, A1, A2;
hence
(PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,
I /. (i + 1)
by A5, A1, Th15;
verum end; end;
end;
hence
f is_partial_differentiable_on X,I
; f `partial| (X,I) is_continuous_on X
reconsider k = (len I) - 1 as Element of NAT by INT_1:5, FINSEQ_1:20;
A6:
f `partial| (X,I) = ((PartDiffSeq (f,X,I)) . k) `partial| (X,(I /. (k + 1)))
by PDIFF_9:def 7;
A7:
(len I) - 1 <= (len I) - 0
by XREAL_1:10;