let x0 be Real; for n being non zero Element of NAT
for h being PartFunc of REAL,(REAL n) holds
( h is_continuous_in x0 iff ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) ) )
let n be non zero Element of NAT ; for h being PartFunc of REAL,(REAL n) holds
( h is_continuous_in x0 iff ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) ) )
let h be PartFunc of REAL,(REAL n); ( h is_continuous_in x0 iff ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) ) )
hereby ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) implies h is_continuous_in x0 )
assume A1:
h is_continuous_in x0
;
( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) )hence A2:
x0 in dom h
by Th3;
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0thus
for
i being
Element of
NAT st
i in Seg n holds
(proj (i,n)) * h is_continuous_in x0
verumproof
let i be
Element of
NAT ;
( i in Seg n implies (proj (i,n)) * h is_continuous_in x0 )
assume
i in Seg n
;
(proj (i,n)) * h is_continuous_in x0
then A3:
( 1
<= i &
i <= n )
by FINSEQ_1:1;
A4:
dom (proj (i,n)) = REAL n
by FUNCT_2:def 1;
rng h c= REAL n
;
then A5:
dom ((proj (i,n)) * h) = dom h
by A4, RELAT_1:27;
proj (
i,
n)
is_continuous_in h /. x0
by A3, Th42;
hence
(proj (i,n)) * h is_continuous_in x0
by A5, A1, A2, Th22;
verum
end;
end;
assume A6:
( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) )
; h is_continuous_in x0
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x0).| < s holds
|.((h /. x1) - (h /. x0)).| < r ) )
proof
let r0 be
Real;
( 0 < r0 implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x0).| < s holds
|.((h /. x1) - (h /. x0)).| < r0 ) ) )
assume A7:
0 < r0
;
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x0).| < s holds
|.((h /. x1) - (h /. x0)).| < r0 ) )
set r =
r0 / 2;
A8:
0 < r0 / 2
by A7, XREAL_1:215;
defpred S1[
Nat,
Real]
means (
0 < $2 & ( for
x1 being
Real st
x1 in dom h &
|.(x1 - x0).| < $2 holds
|.((((proj ($1,n)) * h) . x1) - (((proj ($1,n)) * h) . x0)).| < (r0 / 2) / n ) );
A9:
0 < (r0 / 2) / n
by A8, XREAL_1:139;
A10:
for
j being
Nat st
j in Seg n holds
ex
x being
Element of
REAL st
S1[
j,
x]
proof
let j be
Nat;
( j in Seg n implies ex x being Element of REAL st S1[j,x] )
assume A11:
j in Seg n
;
ex x being Element of REAL st S1[j,x]
A12:
(proj (j,n)) * h is_continuous_in x0
by A6, A11;
A13:
dom (proj (j,n)) = REAL n
by FUNCT_2:def 1;
rng h c= REAL n
;
then A14:
dom ((proj (j,n)) * h) = dom h
by A13, RELAT_1:27;
consider sj being
Real such that A15:
(
0 < sj & ( for
x1 being
Real st
x1 in dom ((proj (j,n)) * h) &
|.(x1 - x0).| < sj holds
|.((((proj (j,n)) * h) . x1) - (((proj (j,n)) * h) . x0)).| < (r0 / 2) / n ) )
by A12, A9, FCONT_1:3;
sj in REAL
by XREAL_0:def 1;
hence
ex
x being
Element of
REAL st
S1[
j,
x]
by A15, A14;
verum
end;
consider s0 being
FinSequence of
REAL such that A16:
(
dom s0 = Seg n & ( for
k being
Nat st
k in Seg n holds
S1[
k,
s0 . k] ) )
from FINSEQ_1:sch 5(A10);
n in Seg n
by FINSEQ_1:3;
then reconsider rs0 =
rng s0 as non
empty ext-real-membered set by A16, FUNCT_1:3;
rng s0 is
finite
by A16, FINSET_1:8;
then reconsider rs0 =
rs0 as non
empty ext-real-membered left_end right_end set ;
A17:
min rs0 in rng s0
by XXREAL_2:def 7;
reconsider s =
min rs0 as
Real ;
take
s
;
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x0).| < s holds
|.((h /. x1) - (h /. x0)).| < r0 ) )
ex
i1 being
object st
(
i1 in dom s0 &
s = s0 . i1 )
by A17, FUNCT_1:def 3;
hence
0 < s
by A16;
for x1 being Real st x1 in dom h & |.(x1 - x0).| < s holds
|.((h /. x1) - (h /. x0)).| < r0
now for x1 being Real st x1 in dom h & |.(x1 - x0).| < s holds
|.((h /. x1) - (h /. x0)).| < r0let x1 be
Real;
( x1 in dom h & |.(x1 - x0).| < s implies |.((h /. x1) - (h /. x0)).| < r0 )assume A18:
(
x1 in dom h &
|.(x1 - x0).| < s )
;
|.((h /. x1) - (h /. x0)).| < r0now for j being Element of NAT st 1 <= j & j <= n holds
|.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / nlet j be
Element of
NAT ;
( 1 <= j & j <= n implies |.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n )assume
( 1
<= j &
j <= n )
;
|.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / nthen A19:
j in Seg n
by FINSEQ_1:1;
then
s0 . j in rng s0
by A16, FUNCT_1:3;
then
s <= s0 . j
by XXREAL_2:def 7;
then
|.(x1 - x0).| < s0 . j
by A18, XXREAL_0:2;
then A20:
|.((((proj (j,n)) * h) . x1) - (((proj (j,n)) * h) . x0)).| < (r0 / 2) / n
by A19, A18, A16;
A21:
((proj (j,n)) * h) . x1 =
(proj (j,n)) . (h . x1)
by A18, FUNCT_1:13
.=
(proj (j,n)) . (h /. x1)
by A18, PARTFUN1:def 6
;
((proj (j,n)) * h) . x0 =
(proj (j,n)) . (h . x0)
by A6, FUNCT_1:13
.=
(proj (j,n)) . (h /. x0)
by A6, PARTFUN1:def 6
;
hence
|.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n
by A20, A21, PDIFF_8:12;
verum end; then
|.((h /. x1) - (h /. x0)).| <= n * ((r0 / 2) / n)
by PDIFF_8:17;
then A22:
|.((h /. x1) - (h /. x0)).| <= r0 / 2
by XCMPLX_1:87;
r0 / 2
< r0
by A7, XREAL_1:216;
hence
|.((h /. x1) - (h /. x0)).| < r0
by A22, XXREAL_0:2;
verum end;
hence
for
x1 being
Real st
x1 in dom h &
|.(x1 - x0).| < s holds
|.((h /. x1) - (h /. x0)).| < r0
;
verum
end;
hence
h is_continuous_in x0
by A6, Th3; verum