let T be non empty TopSpace; ( T is normal implies for A being closed Subset of T
for f being Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) st f is continuous holds
ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f )
assume A1:
T is normal
; for A being closed Subset of T
for f being Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) st f is continuous holds
ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f
let A be closed Subset of T; for f being Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) st f is continuous holds
ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f
let f be Function of (T | A),(Closed-Interval-TSpace ((- 1),1)); ( f is continuous implies ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f )
assume A2:
f is continuous
; ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f
A3:
the carrier of (T | A) = A
by PRE_TOPC:8;
A4:
the carrier of (Closed-Interval-TSpace ((- 1),1)) = [.(- 1),1.]
by TOPMETR:18;
per cases
( A is empty or not A is empty )
;
suppose
not
A is
empty
;
ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = fthen reconsider A1 =
A as non
empty Subset of
T ;
set DF =
Funcs ( the
carrier of
T, the
carrier of
R^1);
set D =
{ q where q is Element of Funcs ( the carrier of T, the carrier of R^1) : q is continuous Function of T,R^1 } ;
reconsider f1 =
f as
Function of
(T | A1),
R^1 by TOPREALA:7;
defpred S1[
Nat,
set ,
set ]
means ex
E2 being
continuous Function of
T,
R^1 st
(
E2 = $2 & (
f - E2,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ $1) implies ex
g being
continuous Function of
T,
R^1 st
( $3
= E2 + g &
g, the
carrier of
T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ ($1 + 1)) &
(f - E2) - g,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ ($1 + 1)) ) ) );
A6:
2
/ 3
> 0
;
f1 is
continuous
by A2, PRE_TOPC:26;
then reconsider f1 =
f as
continuous Function of
(T | A1),
R^1 ;
T --> (R^1 0) is
Element of
Funcs ( the
carrier of
T, the
carrier of
R^1)
by FUNCT_2:8;
then
T --> (R^1 0) in { q where q is Element of Funcs ( the carrier of T, the carrier of R^1) : q is continuous Function of T,R^1 }
;
then reconsider D =
{ q where q is Element of Funcs ( the carrier of T, the carrier of R^1) : q is continuous Function of T,R^1 } as non
empty set ;
f1,
A is_absolutely_bounded_by 1
then consider g0 being
continuous Function of
T,
R^1 such that A8:
g0,
dom g0 is_absolutely_bounded_by 1
/ 3
and A9:
f1 - g0,
A is_absolutely_bounded_by (2 * 1) / 3
by A1, Th17;
g0 in Funcs ( the
carrier of
T, the
carrier of
R^1)
by FUNCT_2:8;
then
g0 in D
;
then reconsider g0d =
g0 as
Element of
D ;
A10:
for
n being
Nat for
x being
Element of
D ex
y being
Element of
D st
S1[
n,
x,
y]
proof
let n be
Nat;
for x being Element of D ex y being Element of D st S1[n,x,y]let x be
Element of
D;
ex y being Element of D st S1[n,x,y]
x in D
;
then consider E2 being
Element of
Funcs ( the
carrier of
T, the
carrier of
R^1)
such that A11:
E2 = x
and A12:
E2 is
continuous Function of
T,
R^1
;
reconsider E2 =
E2 as
continuous Function of
T,
R^1 by A12;
per cases
( not f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) or f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) )
;
suppose A13:
not
f - E2,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n)
;
ex y being Element of D st S1[n,x,y]take
x
;
S1[n,x,x]take
E2
;
( E2 = x & ( f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) implies ex g being continuous Function of T,R^1 st
( x = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) ) ) )thus
(
E2 = x & (
f - E2,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) implies ex
g being
continuous Function of
T,
R^1 st
(
x = E2 + g &
g, the
carrier of
T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) &
(f - E2) - g,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) ) ) )
by A11, A13;
verum end; suppose A14:
f - E2,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n)
;
ex y being Element of D st S1[n,x,y]reconsider E2b =
E2 | A as
Function of
(T | A1),
R^1 by PRE_TOPC:9;
reconsider E2b =
E2b as
continuous Function of
(T | A1),
R^1 by TOPMETR:7;
E2b c= E2
by RELAT_1:59;
then A15:
f - E2b,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n)
by A14, Th2, Th15;
set r =
(2 / 3) * ((2 / 3) |^ n);
reconsider f1c =
f1,
E2c =
E2b as
continuous RealMap of
(T | A1) by JORDAN5A:27, TOPMETR:17;
set k =
f1 - E2b;
reconsider E2a =
E2 as
RealMap of
T by TOPMETR:17;
reconsider E2a =
E2a as
continuous RealMap of
T by JORDAN5A:27;
f1c - E2c is
continuous RealMap of
(T | A1)
;
then reconsider k =
f1 - E2b as
continuous Function of
(T | A1),
R^1 by JORDAN5A:27, TOPMETR:17;
reconsider f1c =
f1c,
E2c =
E2c as
continuous RealMap of
(T | A1) ;
A16:
(
dom f = the
carrier of
(T | A) &
dom E2b = the
carrier of
(T | A) )
by FUNCT_2:def 1;
(2 / 3) |^ n > 0
by NEWTON:83;
then
(2 / 3) * ((2 / 3) |^ n) > (2 / 3) * 0
by XREAL_1:68;
then
(2 / 3) * ((2 / 3) |^ n) > 0
;
then consider g being
continuous Function of
T,
R^1 such that A17:
g,
dom g is_absolutely_bounded_by ((2 / 3) * ((2 / 3) |^ n)) / 3
and A18:
k - g,
A is_absolutely_bounded_by (2 * ((2 / 3) * ((2 / 3) |^ n))) / 3
by A1, A15, Th17;
reconsider ga =
g as
RealMap of
T by TOPMETR:17;
reconsider ga =
ga as
continuous RealMap of
T by JORDAN5A:27;
set y =
E2a + ga;
reconsider y1 =
E2a + ga as
continuous Function of
T,
R^1 by JORDAN5A:27, TOPMETR:17;
(
y1 in Funcs ( the
carrier of
T, the
carrier of
R^1) &
y1 is
continuous Function of
T,
R^1 )
by FUNCT_2:8;
then
E2a + ga in D
;
then reconsider y =
E2a + ga as
Element of
D ;
take
y
;
S1[n,x,y]take
E2
;
( E2 = x & ( f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) implies ex g being continuous Function of T,R^1 st
( y = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) ) ) )thus
E2 = x
by A11;
( f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) implies ex g being continuous Function of T,R^1 st
( y = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) ) )assume
f - E2,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n)
;
ex g being continuous Function of T,R^1 st
( y = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) )take
g
;
( y = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) )thus
y = E2 + g
;
( g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) )A19:
(2 / 3) * ((2 / 3) |^ n) = (2 / 3) |^ (n + 1)
by NEWTON:6;
hence
g, the
carrier of
T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1))
by A17, FUNCT_2:def 1;
(f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1))A20:
dom g = the
carrier of
T
by FUNCT_2:def 1;
A21:
((f - E2b) - g) | A =
((f - E2b) | A) - g
by RFUNCT_1:47
.=
(f - (E2b | A)) - g
.=
(f - (E2 | A)) - g
.=
((f - E2) | A) - g
by RFUNCT_1:47
.=
((f - E2) - g) | A
by RFUNCT_1:47
;
dom ((f - E2b) - g) =
(dom (f - E2b)) /\ (dom g)
by VALUED_1:12
.=
((dom f) /\ (dom E2b)) /\ (dom g)
by VALUED_1:12
.=
A
by A3, A16, A20, XBOOLE_1:28
;
hence
(f - E2) - g,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1))
by A18, A19, A21, Th16;
verum end; end;
end; consider F being
sequence of
D such that A22:
F . 0 = g0d
and A23:
for
n being
Nat holds
S1[
n,
F . n,
F . (n + 1)]
from RECDEF_1:sch 2(A10);
dom F = NAT
by FUNCT_2:def 1;
then reconsider F =
F as
Functional_Sequence of the
carrier of
T,
REAL by A24, SEQFUNC:1;
consider E2 being
continuous Function of
T,
R^1 such that A25:
E2 = F . 0
and A26:
(
f - E2,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ 0) implies ex
g being
continuous Function of
T,
R^1 st
(
F . (0 + 1) = E2 + g &
g, the
carrier of
T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (0 + 1)) &
(f - E2) - g,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (0 + 1)) ) )
by A23;
(2 / 3) |^ 0 = 1
by NEWTON:4;
then consider g1 being
continuous Function of
T,
R^1 such that A27:
F . (0 + 1) = E2 + g1
and A28:
g1, the
carrier of
T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (0 + 1))
and
(f - E2) - g1,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (0 + 1))
by A9, A22, A25, A26;
A29:
dom g1 =
the
carrier of
T
by FUNCT_2:def 1
.=
dom E2
by FUNCT_2:def 1
;
defpred S2[
Nat]
means (
F . $1 is
continuous Function of
T,
R^1 &
(F . $1) - (F . ($1 + 1)), the
carrier of
T is_absolutely_bounded_by (2 / 9) * ((2 / 3) to_power $1) &
(F . $1) - f,
A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power $1) );
A30:
now for n being Nat st S2[n] holds
S2[n + 1]let n be
Nat;
( S2[n] implies S2[n + 1] )A31:
dom f =
[#] (T | A1)
by FUNCT_2:def 1
.=
A
by PRE_TOPC:def 5
;
consider E2 being
continuous Function of
T,
R^1 such that A32:
(
E2 = F . n & (
f - E2,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) implies ex
g being
continuous Function of
T,
R^1 st
(
F . (n + 1) = E2 + g &
g, the
carrier of
T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) &
(f - E2) - g,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) ) ) )
by A23;
assume
S2[
n]
;
S2[n + 1]then
(F . n) - f,
A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n)
by POWER:41;
then consider g being
continuous Function of
T,
R^1 such that A33:
F . (n + 1) = E2 + g
and
g, the
carrier of
T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1))
and A34:
(f - E2) - g,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1))
by A32, Th22;
A35:
dom ((f - E2) - g) =
(dom (f - E2)) /\ (dom g)
by VALUED_1:12
.=
((dom f) /\ (dom E2)) /\ (dom g)
by VALUED_1:12
.=
((dom f) /\ the carrier of T) /\ (dom g)
by FUNCT_2:def 1
.=
(dom f) /\ (dom g)
by A31, XBOOLE_1:28
.=
(dom f) /\ the
carrier of
T
by FUNCT_2:def 1
.=
A
by A31, XBOOLE_1:28
;
reconsider g9 =
g as
continuous RealMap of
T by JORDAN5A:27, METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6;
consider E3 being
continuous Function of
T,
R^1 such that A36:
E3 = F . (n + 1)
and A37:
(
f - E3,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) implies ex
g being
continuous Function of
T,
R^1 st
(
F . ((n + 1) + 1) = E3 + g &
g, the
carrier of
T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ ((n + 1) + 1)) &
(f - E3) - g,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ ((n + 1) + 1)) ) )
by A23;
A38:
dom (f - (E2 + g)) =
(dom f) /\ (dom (E2 + g))
by VALUED_1:12
.=
A /\ ((dom E2) /\ (dom g))
by A31, VALUED_1:def 1
.=
A /\ ((dom E2) /\ the carrier of T)
by FUNCT_2:def 1
.=
A /\ ( the carrier of T /\ the carrier of T)
by FUNCT_2:def 1
.=
A
by XBOOLE_1:28
;
A39:
dom (f - E2) =
A /\ (dom E2)
by A31, VALUED_1:12
.=
A /\ the
carrier of
T
by FUNCT_2:def 1
.=
A
by XBOOLE_1:28
;
then consider gx being
continuous Function of
T,
R^1 such that A42:
F . ((n + 1) + 1) = E3 + gx
and A43:
gx, the
carrier of
T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ ((n + 1) + 1))
and
(f - E3) - gx,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ ((n + 1) + 1))
by A33, A34, A36, A37, A35, A38, FUNCT_1:2;
A44:
dom gx =
the
carrier of
T
by FUNCT_2:def 1
.=
dom E3
by FUNCT_2:def 1
;
reconsider E29 =
E2 as
continuous RealMap of
T by JORDAN5A:27, METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6;
A45:
(2 / 9) * ((2 / 3) to_power (n + 1)) =
((1 / 3) * (2 / 3)) * ((2 / 3) |^ (n + 1))
by POWER:41
.=
(1 / 3) * ((2 / 3) * ((2 / 3) |^ (n + 1)))
.=
(1 / 3) * ((2 / 3) |^ ((n + 1) + 1))
by NEWTON:6
;
A46:
dom ((gx + E3) - E3) =
(dom (gx + E3)) /\ (dom E3)
by VALUED_1:12
.=
((dom gx) /\ (dom E3)) /\ (dom E3)
by VALUED_1:def 1
.=
dom gx
by A44
;
then A48:
(F . ((n + 1) + 1)) - (F . (n + 1)) = gx
by A36, A42, A46, FUNCT_1:2;
(f - E2) - g,
A is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power (n + 1))
by A34, POWER:41;
then
(
E29 + g9 is
continuous RealMap of
T &
f - (F . (n + 1)),
A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power (n + 1)) )
by A33, A35, A38, A40, FUNCT_1:2;
hence
S2[
n + 1]
by A33, A43, A45, A48, Th22, JORDAN5A:27, METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6;
verum end; A49:
dom ((g1 + E2) - E2) =
(dom (g1 + E2)) /\ (dom E2)
by VALUED_1:12
.=
((dom g1) /\ (dom E2)) /\ (dom E2)
by VALUED_1:def 1
.=
dom g1
by A29
;
then A51:
(F . (0 + 1)) - (F . 0) = g1
by A25, A27, A49, FUNCT_1:2;
(
(2 / 3) to_power 0 = 1 &
(1 / 3) * ((2 / 3) |^ 1) = (1 / 3) * (2 / 3) )
by POWER:24;
then A52:
S2[
0 ]
by A9, A22, A28, A51, Th22;
A53:
for
n being
Nat holds
S2[
n]
from NAT_1:sch 2(A52, A30);
A54:
for
n being
Nat holds
(F . n) - (F . (n + 1)), the
carrier of
T is_absolutely_bounded_by (2 / 9) * ((2 / 3) to_power n)
by A53;
(
dom f = the
carrier of
(T | A1) &
rng f c= REAL )
by FUNCT_2:def 1, VALUED_0:def 3;
then A55:
f is
Function of
A1,
REAL
by A3, FUNCT_2:2;
then A56:
the
carrier of
T common_on_dom F
;
then A57:
A1 common_on_dom F
by SEQFUNC:23;
A58:
for
n being
Nat holds
(F . n) - f,
A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power n)
by A53;
A59:
2
/ 9
> 0
;
then
F is_unif_conv_on the
carrier of
T
by A56, A6, A54, Th9;
then reconsider h =
lim (
F, the
carrier of
T) as
continuous Function of
T,
R^1 by A53, Th20;
F is_point_conv_on the
carrier of
T
by A56, A59, A6, A54, Th9, SEQFUNC:22;
then A60:
h | A1 =
lim (
F,
A1)
by SEQFUNC:24
.=
f
by A6, A58, A57, A55, Th11
;
h, the
carrier of
T is_absolutely_bounded_by 1
proof
let x be
set ;
TIETZE:def 1 ( x in the carrier of T /\ (dom h) implies |.(h . x).| <= 1 )
assume
x in the
carrier of
T /\ (dom h)
;
|.(h . x).| <= 1
then reconsider z =
x as
Element of
T ;
A61:
dom (F . 0) = the
carrier of
T
by A22, FUNCT_2:def 1;
A62:
|.((F . 0) . z).| <= 1
/ 3
by A8, A22, A61;
then
(F . 0) . z >= - (1 / 3)
by ABSVALUE:5;
then A63:
((F . 0) . z) - ((2 / 9) / (1 - (2 / 3))) >= (- (1 / 3)) - ((2 / 9) / (1 - (2 / 3)))
by XREAL_1:9;
(F . 0) . z <= 1
/ 3
by A62, ABSVALUE:5;
then A64:
((F . 0) . z) + ((2 / 9) / (1 - (2 / 3))) <= (1 / 3) + ((2 / 9) / (1 - (2 / 3)))
by XREAL_1:7;
h . z <= ((F . 0) . z) + ((2 / 9) / (1 - (2 / 3)))
by A56, A59, A6, A54, Th10;
then A65:
h . z <= 1
by A64, XXREAL_0:2;
h . z >= ((F . 0) . z) - ((2 / 9) / (1 - (2 / 3)))
by A56, A59, A6, A54, Th10;
then
h . z >= - 1
by A63, XXREAL_0:2;
hence
|.(h . x).| <= 1
by A65, ABSVALUE:5;
verum
end; then reconsider h =
h as
Function of
T,
(Closed-Interval-TSpace ((- 1),1)) by Th21;
R^1 [.(- 1),1.] = [#] (Closed-Interval-TSpace ((- 1),1))
by A4, TOPREALB:def 3;
then
Closed-Interval-TSpace (
(- 1),1)
= R^1 | (R^1 [.(- 1),1.])
by PRE_TOPC:def 5;
then
h is
continuous
by TOPMETR:6;
hence
ex
g being
continuous Function of
T,
(Closed-Interval-TSpace ((- 1),1)) st
g | A = f
by A60;
verum end; end;