:: TIETZE semantic presentation
begin
theorem Th1: :: TIETZE:1
for a, b, c being real number st |.(a - b).| <= c holds
( b - c <= a & a <= b + c )
proof
let a, b, c be real number ; ::_thesis: ( |.(a - b).| <= c implies ( b - c <= a & a <= b + c ) )
assume A1: |.(a - b).| <= c ; ::_thesis: ( b - c <= a & a <= b + c )
A2: |.(a - b).| >= 0 by COMPLEX1:46;
then A3: b <= b + c by A1, XREAL_1:31;
A4: b >= b - c by A1, A2, XREAL_1:43;
percases ( a - b >= 0 or a - b < 0 ) ;
suppose a - b >= 0 ; ::_thesis: ( b - c <= a & a <= b + c )
then ( |.(a - b).| = a - b & a >= 0 + b ) by ABSVALUE:def_1, XREAL_1:19;
hence ( b - c <= a & a <= b + c ) by A1, A4, XREAL_1:20, XXREAL_0:2; ::_thesis: verum
end;
suppose a - b < 0 ; ::_thesis: ( b - c <= a & a <= b + c )
then A5: |.(a - b).| = - (a - b) by ABSVALUE:def_1
.= b - a ;
then 0 + a <= b by A2, XREAL_1:19;
hence ( b - c <= a & a <= b + c ) by A1, A3, A5, XREAL_1:12, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
theorem Th2: :: TIETZE:2
for f, g, h being real-valued Function st f c= g holds
h - f c= h - g
proof
let f, g, h be real-valued Function; ::_thesis: ( f c= g implies h - f c= h - g )
A1: dom (h - g) = (dom h) /\ (dom g) by VALUED_1:12;
A2: dom (h - f) = (dom h) /\ (dom f) by VALUED_1:12;
assume A3: f c= g ; ::_thesis: h - f c= h - g
then dom f c= dom g by GRFUNC_1:2;
then A4: dom (h - f) c= dom (h - g) by A1, A2, XBOOLE_1:27;
now__::_thesis:_for_x_being_set_st_x_in_dom_(h_-_f)_holds_
(h_-_f)_._x_=_(h_-_g)_._x
let x be set ; ::_thesis: ( x in dom (h - f) implies (h - f) . x = (h - g) . x )
assume A5: x in dom (h - f) ; ::_thesis: (h - f) . x = (h - g) . x
then A6: x in dom f by A2, XBOOLE_0:def_4;
thus (h - f) . x = (h . x) - (f . x) by A5, VALUED_1:13
.= (h . x) - (g . x) by A3, A6, GRFUNC_1:2
.= (h - g) . x by A4, A5, VALUED_1:13 ; ::_thesis: verum
end;
hence h - f c= h - g by A4, GRFUNC_1:2; ::_thesis: verum
end;
theorem :: TIETZE:3
for f, g, h being real-valued Function st f c= g holds
f - h c= g - h
proof
let f, g, h be real-valued Function; ::_thesis: ( f c= g implies f - h c= g - h )
A1: dom (f - h) = (dom f) /\ (dom h) by VALUED_1:12;
A2: dom (g - h) = (dom g) /\ (dom h) by VALUED_1:12;
assume A3: f c= g ; ::_thesis: f - h c= g - h
then dom f c= dom g by GRFUNC_1:2;
then A4: dom (f - h) c= dom (g - h) by A1, A2, XBOOLE_1:27;
now__::_thesis:_for_x_being_set_st_x_in_dom_(f_-_h)_holds_
(f_-_h)_._x_=_(g_-_h)_._x
let x be set ; ::_thesis: ( x in dom (f - h) implies (f - h) . x = (g - h) . x )
assume A5: x in dom (f - h) ; ::_thesis: (f - h) . x = (g - h) . x
then A6: x in dom f by A1, XBOOLE_0:def_4;
thus (f - h) . x = (f . x) - (h . x) by A5, VALUED_1:13
.= (g . x) - (h . x) by A3, A6, GRFUNC_1:2
.= (g - h) . x by A4, A5, VALUED_1:13 ; ::_thesis: verum
end;
hence f - h c= g - h by A4, GRFUNC_1:2; ::_thesis: verum
end;
definition
let f be real-valued Function;
let r be real number ;
let X be set ;
predf,X is_absolutely_bounded_by r means :Def1: :: TIETZE:def 1
for x being set st x in X /\ (dom f) holds
abs (f . x) <= r;
end;
:: deftheorem Def1 defines is_absolutely_bounded_by TIETZE:def_1_:_
for f being real-valued Function
for r being real number
for X being set holds
( f,X is_absolutely_bounded_by r iff for x being set st x in X /\ (dom f) holds
abs (f . x) <= r );
registration
cluster non empty Relation-like NAT -defined REAL -valued Function-like constant total quasi_total complex-valued ext-real-valued real-valued summable convergent for Element of K10(K11(NAT,REAL));
existence
ex b1 being Real_Sequence st
( b1 is summable & b1 is constant & b1 is convergent )
proof
set f = NAT --> 0;
reconsider f = NAT --> 0 as Real_Sequence by FUNCOP_1:45;
take f ; ::_thesis: ( f is summable & f is constant & f is convergent )
for n being Element of NAT holds f . n = 0 by FUNCOP_1:7;
hence f is summable by RSSPACE:16; ::_thesis: ( f is constant & f is convergent )
thus f is constant ; ::_thesis: f is convergent
thus f is convergent ; ::_thesis: verum
end;
end;
theorem :: TIETZE:4
for T1 being empty TopSpace
for T2 being TopSpace
for f being Function of T1,T2 holds f is continuous
proof
let T1 be empty TopSpace; ::_thesis: for T2 being TopSpace
for f being Function of T1,T2 holds f is continuous
let T2 be TopSpace; ::_thesis: for f being Function of T1,T2 holds f is continuous
let f be Function of T1,T2; ::_thesis: f is continuous
let A be Subset of T2; :: according to PRE_TOPC:def_6 ::_thesis: ( not A is closed or f " A is closed )
thus ( not A is closed or f " A is closed ) ; ::_thesis: verum
end;
theorem :: TIETZE:5
for f, g being summable Real_Sequence st ( for n being Element of NAT holds f . n <= g . n ) holds
Sum f <= Sum g
proof
let f, g be summable Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds f . n <= g . n ) implies Sum f <= Sum g )
A1: ( Sum f = lim (Partial_Sums f) & Sum g = lim (Partial_Sums g) ) by SERIES_1:def_3;
assume for n being Element of NAT holds f . n <= g . n ; ::_thesis: Sum f <= Sum g
then A2: for n being Element of NAT holds (Partial_Sums f) . n <= (Partial_Sums g) . n by SERIES_1:14;
( Partial_Sums f is convergent & Partial_Sums g is convergent ) by SERIES_1:def_2;
hence Sum f <= Sum g by A1, A2, SEQ_2:18; ::_thesis: verum
end;
theorem Th6: :: TIETZE:6
for f being Real_Sequence st f is absolutely_summable holds
abs (Sum f) <= Sum (abs f)
proof
let f be Real_Sequence; ::_thesis: ( f is absolutely_summable implies abs (Sum f) <= Sum (abs f) )
defpred S1[ Element of NAT ] means (abs (Partial_Sums f)) . $1 <= (Partial_Sums (abs f)) . $1;
A1: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; ::_thesis: S1[n + 1]
then |.((Partial_Sums f) . n).| <= (Partial_Sums (abs f)) . n by SEQ_1:12;
then ( |.(((Partial_Sums f) . n) + (f . (n + 1))).| <= |.((Partial_Sums f) . n).| + |.(f . (n + 1)).| & |.((Partial_Sums f) . n).| + |.(f . (n + 1)).| <= ((Partial_Sums (abs f)) . n) + |.(f . (n + 1)).| ) by COMPLEX1:56, XREAL_1:6;
then |.(((Partial_Sums f) . n) + (f . (n + 1))).| <= ((Partial_Sums (abs f)) . n) + |.(f . (n + 1)).| by XXREAL_0:2;
then |.((Partial_Sums f) . (n + 1)).| <= ((Partial_Sums (abs f)) . n) + |.(f . (n + 1)).| by SERIES_1:def_1;
then (abs (Partial_Sums f)) . (n + 1) <= ((Partial_Sums (abs f)) . n) + |.(f . (n + 1)).| by SEQ_1:12;
then (abs (Partial_Sums f)) . (n + 1) <= ((Partial_Sums (abs f)) . n) + ((abs f) . (n + 1)) by SEQ_1:12;
hence S1[n + 1] by SERIES_1:def_1; ::_thesis: verum
end;
(abs (Partial_Sums f)) . 0 = abs ((Partial_Sums f) . 0) by SEQ_1:12
.= abs (f . 0) by SERIES_1:def_1
.= (abs f) . 0 by SEQ_1:12 ;
then A2: S1[ 0 ] by SERIES_1:def_1;
A3: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1);
assume A4: f is absolutely_summable ; ::_thesis: abs (Sum f) <= Sum (abs f)
then abs f is summable by SERIES_1:def_4;
then A5: Partial_Sums (abs f) is convergent by SERIES_1:def_2;
f is summable by A4;
then A6: Partial_Sums f is convergent by SERIES_1:def_2;
then lim (abs (Partial_Sums f)) <= lim (Partial_Sums (abs f)) by A5, A3, SEQ_2:18;
then abs (lim (Partial_Sums f)) <= lim (Partial_Sums (abs f)) by A6, SEQ_4:14;
then abs (lim (Partial_Sums f)) <= Sum (abs f) by SERIES_1:def_3;
hence abs (Sum f) <= Sum (abs f) by SERIES_1:def_3; ::_thesis: verum
end;
theorem Th7: :: TIETZE:7
for f being Real_Sequence
for a, r being positive real number st r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds
( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) )
proof
let f be Real_Sequence; ::_thesis: for a, r being positive real number st r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds
( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) )
let a, r be positive real number ; ::_thesis: ( r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) implies ( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) ) )
deffunc H1( Nat, Real) -> Element of REAL = (f . ($1 + 1)) - (f . $1);
consider g being Function of NAT,REAL such that
A1: ( g . 0 = f . 0 & ( for n being Nat holds g . (n + 1) = H1(n,g . n) ) ) from NAT_1:sch_12();
now__::_thesis:_for_n_being_Element_of_NAT_holds_f_._(n_+_1)_=_(f_._n)_+_(g_._(n_+_1))
let n be Element of NAT ; ::_thesis: f . (n + 1) = (f . n) + (g . (n + 1))
thus f . (n + 1) = ((f . (n + 1)) - (f . n)) + (f . n)
.= (f . n) + (g . (n + 1)) by A1 ; ::_thesis: verum
end;
then A2: f = Partial_Sums g by A1, SERIES_1:def_1;
A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_(abs_g)_._n
let n be Element of NAT ; ::_thesis: 0 <= (abs g) . n
(abs g) . n = abs (g . n) by SEQ_1:12;
hence 0 <= (abs g) . n by COMPLEX1:46; ::_thesis: verum
end;
A4: |.r.| = r by COMPLEX1:43;
assume A5: r < 1 ; ::_thesis: ( ex n being Nat st not |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) or ( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) ) )
then A6: r GeoSeq is summable by A4, SERIES_1:24;
assume A7: for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ; ::_thesis: ( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) )
A8: now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_holds_
(abs_g)_._n_<=_((a_*_(r_"))_(#)_(r_GeoSeq))_._n
let n be Element of NAT ; ::_thesis: ( 1 <= n implies (abs g) . n <= ((a * (r ")) (#) (r GeoSeq)) . n )
set m = 1;
assume 1 <= n ; ::_thesis: (abs g) . n <= ((a * (r ")) (#) (r GeoSeq)) . n
then consider k being Nat such that
A9: n = 1 + k by NAT_1:10;
g . n = H1(k,g . k) by A1, A9;
then (abs g) . n = |.((f . n) - (f . k)).| by A9, SEQ_1:12
.= |.((f . k) - (f . n)).| by COMPLEX1:60 ;
then A10: (abs g) . n <= a * (r to_power k) by A7, A9;
(a * 1) * (r to_power k) = (a * ((r ") * r)) * (r to_power k) by XCMPLX_0:def_7
.= (a * (r ")) * (r * (r to_power k))
.= (a * (r ")) * ((r to_power 1) * (r to_power k)) by POWER:25
.= (a * (r ")) * (r to_power n) by A9, POWER:27
.= (a * (r ")) * (r |^ n) by POWER:41
.= (a * (r ")) * ((r GeoSeq) . n) by PREPOWER:def_1 ;
hence (abs g) . n <= ((a * (r ")) (#) (r GeoSeq)) . n by A10, SEQ_1:9; ::_thesis: verum
end;
(a * (r ")) (#) (r GeoSeq) is summable by A6, SERIES_1:10;
then abs g is summable by A3, A8, SERIES_1:19;
then A11: g is absolutely_summable by SERIES_1:def_4;
then g is summable ;
hence f is convergent by A2, SERIES_1:def_2; ::_thesis: for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r)
let n be Nat; ::_thesis: |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r)
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
A12: now__::_thesis:_for_k_being_Element_of_NAT_holds_
(_0_<=_(abs_(g_^\_(n9_+_1)))_._k_&_(abs_(g_^\_(n9_+_1)))_._k_<=_((a_*_(r_to_power_n))_(#)_(r_GeoSeq))_._k_)
let k be Element of NAT ; ::_thesis: ( 0 <= (abs (g ^\ (n9 + 1))) . k & (abs (g ^\ (n9 + 1))) . k <= ((a * (r to_power n)) (#) (r GeoSeq)) . k )
(abs (g ^\ (n9 + 1))) . k = |.((g ^\ (n9 + 1)) . k).| by SEQ_1:12;
hence 0 <= (abs (g ^\ (n9 + 1))) . k by COMPLEX1:46; ::_thesis: (abs (g ^\ (n9 + 1))) . k <= ((a * (r to_power n)) (#) (r GeoSeq)) . k
(abs (g ^\ (n9 + 1))) . k = |.((g ^\ (n9 + 1)) . k).| by SEQ_1:12
.= |.(g . ((n9 + 1) + k)).| by NAT_1:def_3
.= |.((f . ((n9 + k) + 1)) - (f . (n9 + k))).| by A1
.= |.((f . (n9 + k)) - (f . ((n9 + k) + 1))).| by UNIFORM1:11 ;
then (abs (g ^\ (n9 + 1))) . k <= a * (r to_power (n9 + k)) by A7;
then (abs (g ^\ (n9 + 1))) . k <= a * ((r to_power n9) * (r to_power k)) by POWER:27;
then (abs (g ^\ (n9 + 1))) . k <= (a * (r to_power n9)) * (r to_power k) ;
then (abs (g ^\ (n9 + 1))) . k <= (a * (r to_power n9)) * (r |^ k) by POWER:41;
then (abs (g ^\ (n9 + 1))) . k <= (a * (r to_power n9)) * ((r GeoSeq) . k) by PREPOWER:def_1;
hence (abs (g ^\ (n9 + 1))) . k <= ((a * (r to_power n)) (#) (r GeoSeq)) . k by SEQ_1:9; ::_thesis: verum
end;
A13: (a * (r to_power n)) (#) (r GeoSeq) is summable by A6, SERIES_1:10;
then abs (g ^\ (n9 + 1)) is summable by A12, SERIES_1:20;
then A14: g ^\ (n9 + 1) is absolutely_summable by SERIES_1:def_4;
lim f = Sum g by A2, SERIES_1:def_3;
then lim f = (f . n) + (Sum (g ^\ (n9 + 1))) by A2, A11, SERIES_1:15;
then A15: |.((lim f) - (f . n)).| <= Sum (abs (g ^\ (n9 + 1))) by A14, Th6;
A16: Sum (abs (g ^\ (n9 + 1))) <= Sum ((a * (r to_power n)) (#) (r GeoSeq)) by A13, A12, SERIES_1:20;
Sum ((a * (r to_power n)) (#) (r GeoSeq)) = (a * (r to_power n)) * (Sum (r GeoSeq)) by A6, SERIES_1:10
.= (a * (r to_power n)) * (1 / (1 - r)) by A5, A4, SERIES_1:24
.= (a * (r to_power n)) / (1 - r) by XCMPLX_1:99 ;
hence |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) by A16, A15, XXREAL_0:2; ::_thesis: verum
end;
theorem :: TIETZE:8
for f being Real_Sequence
for a, r being positive real number st r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds
( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) )
proof
let f be Real_Sequence; ::_thesis: for a, r being positive real number st r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds
( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) )
let a, r be positive real number ; ::_thesis: ( r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) implies ( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) ) )
assume A1: r < 1 ; ::_thesis: ( ex n being Nat st not |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) or ( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) ) )
A2: r to_power 0 = 1 by POWER:24;
assume for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ; ::_thesis: ( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) )
then |.((lim f) - (f . 0)).| <= (a * 1) / (1 - r) by A1, A2, Th7;
hence ( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) ) by Th1; ::_thesis: verum
end;
theorem Th9: :: TIETZE:9
for X, Z being non empty set
for F being Functional_Sequence of X,REAL st Z common_on_dom F holds
for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds
( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) )
proof
let X, Z be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL st Z common_on_dom F holds
for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds
( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) )
let F be Functional_Sequence of X,REAL; ::_thesis: ( Z common_on_dom F implies for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds
( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) ) )
assume A1: Z common_on_dom F ; ::_thesis: for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds
( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) )
Z c= dom (F . 0) by A1, SEQFUNC:def_9;
then reconsider Z9 = Z as non empty Subset of X by XBOOLE_1:1;
deffunc H1( Element of Z9) -> Element of REAL = lim (F # $1);
let a, r be positive real number ; ::_thesis: ( r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) implies ( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) ) )
assume A2: r < 1 ; ::_thesis: ( ex n being Nat st not (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) or ( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) ) )
consider f being Function of Z9,REAL such that
A3: for x being Element of Z9 holds f . x = H1(x) from FUNCT_2:sch_4();
reconsider f = f as PartFunc of X,REAL by RELSET_1:7;
assume A4: for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ; ::_thesis: ( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) )
thus F is_unif_conv_on Z ::_thesis: for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r)
proof
thus Z common_on_dom F by A1; :: according to SEQFUNC:def_12 ::_thesis: ex b1 being Element of K10(K11(X,REAL)) st
( Z = dom b1 & ( for b2 being Element of REAL holds
( b2 <= 0 or ex b3 being Element of NAT st
for b4 being Element of NAT
for b5 being Element of X holds
( not b3 <= b4 or not b5 in Z or not b2 <= abs (((F . b4) . b5) - (b1 . b5)) ) ) ) )
take f ; ::_thesis: ( Z = dom f & ( for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT
for b4 being Element of X holds
( not b2 <= b3 or not b4 in Z or not b1 <= abs (((F . b3) . b4) - (f . b4)) ) ) ) )
thus Z = dom f by FUNCT_2:def_1; ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT
for b4 being Element of X holds
( not b2 <= b3 or not b4 in Z or not b1 <= abs (((F . b3) . b4) - (f . b4)) ) )
A5: 1 - r > 0 by A2, XREAL_1:50;
let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT
for b3 being Element of X holds
( not b1 <= b2 or not b3 in Z or not p <= abs (((F . b2) . b3) - (f . b3)) ) )
assume p > 0 ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT
for b3 being Element of X holds
( not b1 <= b2 or not b3 in Z or not p <= abs (((F . b2) . b3) - (f . b3)) )
then p * (1 - r) > 0 by A5, XREAL_1:129;
then A6: (p * (1 - r)) / a > 0 by XREAL_1:139;
consider k being Element of NAT such that
A7: k >= 1 + (log (r,((p * (1 - r)) / a))) by MESFUNC1:8;
A8: ( a * ((p * (1 - r)) / a) = (p * (1 - r)) * (a / a) & a / a = 1 ) by XCMPLX_1:60, XCMPLX_1:75;
k > log (r,((p * (1 - r)) / a)) by A7, XREAL_1:39;
then r to_power k < r to_power (log (r,((p * (1 - r)) / a))) by A2, POWER:40;
then r to_power k < (p * (1 - r)) / a by A2, A6, POWER:def_3;
then a * (r to_power k) < a * ((p * (1 - r)) / a) by XREAL_1:68;
then (a * (r to_power k)) / (1 - r) < (p * (1 - r)) / (1 - r) by A5, A8, XREAL_1:74;
then A9: (a * (r to_power k)) / (1 - r) < p by A5, XCMPLX_1:89;
take k ; ::_thesis: for b1 being Element of NAT
for b2 being Element of X holds
( not k <= b1 or not b2 in Z or not p <= abs (((F . b1) . b2) - (f . b2)) )
let n be Element of NAT ; ::_thesis: for b1 being Element of X holds
( not k <= n or not b1 in Z or not p <= abs (((F . n) . b1) - (f . b1)) )
let x be Element of X; ::_thesis: ( not k <= n or not x in Z or not p <= abs (((F . n) . x) - (f . x)) )
assume that
A10: n >= k and
A11: x in Z ; ::_thesis: not p <= abs (((F . n) . x) - (f . x))
A12: ( (F . n) . x = (F # x) . n & |.(((F . n) . x) - (f . x)).| = |.((f . x) - ((F . n) . x)).| ) by COMPLEX1:60, SEQFUNC:def_10;
now__::_thesis:_for_n_being_Nat_holds_|.(((F_#_x)_._n)_-_((F_#_x)_._(n_+_1))).|_<=_a_*_(r_to_power_n)
let n be Nat; ::_thesis: |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n)
A13: n in NAT by ORDINAL1:def_12;
then A14: (F # x) . n = (F . n) . x by SEQFUNC:def_10;
A15: Z c= dom (F . (n + 1)) by A1, SEQFUNC:def_9;
Z c= dom (F . n) by A1, A13, SEQFUNC:def_9;
then x in (dom (F . n)) /\ (dom (F . (n + 1))) by A11, A15, XBOOLE_0:def_4;
then x in dom ((F . n) - (F . (n + 1))) by VALUED_1:12;
then A16: ( ((F . n) - (F . (n + 1))) . x = ((F . n) . x) - ((F . (n + 1)) . x) & x in Z /\ (dom ((F . n) - (F . (n + 1)))) ) by A11, VALUED_1:13, XBOOLE_0:def_4;
(F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) by A4;
then |.(((F . n) . x) - ((F . (n + 1)) . x)).| <= a * (r to_power n) by A16, Def1;
hence |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n) by A14, SEQFUNC:def_10; ::_thesis: verum
end;
then A17: |.((lim (F # x)) - ((F # x) . n)).| <= (a * (r to_power n)) / (1 - r) by A2, Th7;
( n = k or n > k ) by A10, XXREAL_0:1;
then r to_power n <= r to_power k by A2, POWER:40;
then A18: a * (r to_power n) <= a * (r to_power k) by XREAL_1:64;
1 - r > 1 - 1 by A2, XREAL_1:10;
then (a * (r to_power n)) / (1 - r) <= (a * (r to_power k)) / (1 - r) by A18, XREAL_1:72;
then A19: |.((lim (F # x)) - ((F # x) . n)).| <= (a * (r to_power k)) / (1 - r) by A17, XXREAL_0:2;
f . x = lim (F # x) by A3, A11;
hence |.(((F . n) . x) - (f . x)).| < p by A9, A19, A12, XXREAL_0:2; ::_thesis: verum
end;
then A20: F is_point_conv_on Z by SEQFUNC:22;
let n9 be Nat; ::_thesis: (lim (F,Z)) - (F . n9),Z is_absolutely_bounded_by (a * (r to_power n9)) / (1 - r)
let z be set ; :: according to TIETZE:def_1 ::_thesis: ( z in Z /\ (dom ((lim (F,Z)) - (F . n9))) implies abs (((lim (F,Z)) - (F . n9)) . z) <= (a * (r to_power n9)) / (1 - r) )
reconsider n = n9 as Element of NAT by ORDINAL1:def_12;
assume A21: z in Z /\ (dom ((lim (F,Z)) - (F . n9))) ; ::_thesis: abs (((lim (F,Z)) - (F . n9)) . z) <= (a * (r to_power n9)) / (1 - r)
then reconsider x = z as Element of X ;
A22: z in Z9 by A21, XBOOLE_0:def_4;
now__::_thesis:_for_n_being_Nat_holds_|.(((F_#_x)_._n)_-_((F_#_x)_._(n_+_1))).|_<=_a_*_(r_to_power_n)
let n be Nat; ::_thesis: |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n)
A23: (F # x) . (n + 1) = (F . (n + 1)) . x by SEQFUNC:def_10;
A24: Z c= dom (F . (n + 1)) by A1, SEQFUNC:def_9;
A25: n in NAT by ORDINAL1:def_12;
then Z c= dom (F . n) by A1, SEQFUNC:def_9;
then z in (dom (F . n)) /\ (dom (F . (n + 1))) by A22, A24, XBOOLE_0:def_4;
then A26: x in dom ((F . n) - (F . (n + 1))) by VALUED_1:12;
then A27: x in Z /\ (dom ((F . n) - (F . (n + 1)))) by A22, XBOOLE_0:def_4;
A28: (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) by A4;
(F # x) . n = (F . n) . x by A25, SEQFUNC:def_10;
then ((F . n) - (F . (n + 1))) . x = ((F # x) . n) - ((F # x) . (n + 1)) by A26, A23, VALUED_1:13;
hence |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n) by A27, A28, Def1; ::_thesis: verum
end;
then A29: |.((lim (F # x)) - ((F # x) . n)).| <= (a * (r to_power n)) / (1 - r) by A2, Th7;
Z = dom (lim (F,Z)) by A20, SEQFUNC:def_13;
then |.(((lim (F,Z)) . x) - ((F # x) . n)).| <= (a * (r to_power n)) / (1 - r) by A20, A22, A29, SEQFUNC:def_13;
then A30: |.(((lim (F,Z)) . x) - ((F . n) . x)).| <= (a * (r to_power n)) / (1 - r) by SEQFUNC:def_10;
z in dom ((lim (F,Z)) - (F . n9)) by A21, XBOOLE_0:def_4;
hence abs (((lim (F,Z)) - (F . n9)) . z) <= (a * (r to_power n9)) / (1 - r) by A30, VALUED_1:13; ::_thesis: verum
end;
theorem Th10: :: TIETZE:10
for X, Z being non empty set
for F being Functional_Sequence of X,REAL st Z common_on_dom F holds
for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds
for z being Element of Z holds
( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) )
proof
let X, Z be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL st Z common_on_dom F holds
for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds
for z being Element of Z holds
( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) )
let F be Functional_Sequence of X,REAL; ::_thesis: ( Z common_on_dom F implies for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds
for z being Element of Z holds
( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) ) )
assume A1: Z common_on_dom F ; ::_thesis: for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds
for z being Element of Z holds
( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) )
let a, r be positive real number ; ::_thesis: ( r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) implies for z being Element of Z holds
( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) ) )
assume A2: r < 1 ; ::_thesis: ( ex n being Nat st not (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) or for z being Element of Z holds
( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) ) )
assume A3: for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ; ::_thesis: for z being Element of Z holds
( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) )
then F is_point_conv_on Z by A1, A2, Th9, SEQFUNC:22;
then A4: dom (lim (F,Z)) = Z by SEQFUNC:def_13;
r to_power 0 = 1 by POWER:24;
then A5: (lim (F,Z)) - (F . 0),Z is_absolutely_bounded_by (a * 1) / (1 - r) by A1, A2, A3, Th9;
let z be Element of Z; ::_thesis: ( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) )
( z in Z & Z c= dom (F . 0) ) by A1, SEQFUNC:def_9;
then z in (dom (lim (F,Z))) /\ (dom (F . 0)) by A4, XBOOLE_0:def_4;
then A6: z in dom ((lim (F,Z)) - (F . 0)) by VALUED_1:12;
then z in Z /\ (dom ((lim (F,Z)) - (F . 0))) by XBOOLE_0:def_4;
then |.(((lim (F,Z)) - (F . 0)) . z).| <= (a * 1) / (1 - r) by A5, Def1;
then |.(((lim (F,Z)) . z) - ((F . 0) . z)).| <= (a * 1) / (1 - r) by A6, VALUED_1:13;
hence ( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) ) by Th1; ::_thesis: verum
end;
theorem Th11: :: TIETZE:11
for X, Z being non empty set
for F being Functional_Sequence of X,REAL st Z common_on_dom F holds
for a, r being positive real number
for f being Function of Z,REAL st r < 1 & ( for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ) holds
( F is_point_conv_on Z & lim (F,Z) = f )
proof
let X, Z be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL st Z common_on_dom F holds
for a, r being positive real number
for f being Function of Z,REAL st r < 1 & ( for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ) holds
( F is_point_conv_on Z & lim (F,Z) = f )
let F be Functional_Sequence of X,REAL; ::_thesis: ( Z common_on_dom F implies for a, r being positive real number
for f being Function of Z,REAL st r < 1 & ( for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ) holds
( F is_point_conv_on Z & lim (F,Z) = f ) )
assume A1: Z common_on_dom F ; ::_thesis: for a, r being positive real number
for f being Function of Z,REAL st r < 1 & ( for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ) holds
( F is_point_conv_on Z & lim (F,Z) = f )
let a, r be positive real number ; ::_thesis: for f being Function of Z,REAL st r < 1 & ( for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ) holds
( F is_point_conv_on Z & lim (F,Z) = f )
let f be Function of Z,REAL; ::_thesis: ( r < 1 & ( for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ) implies ( F is_point_conv_on Z & lim (F,Z) = f ) )
A2: dom f = Z by FUNCT_2:def_1;
Z c= dom (F . 0) by A1, SEQFUNC:def_9;
then reconsider g = f as PartFunc of X,REAL by A2, RELSET_1:5, XBOOLE_1:1;
assume A3: r < 1 ; ::_thesis: ( ex n being Nat st not (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) or ( F is_point_conv_on Z & lim (F,Z) = f ) )
assume A4: for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ; ::_thesis: ( F is_point_conv_on Z & lim (F,Z) = f )
A5: now__::_thesis:_for_x_being_Element_of_X_st_x_in_Z_holds_
for_p_being_Real_st_p_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
abs_(((F_._n)_._x)_-_(g_._x))_<_p
let x be Element of X; ::_thesis: ( x in Z implies for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((F . n) . x) - (g . x)) < p )
assume A6: x in Z ; ::_thesis: for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((F . n) . x) - (g . x)) < p
let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((F . n) . x) - (g . x)) < p )
assume A7: p > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((F . n) . x) - (g . x)) < p
consider k being Element of NAT such that
A8: k >= 1 + (log (r,((p * (1 - r)) / a))) by MESFUNC1:8;
k > log (r,((p * (1 - r)) / a)) by A8, XREAL_1:39;
then A9: r to_power k < r to_power (log (r,((p * (1 - r)) / a))) by A3, POWER:40;
A10: ( a * ((p * (1 - r)) / a) = (p * (1 - r)) * (a / a) & a / a = 1 ) by XCMPLX_1:60, XCMPLX_1:75;
A11: 1 - r > 0 by A3, XREAL_1:50;
then p * (1 - r) > 0 by A7, XREAL_1:129;
then (p * (1 - r)) / a > 0 by XREAL_1:139;
then r to_power k < (p * (1 - r)) / a by A3, A9, POWER:def_3;
then a * (r to_power k) < a * ((p * (1 - r)) / a) by XREAL_1:68;
then (a * (r to_power k)) / (1 - r) < (p * (1 - r)) / (1 - r) by A11, A10, XREAL_1:74;
then A12: (a * (r to_power k)) / (1 - r) < p by A11, XCMPLX_1:89;
take k = k; ::_thesis: for n being Element of NAT st n >= k holds
abs (((F . n) . x) - (g . x)) < p
let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((F . n) . x) - (g . x)) < p )
Z c= dom (F . n) by A1, SEQFUNC:def_9;
then x in (dom (F . n)) /\ (dom f) by A2, A6, XBOOLE_0:def_4;
then A13: x in dom ((F . n) - f) by VALUED_1:12;
then A14: ((F . n) - f) . x = ((F . n) . x) - (f . x) by VALUED_1:13;
assume n >= k ; ::_thesis: abs (((F . n) . x) - (g . x)) < p
then ( n = k or n > k ) by XXREAL_0:1;
then r to_power n <= r to_power k by A3, POWER:40;
then A15: a * (r to_power n) <= a * (r to_power k) by XREAL_1:64;
A16: (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) by A4;
r to_power n >= 0 by POWER:34;
then (a * (r to_power n)) * (1 - r) <= (a * (r to_power n)) * 1 by XREAL_1:43, XREAL_1:64;
then A17: (a * (r to_power n)) / 1 <= (a * (r to_power n)) / (1 - r) by A11, XREAL_1:102;
1 - r > 1 - 1 by A3, XREAL_1:10;
then (a * (r to_power n)) / (1 - r) <= (a * (r to_power k)) / (1 - r) by A15, XREAL_1:72;
then A18: a * (r to_power n) <= (a * (r to_power k)) / (1 - r) by A17, XXREAL_0:2;
x in Z /\ (dom ((F . n) - f)) by A13, XBOOLE_0:def_4;
then |.(((F . n) . x) - (f . x)).| <= a * (r to_power n) by A14, A16, Def1;
then abs (((F . n) . x) - (g . x)) <= (a * (r to_power k)) / (1 - r) by A18, XXREAL_0:2;
hence abs (((F . n) . x) - (g . x)) < p by A12, XXREAL_0:2; ::_thesis: verum
end;
thus A19: F is_point_conv_on Z ::_thesis: lim (F,Z) = f
proof
thus Z common_on_dom F by A1; :: according to SEQFUNC:def_11 ::_thesis: ex b1 being Element of K10(K11(X,REAL)) st
( Z = dom b1 & ( for b2 being Element of X holds
( not b2 in Z or for b3 being Element of REAL holds
( b3 <= 0 or ex b4 being Element of NAT st
for b5 being Element of NAT holds
( not b4 <= b5 or not b3 <= abs (((F . b5) . b2) - (b1 . b2)) ) ) ) ) )
take g ; ::_thesis: ( Z = dom g & ( for b1 being Element of X holds
( not b1 in Z or for b2 being Element of REAL holds
( b2 <= 0 or ex b3 being Element of NAT st
for b4 being Element of NAT holds
( not b3 <= b4 or not b2 <= abs (((F . b4) . b1) - (g . b1)) ) ) ) ) )
thus Z = dom g by FUNCT_2:def_1; ::_thesis: for b1 being Element of X holds
( not b1 in Z or for b2 being Element of REAL holds
( b2 <= 0 or ex b3 being Element of NAT st
for b4 being Element of NAT holds
( not b3 <= b4 or not b2 <= abs (((F . b4) . b1) - (g . b1)) ) ) )
thus for b1 being Element of X holds
( not b1 in Z or for b2 being Element of REAL holds
( b2 <= 0 or ex b3 being Element of NAT st
for b4 being Element of NAT holds
( not b3 <= b4 or not b2 <= abs (((F . b4) . b1) - (g . b1)) ) ) ) by A5; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_lim_(F_#_x)
let x be Element of X; ::_thesis: ( x in dom g implies g . x = lim (F # x) )
assume A20: x in dom g ; ::_thesis: g . x = lim (F # x)
A21: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((F # x) . m) - (g . x)) < p
proof
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((F # x) . m) - (g . x)) < p )
reconsider p9 = p as Real by XREAL_0:def_1;
assume 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((F # x) . m) - (g . x)) < p
then consider n being Element of NAT such that
A22: for m being Element of NAT st n <= m holds
abs (((F . m) . x) - (g . x)) < p9 by A2, A5, A20;
take n ; ::_thesis: for m being Element of NAT st n <= m holds
abs (((F # x) . m) - (g . x)) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((F # x) . m) - (g . x)) < p )
(F . m) . x = (F # x) . m by SEQFUNC:def_10;
hence ( n <= m implies abs (((F # x) . m) - (g . x)) < p ) by A22; ::_thesis: verum
end;
F # x is convergent by A2, A19, A20, SEQFUNC:20;
hence g . x = lim (F # x) by A21, SEQ_2:def_7; ::_thesis: verum
end;
hence lim (F,Z) = f by A2, A19, SEQFUNC:def_13; ::_thesis: verum
end;
registration
let T be TopSpace;
let A be closed Subset of T;
clusterT | A -> closed ;
coherence
T | A is closed
proof
let X be Subset of T; :: according to BORSUK_1:def_11 ::_thesis: ( not X = the carrier of (T | A) or X is closed )
thus ( not X = the carrier of (T | A) or X is closed ) by PRE_TOPC:8; ::_thesis: verum
end;
end;
theorem Th12: :: TIETZE:12
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
for x being Point of X holds
( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
for x being Point of X holds
( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) )
let X1, X2 be non empty SubSpace of X; ::_thesis: for f1 being Function of X1,Y
for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
for x being Point of X holds
( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) )
let f1 be Function of X1,Y; ::_thesis: for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
for x being Point of X holds
( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) )
let f2 be Function of X2,Y; ::_thesis: ( ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) implies for x being Point of X holds
( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) ) )
assume A1: ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) ; ::_thesis: for x being Point of X holds
( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) )
let x be Point of X; ::_thesis: ( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) )
set F = f1 union f2;
A2: X1 is SubSpace of X1 union X2 by TSEP_1:22;
hereby ::_thesis: ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x )
assume x in the carrier of X1 ; ::_thesis: (f1 union f2) . x = f1 . x
hence (f1 union f2) . x = ((f1 union f2) | the carrier of X1) . x by FUNCT_1:49
.= ((f1 union f2) | X1) . x by A2, TMAP_1:def_5
.= f1 . x by A1, TMAP_1:def_12 ;
::_thesis: verum
end;
A3: X2 is SubSpace of X1 union X2 by TSEP_1:22;
assume x in the carrier of X2 ; ::_thesis: (f1 union f2) . x = f2 . x
hence (f1 union f2) . x = ((f1 union f2) | the carrier of X2) . x by FUNCT_1:49
.= ((f1 union f2) | X2) . x by A3, TMAP_1:def_5
.= f2 . x by A1, TMAP_1:def_12 ;
::_thesis: verum
end;
theorem Th13: :: TIETZE:13
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
rng (f1 union f2) c= (rng f1) \/ (rng f2)
proof
let X, Y be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
rng (f1 union f2) c= (rng f1) \/ (rng f2)
let X1, X2 be non empty SubSpace of X; ::_thesis: for f1 being Function of X1,Y
for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
rng (f1 union f2) c= (rng f1) \/ (rng f2)
let f1 be Function of X1,Y; ::_thesis: for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
rng (f1 union f2) c= (rng f1) \/ (rng f2)
let f2 be Function of X2,Y; ::_thesis: ( ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) implies rng (f1 union f2) c= (rng f1) \/ (rng f2) )
set F = f1 union f2;
assume A1: ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) ; ::_thesis: rng (f1 union f2) c= (rng f1) \/ (rng f2)
thus rng (f1 union f2) c= (rng f1) \/ (rng f2) ::_thesis: verum
proof
A2: the carrier of (X1 union X2) = the carrier of X1 \/ the carrier of X2 by TSEP_1:def_2;
A3: the carrier of X2 = dom f2 by FUNCT_2:def_1;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f1 union f2) or y in (rng f1) \/ (rng f2) )
A4: the carrier of X1 = dom f1 by FUNCT_2:def_1;
assume y in rng (f1 union f2) ; ::_thesis: y in (rng f1) \/ (rng f2)
then consider x being set such that
A5: x in dom (f1 union f2) and
A6: (f1 union f2) . x = y by FUNCT_1:def_3;
A7: x is Point of X by A5, PRE_TOPC:25;
percases ( x in the carrier of X1 or x in the carrier of X2 ) by A5, A2, XBOOLE_0:def_3;
suppose x in the carrier of X1 ; ::_thesis: y in (rng f1) \/ (rng f2)
then ( f1 . x in rng f1 & (f1 union f2) . x = f1 . x ) by A1, A4, A7, Th12, FUNCT_1:def_3;
hence y in (rng f1) \/ (rng f2) by A6, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x in the carrier of X2 ; ::_thesis: y in (rng f1) \/ (rng f2)
then ( f2 . x in rng f2 & (f1 union f2) . x = f2 . x ) by A1, A3, A7, Th12, FUNCT_1:def_3;
hence y in (rng f1) \/ (rng f2) by A6, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;
theorem Th14: :: TIETZE:14
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) )
let X1, X2 be non empty SubSpace of X; ::_thesis: for f1 being Function of X1,Y
for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) )
let f1 be Function of X1,Y; ::_thesis: for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) )
let f2 be Function of X2,Y; ::_thesis: ( ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) implies ( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) ) )
assume A1: ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) ; ::_thesis: ( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) )
set F = f1 union f2;
A2: the carrier of (X1 union X2) = the carrier of X1 \/ the carrier of X2 by TSEP_1:def_2;
hereby ::_thesis: for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A
let A be Subset of X1; ::_thesis: (f1 union f2) .: A = f1 .: A
thus (f1 union f2) .: A = f1 .: A ::_thesis: verum
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: f1 .: A c= (f1 union f2) .: A
let y be set ; ::_thesis: ( y in (f1 union f2) .: A implies y in f1 .: A )
assume y in (f1 union f2) .: A ; ::_thesis: y in f1 .: A
then consider x being Element of (X1 union X2) such that
A3: x in A and
A4: y = (f1 union f2) . x by FUNCT_2:65;
x is Point of X by PRE_TOPC:25;
then (f1 union f2) . x = f1 . x by A1, A3, Th12;
hence y in f1 .: A by A3, A4, FUNCT_2:35; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f1 .: A or y in (f1 union f2) .: A )
assume y in f1 .: A ; ::_thesis: y in (f1 union f2) .: A
then consider x being Element of X1 such that
A5: ( x in A & y = f1 . x ) by FUNCT_2:65;
x is Point of X by PRE_TOPC:25;
then A6: (f1 union f2) . x = f1 . x by A1, Th12;
x in the carrier of (X1 union X2) by A2, XBOOLE_0:def_3;
hence y in (f1 union f2) .: A by A5, A6, FUNCT_2:35; ::_thesis: verum
end;
end;
let A be Subset of X2; ::_thesis: (f1 union f2) .: A = f2 .: A
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: f2 .: A c= (f1 union f2) .: A
let y be set ; ::_thesis: ( y in (f1 union f2) .: A implies y in f2 .: A )
assume y in (f1 union f2) .: A ; ::_thesis: y in f2 .: A
then consider x being Element of (X1 union X2) such that
A7: x in A and
A8: y = (f1 union f2) . x by FUNCT_2:65;
x is Point of X by PRE_TOPC:25;
then (f1 union f2) . x = f2 . x by A1, A7, Th12;
hence y in f2 .: A by A7, A8, FUNCT_2:35; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f2 .: A or y in (f1 union f2) .: A )
assume y in f2 .: A ; ::_thesis: y in (f1 union f2) .: A
then consider x being Element of X2 such that
A9: ( x in A & y = f2 . x ) by FUNCT_2:65;
x is Point of X by PRE_TOPC:25;
then A10: (f1 union f2) . x = f2 . x by A1, Th12;
x in the carrier of (X1 union X2) by A2, XBOOLE_0:def_3;
hence y in (f1 union f2) .: A by A9, A10, FUNCT_2:35; ::_thesis: verum
end;
theorem Th15: :: TIETZE:15
for r being real number
for X being set
for f, g being real-valued Function st f c= g & g,X is_absolutely_bounded_by r holds
f,X is_absolutely_bounded_by r
proof
let r be real number ; ::_thesis: for X being set
for f, g being real-valued Function st f c= g & g,X is_absolutely_bounded_by r holds
f,X is_absolutely_bounded_by r
let X be set ; ::_thesis: for f, g being real-valued Function st f c= g & g,X is_absolutely_bounded_by r holds
f,X is_absolutely_bounded_by r
let f, g be real-valued Function; ::_thesis: ( f c= g & g,X is_absolutely_bounded_by r implies f,X is_absolutely_bounded_by r )
assume that
A1: f c= g and
A2: g,X is_absolutely_bounded_by r ; ::_thesis: f,X is_absolutely_bounded_by r
let x be set ; :: according to TIETZE:def_1 ::_thesis: ( x in X /\ (dom f) implies abs (f . x) <= r )
assume A3: x in X /\ (dom f) ; ::_thesis: abs (f . x) <= r
then A4: x in dom f by XBOOLE_0:def_4;
A5: x in X by A3, XBOOLE_0:def_4;
dom f c= dom g by A1, GRFUNC_1:2;
then x in X /\ (dom g) by A4, A5, XBOOLE_0:def_4;
then abs (g . x) <= r by A2, Def1;
hence abs (f . x) <= r by A1, A4, GRFUNC_1:2; ::_thesis: verum
end;
theorem Th16: :: TIETZE:16
for r being real number
for X being set
for f, g being real-valued Function st ( X c= dom f or dom g c= dom f ) & f | X = g | X & f,X is_absolutely_bounded_by r holds
g,X is_absolutely_bounded_by r
proof
let r be real number ; ::_thesis: for X being set
for f, g being real-valued Function st ( X c= dom f or dom g c= dom f ) & f | X = g | X & f,X is_absolutely_bounded_by r holds
g,X is_absolutely_bounded_by r
let X be set ; ::_thesis: for f, g being real-valued Function st ( X c= dom f or dom g c= dom f ) & f | X = g | X & f,X is_absolutely_bounded_by r holds
g,X is_absolutely_bounded_by r
let f, g be real-valued Function; ::_thesis: ( ( X c= dom f or dom g c= dom f ) & f | X = g | X & f,X is_absolutely_bounded_by r implies g,X is_absolutely_bounded_by r )
assume that
A1: ( X c= dom f or dom g c= dom f ) and
A2: f | X = g | X and
A3: f,X is_absolutely_bounded_by r ; ::_thesis: g,X is_absolutely_bounded_by r
let x be set ; :: according to TIETZE:def_1 ::_thesis: ( x in X /\ (dom g) implies abs (g . x) <= r )
assume A4: x in X /\ (dom g) ; ::_thesis: abs (g . x) <= r
then A5: x in X by XBOOLE_0:def_4;
then A6: f . x = (f | X) . x by FUNCT_1:49
.= g . x by A2, A5, FUNCT_1:49 ;
x in dom g by A4, XBOOLE_0:def_4;
then x in X /\ (dom f) by A1, A5, XBOOLE_0:def_4;
hence abs (g . x) <= r by A3, A6, Def1; ::_thesis: verum
end;
theorem Th17: :: TIETZE:17
for r being real number
for T being non empty TopSpace
for A being closed Subset of T st r > 0 & T is normal holds
for f being continuous Function of (T | A),R^1 st f,A is_absolutely_bounded_by r holds
ex g being continuous Function of T,R^1 st
( g, dom g is_absolutely_bounded_by r / 3 & f - g,A is_absolutely_bounded_by (2 * r) / 3 )
proof
let r be real number ; ::_thesis: for T being non empty TopSpace
for A being closed Subset of T st r > 0 & T is normal holds
for f being continuous Function of (T | A),R^1 st f,A is_absolutely_bounded_by r holds
ex g being continuous Function of T,R^1 st
( g, dom g is_absolutely_bounded_by r / 3 & f - g,A is_absolutely_bounded_by (2 * r) / 3 )
let T be non empty TopSpace; ::_thesis: for A being closed Subset of T st r > 0 & T is normal holds
for f being continuous Function of (T | A),R^1 st f,A is_absolutely_bounded_by r holds
ex g being continuous Function of T,R^1 st
( g, dom g is_absolutely_bounded_by r / 3 & f - g,A is_absolutely_bounded_by (2 * r) / 3 )
let A be closed Subset of T; ::_thesis: ( r > 0 & T is normal implies for f being continuous Function of (T | A),R^1 st f,A is_absolutely_bounded_by r holds
ex g being continuous Function of T,R^1 st
( g, dom g is_absolutely_bounded_by r / 3 & f - g,A is_absolutely_bounded_by (2 * r) / 3 ) )
assume that
A1: r > 0 and
A2: T is normal ; ::_thesis: for f being continuous Function of (T | A),R^1 st f,A is_absolutely_bounded_by r holds
ex g being continuous Function of T,R^1 st
( g, dom g is_absolutely_bounded_by r / 3 & f - g,A is_absolutely_bounded_by (2 * r) / 3 )
set C2 = R^1 (right_closed_halfline (r / 3));
set C1 = R^1 (left_closed_halfline (- (r / 3)));
set A2 = right_closed_halfline (r / 3);
set A1 = left_closed_halfline (- (r / 3));
let f be continuous Function of (T | A),R^1; ::_thesis: ( f,A is_absolutely_bounded_by r implies ex g being continuous Function of T,R^1 st
( g, dom g is_absolutely_bounded_by r / 3 & f - g,A is_absolutely_bounded_by (2 * r) / 3 ) )
assume A3: for x being set st x in A /\ (dom f) holds
abs (f . x) <= r ; :: according to TIETZE:def_1 ::_thesis: ex g being continuous Function of T,R^1 st
( g, dom g is_absolutely_bounded_by r / 3 & f - g,A is_absolutely_bounded_by (2 * r) / 3 )
reconsider r1 = r as Real by XREAL_0:def_1;
set e = (2 * r1) / 3;
0 < 2 * r by A1, XREAL_1:129;
then (2 * r1) / 3 > 0 by XREAL_1:139;
then consider h being Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (((((2 * r1) / 3) * 0) + (- (r1 / 3))),((((2 * r1) / 3) * 1) + (- (r1 / 3))))) such that
A4: h is being_homeomorphism and
A5: for w being Real st w in [.0,1.] holds
h . w = (((2 * r1) / 3) * w) + (- (r1 / 3)) by JGRAPH_5:36;
A6: h is continuous by A4, TOPS_2:def_5;
A7: the carrier of (Closed-Interval-TSpace (0,1)) = [.0,1.] by TOPMETR:18;
( f " (R^1 (left_closed_halfline (- (r / 3)))) is closed & f " (R^1 (right_closed_halfline (r / 3))) is closed ) by PRE_TOPC:def_6;
then reconsider D1 = f " (R^1 (left_closed_halfline (- (r / 3)))), D2 = f " (R^1 (right_closed_halfline (r / 3))) as closed Subset of T by PRE_TOPC:11, TSEP_1:12;
A8: left_closed_halfline (- (r / 3)) = R^1 (left_closed_halfline (- (r / 3))) by TOPREALB:def_3;
A9: right_closed_halfline (r / 3) = R^1 (right_closed_halfline (r / 3)) by TOPREALB:def_3;
A10: - (- (r / 3)) > 0 by A1, XREAL_1:139;
then f " (left_closed_halfline (- (r / 3))) misses f " (right_closed_halfline (r / 3)) by FUNCT_1:71, XXREAL_1:279;
then consider F being Function of T,R^1 such that
A11: F is continuous and
A12: for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in D1 implies F . x = 0 ) & ( x in D2 implies F . x = 1 ) ) by A2, A8, A9, URYSOHN3:20;
A13: rng F c= [.0,1.]
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in [.0,1.] )
assume y in rng F ; ::_thesis: y in [.0,1.]
then consider x being set such that
A14: x in dom F and
A15: F . x = y by FUNCT_1:def_3;
( 0 <= F . x & F . x <= 1 ) by A12, A14;
hence y in [.0,1.] by A15, XXREAL_1:1; ::_thesis: verum
end;
then reconsider F1 = F as Function of T,(Closed-Interval-TSpace (0,1)) by A7, FUNCT_2:6;
A16: the carrier of (Closed-Interval-TSpace ((- (r / 3)),(r / 3))) = [.(- (r / 3)),(r / 3).] by A1, TOPMETR:18;
set g1 = h * F;
A17: rng (h * F) c= the carrier of (Closed-Interval-TSpace ((- (r / 3)),(r / 3))) ;
( dom F = the carrier of T & dom h = the carrier of (Closed-Interval-TSpace (0,1)) ) by FUNCT_2:def_1;
then A18: dom (h * F) = the carrier of T by A7, A13, RELAT_1:27;
then reconsider g1 = h * F as Function of T,(Closed-Interval-TSpace ((- (r / 3)),(r / 3))) by A17, FUNCT_2:2;
reconsider g = g1 as Function of T,R^1 by TOPREALA:7;
F1 is continuous by A11, PRE_TOPC:27;
then reconsider g = g as continuous Function of T,R^1 by A6, PRE_TOPC:26;
take g ; ::_thesis: ( g, dom g is_absolutely_bounded_by r / 3 & f - g,A is_absolutely_bounded_by (2 * r) / 3 )
A19: rng g1 c= the carrier of (Closed-Interval-TSpace ((- (r / 3)),(r / 3))) ;
thus g, dom g is_absolutely_bounded_by r / 3 ::_thesis: f - g,A is_absolutely_bounded_by (2 * r) / 3
proof
let x be set ; :: according to TIETZE:def_1 ::_thesis: ( x in (dom g) /\ (dom g) implies abs (g . x) <= r / 3 )
assume x in (dom g) /\ (dom g) ; ::_thesis: abs (g . x) <= r / 3
then g . x in rng g by FUNCT_1:def_3;
then ( - (r / 3) <= g . x & g . x <= r / 3 ) by A16, A19, XXREAL_1:1;
hence abs (g . x) <= r / 3 by ABSVALUE:5; ::_thesis: verum
end;
thus f - g,A is_absolutely_bounded_by (2 * r) / 3 ::_thesis: verum
proof
A20: 1 in [.0,1.] by XXREAL_1:1;
A21: 0 in [.0,1.] by XXREAL_1:1;
let x be set ; :: according to TIETZE:def_1 ::_thesis: ( x in A /\ (dom (f - g)) implies abs ((f - g) . x) <= (2 * r) / 3 )
assume A22: x in A /\ (dom (f - g)) ; ::_thesis: abs ((f - g) . x) <= (2 * r) / 3
A23: x in dom (f - g) by A22, XBOOLE_0:def_4;
then A24: (f - g) . x = (f . x) - (g . x) by VALUED_1:13;
dom (f - g) = (dom f) /\ (dom g) by VALUED_1:12;
then A25: x in dom f by A23, XBOOLE_0:def_4;
x in A by A22, XBOOLE_0:def_4;
then x in A /\ (dom f) by A25, XBOOLE_0:def_4;
then A26: abs (f . x) <= r by A3;
then A27: - r <= f . x by ABSVALUE:5;
percases ( f . x <= - (r / 3) or r / 3 <= f . x or ( - (r / 3) < f . x & f . x < r / 3 ) ) ;
supposeA28: f . x <= - (r / 3) ; ::_thesis: abs ((f - g) . x) <= (2 * r) / 3
then f . x in left_closed_halfline (- (r / 3)) by XXREAL_1:234;
then x in f " (left_closed_halfline (- (r / 3))) by A25, FUNCT_1:def_7;
then F . x = 0 by A8, A12;
then A29: g . x = h . 0 by A18, A22, FUNCT_1:12
.= - (r1 / 3) by A5, A21 ;
- r = (- ((2 * r) / 3)) - (r / 3) ;
then A30: - ((2 * r) / 3) <= (f . x) + (r / 3) by A27, XREAL_1:20;
(f . x) + (r / 3) <= (- (r / 3)) + (r / 3) by A28, XREAL_1:6;
hence abs ((f - g) . x) <= (2 * r) / 3 by A1, A24, A29, A30, ABSVALUE:5; ::_thesis: verum
end;
supposeA31: r / 3 <= f . x ; ::_thesis: abs ((f - g) . x) <= (2 * r) / 3
then f . x in right_closed_halfline (r / 3) by XXREAL_1:236;
then x in f " (right_closed_halfline (r / 3)) by A25, FUNCT_1:def_7;
then F . x = 1 by A9, A12;
then A32: g . x = h . 1 by A18, A22, FUNCT_1:12
.= r1 / 3 by A5, A20 ;
f . x <= (r / 3) + ((2 * r) / 3) by A26, ABSVALUE:5;
then A33: (f . x) - (r / 3) <= (2 * r) / 3 by XREAL_1:20;
(- ((2 * r) / 3)) + (r / 3) <= f . x by A10, A31;
then - ((2 * r) / 3) <= (f . x) - (r / 3) by XREAL_1:19;
hence abs ((f - g) . x) <= (2 * r) / 3 by A24, A32, A33, ABSVALUE:5; ::_thesis: verum
end;
supposeA34: ( - (r / 3) < f . x & f . x < r / 3 ) ; ::_thesis: abs ((f - g) . x) <= (2 * r) / 3
A35: g . x in rng g by A18, A22, FUNCT_1:def_3;
then ( - ((2 * r) / 3) = (- (r / 3)) - (r / 3) & g . x <= r / 3 ) by A16, A17, XXREAL_1:1;
then A36: - ((2 * r) / 3) <= (f . x) - (g . x) by A34, XREAL_1:13;
- (r / 3) <= g . x by A16, A17, A35, XXREAL_1:1;
then (f . x) - (g . x) <= (r / 3) - (- (r / 3)) by A34, XREAL_1:14;
hence abs ((f - g) . x) <= (2 * r) / 3 by A24, A36, ABSVALUE:5; ::_thesis: verum
end;
end;
end;
end;
theorem Th18: :: TIETZE:18
for T being non empty TopSpace st ( for A, B being non empty closed Subset of T st A misses B holds
ex f being continuous Function of T,R^1 st
( f .: A = {0} & f .: B = {1} ) ) holds
T is normal
proof
let T be non empty TopSpace; ::_thesis: ( ( for A, B being non empty closed Subset of T st A misses B holds
ex f being continuous Function of T,R^1 st
( f .: A = {0} & f .: B = {1} ) ) implies T is normal )
assume A1: for A, B being non empty closed Subset of T st A misses B holds
ex f being continuous Function of T,R^1 st
( f .: A = {0} & f .: B = {1} ) ; ::_thesis: T is normal
let W, V be Subset of T; :: according to COMPTS_1:def_3 ::_thesis: ( W = {} or V = {} or not W is closed or not V is closed or not W misses V or ex b1, b2 being Element of K10( the carrier of T) st
( b1 is open & b2 is open & W c= b1 & V c= b2 & b1 misses b2 ) )
assume ( W <> {} & V <> {} & W is closed & V is closed & W misses V ) ; ::_thesis: ex b1, b2 being Element of K10( the carrier of T) st
( b1 is open & b2 is open & W c= b1 & V c= b2 & b1 misses b2 )
then consider f being continuous Function of T,R^1 such that
A2: f .: W = {0} and
A3: f .: V = {1} by A1;
set Q = f " (R^1 (right_open_halfline (1 / 2)));
set P = f " (R^1 (left_open_halfline (1 / 2)));
take f " (R^1 (left_open_halfline (1 / 2))) ; ::_thesis: ex b1 being Element of K10( the carrier of T) st
( f " (R^1 (left_open_halfline (1 / 2))) is open & b1 is open & W c= f " (R^1 (left_open_halfline (1 / 2))) & V c= b1 & f " (R^1 (left_open_halfline (1 / 2))) misses b1 )
take f " (R^1 (right_open_halfline (1 / 2))) ; ::_thesis: ( f " (R^1 (left_open_halfline (1 / 2))) is open & f " (R^1 (right_open_halfline (1 / 2))) is open & W c= f " (R^1 (left_open_halfline (1 / 2))) & V c= f " (R^1 (right_open_halfline (1 / 2))) & f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2))) )
[#] R^1 <> {} ;
hence ( f " (R^1 (left_open_halfline (1 / 2))) is open & f " (R^1 (right_open_halfline (1 / 2))) is open ) by TOPS_2:43; ::_thesis: ( W c= f " (R^1 (left_open_halfline (1 / 2))) & V c= f " (R^1 (right_open_halfline (1 / 2))) & f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2))) )
A4: R^1 (left_open_halfline (1 / 2)) = left_open_halfline (1 / 2) by TOPREALB:def_3;
A5: dom f = the carrier of T by FUNCT_2:def_1;
thus W c= f " (R^1 (left_open_halfline (1 / 2))) ::_thesis: ( V c= f " (R^1 (right_open_halfline (1 / 2))) & f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2))) )
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in W or a in f " (R^1 (left_open_halfline (1 / 2))) )
A6: 0 in left_open_halfline (1 / 2) by XXREAL_1:233;
assume A7: a in W ; ::_thesis: a in f " (R^1 (left_open_halfline (1 / 2)))
then f . a in f .: W by FUNCT_2:35;
then f . a = 0 by A2, TARSKI:def_1;
hence a in f " (R^1 (left_open_halfline (1 / 2))) by A4, A5, A7, A6, FUNCT_1:def_7; ::_thesis: verum
end;
A8: R^1 (right_open_halfline (1 / 2)) = right_open_halfline (1 / 2) by TOPREALB:def_3;
thus V c= f " (R^1 (right_open_halfline (1 / 2))) ::_thesis: f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2)))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in V or a in f " (R^1 (right_open_halfline (1 / 2))) )
A9: 1 in right_open_halfline (1 / 2) by XXREAL_1:235;
assume A10: a in V ; ::_thesis: a in f " (R^1 (right_open_halfline (1 / 2)))
then f . a in f .: V by FUNCT_2:35;
then f . a = 1 by A3, TARSKI:def_1;
hence a in f " (R^1 (right_open_halfline (1 / 2))) by A8, A5, A10, A9, FUNCT_1:def_7; ::_thesis: verum
end;
thus f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2))) by A4, A8, FUNCT_1:71, XXREAL_1:275; ::_thesis: verum
end;
theorem Th19: :: TIETZE:19
for T being non empty TopSpace
for f being Function of T,R^1
for x being Point of T holds
( f is_continuous_at x iff for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) )
proof
let T be non empty TopSpace; ::_thesis: for f being Function of T,R^1
for x being Point of T holds
( f is_continuous_at x iff for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) )
let f be Function of T,R^1; ::_thesis: for x being Point of T holds
( f is_continuous_at x iff for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) )
let x be Point of T; ::_thesis: ( f is_continuous_at x iff for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) )
thus ( f is_continuous_at x implies for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) ) ::_thesis: ( ( for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) ) implies f is_continuous_at x )
proof
reconsider fx = f . x as Point of RealSpace by TOPMETR:12, TOPMETR:def_6;
assume A1: f is_continuous_at x ; ::_thesis: for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) )
let e be real number ; ::_thesis: ( e > 0 implies ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) )
assume A2: e > 0 ; ::_thesis: ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) )
reconsider G = Ball (fx,e) as Subset of R^1 by TOPMETR:12, TOPMETR:def_6;
( G is open & fx in G ) by A2, GOBOARD6:1, TOPMETR:14, TOPMETR:def_6;
then consider H being Subset of T such that
A3: ( H is open & x in H ) and
A4: f .: H c= G by A1, TMAP_1:43;
take H ; ::_thesis: ( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) )
thus ( H is open & x in H ) by A3; ::_thesis: for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e
A5: dom f = the carrier of T by FUNCT_2:def_1;
let y be Point of T; ::_thesis: ( y in H implies abs ((f . y) - (f . x)) < e )
assume y in H ; ::_thesis: abs ((f . y) - (f . x)) < e
then A6: f . y in f .: H by A5, FUNCT_1:def_6;
then f . y in G by A4;
then reconsider fy = f . y as Point of RealSpace ;
dist (fy,fx) < e by A4, A6, METRIC_1:11;
hence abs ((f . y) - (f . x)) < e by TOPMETR:11; ::_thesis: verum
end;
assume A7: for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) ; ::_thesis: f is_continuous_at x
now__::_thesis:_for_G_being_Subset_of_R^1_st_G_is_open_&_f_._x_in_G_holds_
ex_H_being_Subset_of_T_st_
(_H_is_open_&_x_in_H_&_f_.:_H_c=_G_)
reconsider fx = f . x as Point of RealSpace by TOPMETR:12, TOPMETR:def_6;
let G be Subset of R^1; ::_thesis: ( G is open & f . x in G implies ex H being Subset of T st
( H is open & x in H & f .: H c= G ) )
assume ( G is open & f . x in G ) ; ::_thesis: ex H being Subset of T st
( H is open & x in H & f .: H c= G )
then consider r being real number such that
A8: r > 0 and
A9: Ball (fx,r) c= G by TOPMETR:15, TOPMETR:def_6;
consider H being Subset of T such that
A10: ( H is open & x in H ) and
A11: for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < r by A7, A8;
take H = H; ::_thesis: ( H is open & x in H & f .: H c= G )
thus ( H is open & x in H ) by A10; ::_thesis: f .: H c= G
thus f .: H c= G ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f .: H or a in G )
assume a in f .: H ; ::_thesis: a in G
then consider y being set such that
A12: y in dom f and
A13: y in H and
A14: a = f . y by FUNCT_1:def_6;
reconsider y = y as Point of T by A12;
reconsider fy = f . y as Point of RealSpace by TOPMETR:12, TOPMETR:def_6;
abs ((f . y) - (f . x)) < r by A11, A13;
then abs (- ((f . y) - (f . x))) < r by COMPLEX1:52;
then abs ((f . x) - (f . y)) < r ;
then dist (fx,fy) < r by TOPMETR:11;
then fy in Ball (fx,r) by METRIC_1:11;
hence a in G by A9, A14; ::_thesis: verum
end;
end;
hence f is_continuous_at x by TMAP_1:43; ::_thesis: verum
end;
theorem Th20: :: TIETZE:20
for T being non empty TopSpace
for F being Functional_Sequence of the carrier of T,REAL st F is_unif_conv_on the carrier of T & ( for i being Element of NAT holds F . i is continuous Function of T,R^1 ) holds
lim (F, the carrier of T) is continuous Function of T,R^1
proof
let T be non empty TopSpace; ::_thesis: for F being Functional_Sequence of the carrier of T,REAL st F is_unif_conv_on the carrier of T & ( for i being Element of NAT holds F . i is continuous Function of T,R^1 ) holds
lim (F, the carrier of T) is continuous Function of T,R^1
let F be Functional_Sequence of the carrier of T,REAL; ::_thesis: ( F is_unif_conv_on the carrier of T & ( for i being Element of NAT holds F . i is continuous Function of T,R^1 ) implies lim (F, the carrier of T) is continuous Function of T,R^1 )
assume that
A1: F is_unif_conv_on the carrier of T and
A2: for i being Element of NAT holds F . i is continuous Function of T,R^1 ; ::_thesis: lim (F, the carrier of T) is continuous Function of T,R^1
F is_point_conv_on the carrier of T by A1, SEQFUNC:43;
then dom (lim (F, the carrier of T)) = the carrier of T by SEQFUNC:def_13;
then reconsider l = lim (F, the carrier of T) as Function of T,R^1 by FUNCT_2:def_1, TOPMETR:17;
now__::_thesis:_for_p_being_Point_of_T_holds_l_is_continuous_at_p
let p be Point of T; ::_thesis: l is_continuous_at p
now__::_thesis:_for_e_being_real_number_st_e_>_0_holds_
ex_H_being_Subset_of_T_st_
(_H_is_open_&_p_in_H_&_(_for_y_being_Point_of_T_st_y_in_H_holds_
abs_((l_._y)_-_(l_._p))_<_e_)_)
let e be real number ; ::_thesis: ( e > 0 implies ex H being Subset of T st
( H is open & p in H & ( for y being Point of T st y in H holds
abs ((l . y) - (l . p)) < e ) ) )
assume A3: e > 0 ; ::_thesis: ex H being Subset of T st
( H is open & p in H & ( for y being Point of T st y in H holds
abs ((l . y) - (l . p)) < e ) )
reconsider e3 = e / 3 as Real ;
A4: e3 > 0 by A3, XREAL_1:139;
then consider k being Element of NAT such that
A5: for n being Element of NAT
for x being Point of T st n >= k & x in the carrier of T holds
abs (((F . n) . x) - ((lim (F, the carrier of T)) . x)) < e3 by A1, SEQFUNC:43;
reconsider Fk = F . k as continuous Function of T,R^1 by A2;
A6: abs ((Fk . p) - (l . p)) < e3 by A5;
Fk is_continuous_at p by TMAP_1:44;
then consider H being Subset of T such that
A7: ( H is open & p in H ) and
A8: for y being Point of T st y in H holds
abs ((Fk . y) - (Fk . p)) < e3 by A4, Th19;
take H = H; ::_thesis: ( H is open & p in H & ( for y being Point of T st y in H holds
abs ((l . y) - (l . p)) < e ) )
thus ( H is open & p in H ) by A7; ::_thesis: for y being Point of T st y in H holds
abs ((l . y) - (l . p)) < e
let y be Point of T; ::_thesis: ( y in H implies abs ((l . y) - (l . p)) < e )
assume A9: y in H ; ::_thesis: abs ((l . y) - (l . p)) < e
abs ((Fk . y) - (l . y)) < e3 by A5;
then abs (- ((Fk . y) - (l . y))) < e3 by COMPLEX1:52;
then ( abs (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y))) <= (abs ((Fk . p) - (l . p))) + (abs (- ((Fk . y) - (l . y)))) & (abs ((Fk . p) - (l . p))) + (abs (- ((Fk . y) - (l . y)))) < e3 + e3 ) by A6, COMPLEX1:56, XREAL_1:8;
then abs (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y))) < 2 * e3 by XXREAL_0:2;
then ( abs (((Fk . y) - (Fk . p)) + (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y)))) <= (abs ((Fk . y) - (Fk . p))) + (abs (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y)))) & (abs ((Fk . y) - (Fk . p))) + (abs (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y)))) < e3 + (2 * e3) ) by A8, A9, COMPLEX1:56, XREAL_1:8;
hence abs ((l . y) - (l . p)) < e by XXREAL_0:2; ::_thesis: verum
end;
hence l is_continuous_at p by Th19; ::_thesis: verum
end;
hence lim (F, the carrier of T) is continuous Function of T,R^1 by TMAP_1:44; ::_thesis: verum
end;
theorem Th21: :: TIETZE:21
for T being non empty TopSpace
for f being Function of T,R^1
for r being positive real number holds
( f, the carrier of T is_absolutely_bounded_by r iff f is Function of T,(Closed-Interval-TSpace ((- r),r)) )
proof
let T be non empty TopSpace; ::_thesis: for f being Function of T,R^1
for r being positive real number holds
( f, the carrier of T is_absolutely_bounded_by r iff f is Function of T,(Closed-Interval-TSpace ((- r),r)) )
let f be Function of T,R^1; ::_thesis: for r being positive real number holds
( f, the carrier of T is_absolutely_bounded_by r iff f is Function of T,(Closed-Interval-TSpace ((- r),r)) )
let r be positive real number ; ::_thesis: ( f, the carrier of T is_absolutely_bounded_by r iff f is Function of T,(Closed-Interval-TSpace ((- r),r)) )
A1: dom f = the carrier of T by FUNCT_2:def_1;
thus ( f, the carrier of T is_absolutely_bounded_by r implies f is Function of T,(Closed-Interval-TSpace ((- r),r)) ) ::_thesis: ( f is Function of T,(Closed-Interval-TSpace ((- r),r)) implies f, the carrier of T is_absolutely_bounded_by r )
proof
assume A2: f, the carrier of T is_absolutely_bounded_by r ; ::_thesis: f is Function of T,(Closed-Interval-TSpace ((- r),r))
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_T_holds_
f_._x_in_the_carrier_of_(Closed-Interval-TSpace_((-_r),r))
let x be set ; ::_thesis: ( x in the carrier of T implies f . x in the carrier of (Closed-Interval-TSpace ((- r),r)) )
assume x in the carrier of T ; ::_thesis: f . x in the carrier of (Closed-Interval-TSpace ((- r),r))
then x in the carrier of T /\ (dom f) by A1;
then abs (f . x) <= r by A2, Def1;
then 2 * (abs (f . x)) <= 2 * r by XREAL_1:64;
then (abs 2) * (abs (f . x)) <= 2 * r by ABSVALUE:def_1;
then (abs (- 2)) * (abs (f . x)) <= 2 * r by COMPLEX1:52;
then abs ((- 2) * (f . x)) <= r - (- r) by COMPLEX1:65;
then abs (((- r) + r) - (2 * (f . x))) <= r - (- r) ;
then f . x in [.(- r),r.] by RCOMP_1:2;
hence f . x in the carrier of (Closed-Interval-TSpace ((- r),r)) by TOPMETR:18; ::_thesis: verum
end;
hence f is Function of T,(Closed-Interval-TSpace ((- r),r)) by A1, FUNCT_2:3; ::_thesis: verum
end;
assume A3: f is Function of T,(Closed-Interval-TSpace ((- r),r)) ; ::_thesis: f, the carrier of T is_absolutely_bounded_by r
let x be set ; :: according to TIETZE:def_1 ::_thesis: ( x in the carrier of T /\ (dom f) implies abs (f . x) <= r )
assume x in the carrier of T /\ (dom f) ; ::_thesis: abs (f . x) <= r
then f . x in the carrier of (Closed-Interval-TSpace ((- r),r)) by A3, FUNCT_2:5;
then f . x in [.(- r),r.] by TOPMETR:18;
then abs (((- r) + r) - (2 * (f . x))) <= r - (- r) by RCOMP_1:2;
then abs ((- 2) * (f . x)) <= r - (- r) ;
then (abs (- 2)) * (abs (f . x)) <= 2 * r by COMPLEX1:65;
then (abs 2) * (abs (f . x)) <= 2 * r by COMPLEX1:52;
then 2 * (abs (f . x)) <= 2 * r by ABSVALUE:def_1;
then (2 * (abs (f . x))) / 2 <= (2 * r) / 2 by XREAL_1:72;
hence abs (f . x) <= r ; ::_thesis: verum
end;
theorem Th22: :: TIETZE:22
for r being real number
for X being set
for f, g being real-valued Function st f - g,X is_absolutely_bounded_by r holds
g - f,X is_absolutely_bounded_by r
proof
let r be real number ; ::_thesis: for X being set
for f, g being real-valued Function st f - g,X is_absolutely_bounded_by r holds
g - f,X is_absolutely_bounded_by r
let X be set ; ::_thesis: for f, g being real-valued Function st f - g,X is_absolutely_bounded_by r holds
g - f,X is_absolutely_bounded_by r
let f, g be real-valued Function; ::_thesis: ( f - g,X is_absolutely_bounded_by r implies g - f,X is_absolutely_bounded_by r )
assume A1: f - g,X is_absolutely_bounded_by r ; ::_thesis: g - f,X is_absolutely_bounded_by r
let x be set ; :: according to TIETZE:def_1 ::_thesis: ( x in X /\ (dom (g - f)) implies abs ((g - f) . x) <= r )
assume A2: x in X /\ (dom (g - f)) ; ::_thesis: abs ((g - f) . x) <= r
then A3: x in dom (g - f) by XBOOLE_0:def_4;
A4: dom (f - g) = (dom f) /\ (dom g) by VALUED_1:12
.= dom (g - f) by VALUED_1:12 ;
then abs ((f - g) . x) <= r by A1, A2, Def1;
then abs ((f . x) - (g . x)) <= r by A4, A3, VALUED_1:13;
then abs (- ((f . x) - (g . x))) <= r by COMPLEX1:52;
then abs ((g . x) - (f . x)) <= r ;
hence abs ((g - f) . x) <= r by A3, VALUED_1:13; ::_thesis: verum
end;
theorem :: TIETZE:23
for T being non empty TopSpace st T is normal holds
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
proof
let T be non empty TopSpace; ::_thesis: ( 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 ; ::_thesis: 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; ::_thesis: 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)); ::_thesis: ( 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 ; ::_thesis: 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;
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f
then reconsider A1 = A as empty Subset of T ;
set g = T --> (R^1 0);
T --> (R^1 0) = the carrier of T --> 0 by TOPREALB:def_2;
then A5: rng (T --> (R^1 0)) = {0} by FUNCOP_1:8;
rng (T --> (R^1 0)) c= the carrier of (Closed-Interval-TSpace ((- 1),1))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (T --> (R^1 0)) or y in the carrier of (Closed-Interval-TSpace ((- 1),1)) )
assume y in rng (T --> (R^1 0)) ; ::_thesis: y in the carrier of (Closed-Interval-TSpace ((- 1),1))
then y = 0 by A5, TARSKI:def_1;
hence y in the carrier of (Closed-Interval-TSpace ((- 1),1)) by A4, XXREAL_1:1; ::_thesis: verum
end;
then reconsider g = T --> (R^1 0) as Function of T,(Closed-Interval-TSpace ((- 1),1)) by FUNCT_2:6;
reconsider g = g as continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) by PRE_TOPC:27;
take g ; ::_thesis: g | A = f
g | A1 is empty ;
hence g | A = f ; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f
then 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[ Element of 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
proof
let x be set ; :: according to TIETZE:def_1 ::_thesis: ( x in A /\ (dom f1) implies abs (f1 . x) <= 1 )
assume x in A /\ (dom f1) ; ::_thesis: abs (f1 . x) <= 1
then x in dom f1 by XBOOLE_0:def_4;
then A7: f1 . x in rng f1 by FUNCT_1:def_3;
rng f1 c= the carrier of (Closed-Interval-TSpace ((- 1),1)) by RELAT_1:def_19;
then ( - 1 <= f1 . x & f1 . x <= 1 ) by A4, A7, XXREAL_1:1;
hence abs (f1 . x) <= 1 by ABSVALUE:5; ::_thesis: verum
end;
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 Element of NAT
for x being Element of D ex y being Element of D st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of D ex y being Element of D st S1[n,x,y]
let x be Element of D; ::_thesis: 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;
percases ( 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) ) ;
supposeA13: not f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) ; ::_thesis: ex y being Element of D st S1[n,x,y]
take x ; ::_thesis: S1[n,x,x]
take E2 ; ::_thesis: ( 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; ::_thesis: verum
end;
supposeA14: f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) ; ::_thesis: 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 ; ::_thesis: S1[n,x,y]
take E2 ; ::_thesis: ( 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; ::_thesis: ( 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) ; ::_thesis: 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 ; ::_thesis: ( 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 ; ::_thesis: ( 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; ::_thesis: (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 by RFUNCT_1:47
.= (f - (E2 | A)) - g by RELAT_1:72
.= ((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; ::_thesis: verum
end;
end;
end;
consider F being Function of NAT,D such that
A22: F . 0 = g0d and
A23: for n being Element of NAT holds S1[n,F . n,F . (n + 1)] from RECDEF_1:sch_2(A10);
A24: now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_is_PartFunc_of_the_carrier_of_T,REAL
let n be Element of NAT ; ::_thesis: F . n is PartFunc of the carrier of T,REAL
S1[n,F . n,F . (n + 1)] by A23;
hence F . n is PartFunc of the carrier of T,REAL by METRIC_1:def_13, TOPMETR:12, TOPMETR:def_6; ::_thesis: verum
end;
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__::_thesis:_for_n_being_Element_of_NAT_st_S2[n]_holds_
S2[n_+_1]
let n be Element of NAT ; ::_thesis: ( 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] ; ::_thesis: 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 ;
A40: now__::_thesis:_for_a_being_set_st_a_in_A_holds_
((f_-_E2)_-_g)_._a_=_(f_-_(E2_+_g))_._a
let a be set ; ::_thesis: ( a in A implies ((f - E2) - g) . a = (f - (E2 + g)) . a )
assume A41: a in A ; ::_thesis: ((f - E2) - g) . a = (f - (E2 + g)) . a
hence ((f - E2) - g) . a = ((f - E2) . a) - (g . a) by A35, VALUED_1:13
.= ((f . a) - (E2 . a)) - (g . a) by A39, A41, VALUED_1:13
.= (f . a) - ((E2 . a) + (g . a))
.= (f . a) - ((E2 + g) . a) by A41, VALUED_1:1
.= (f - (E2 + g)) . a by A38, A41, VALUED_1:13 ;
::_thesis: verum
end;
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 ;
now__::_thesis:_for_a_being_set_st_a_in_dom_gx_holds_
((gx_+_E3)_-_E3)_._a_=_gx_._a
let a be set ; ::_thesis: ( a in dom gx implies ((gx + E3) - E3) . a = gx . a )
assume A47: a in dom gx ; ::_thesis: ((gx + E3) - E3) . a = gx . a
hence ((gx + E3) - E3) . a = ((gx + E3) . a) - (E3 . a) by A46, VALUED_1:13
.= ((gx . a) + (E3 . a)) - (E3 . a) by A47, VALUED_1:1
.= gx . a ;
::_thesis: verum
end;
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; ::_thesis: 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 ;
now__::_thesis:_for_a_being_set_st_a_in_dom_g1_holds_
((g1_+_E2)_-_E2)_._a_=_g1_._a
let a be set ; ::_thesis: ( a in dom g1 implies ((g1 + E2) - E2) . a = g1 . a )
assume A50: a in dom g1 ; ::_thesis: ((g1 + E2) - E2) . a = g1 . a
hence ((g1 + E2) - E2) . a = ((g1 + E2) . a) - (E2 . a) by A49, VALUED_1:13
.= ((g1 . a) + (E2 . a)) - (E2 . a) by A50, VALUED_1:1
.= g1 . a ;
::_thesis: verum
end;
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 NEWTON:5, POWER:24;
then A52: S2[ 0 ] by A9, A22, A28, A51, Th22;
A53: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A52, A30);
A54: now__::_thesis:_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)
let n be Nat; ::_thesis: (F . n) - (F . (n + 1)), the carrier of T is_absolutely_bounded_by (2 / 9) * ((2 / 3) to_power n)
n in NAT by ORDINAL1:def_12;
hence (F . n) - (F . (n + 1)), the carrier of T is_absolutely_bounded_by (2 / 9) * ((2 / 3) to_power n) by A53; ::_thesis: verum
end;
( 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;
now__::_thesis:_for_n_being_Element_of_NAT_holds_the_carrier_of_T_c=_dom_(F_._n)
let n be Element of NAT ; ::_thesis: the carrier of T c= dom (F . n)
S1[n,F . n,F . (n + 1)] by A23;
hence the carrier of T c= dom (F . n) by FUNCT_2:def_1; ::_thesis: verum
end;
then A56: the carrier of T common_on_dom F by SEQFUNC:def_9;
then A57: A1 common_on_dom F by SEQFUNC:23;
A58: now__::_thesis:_for_n_being_Nat_holds_(F_._n)_-_f,A1_is_absolutely_bounded_by_(2_/_3)_*_((2_/_3)_to_power_n)
let n be Nat; ::_thesis: (F . n) - f,A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power n)
n in NAT by ORDINAL1:def_12;
hence (F . n) - f,A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power n) by A53; ::_thesis: verum
end;
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 ; :: according to TIETZE:def_1 ::_thesis: ( x in the carrier of T /\ (dom h) implies abs (h . x) <= 1 )
assume x in the carrier of T /\ (dom h) ; ::_thesis: abs (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;
then z in the carrier of T /\ (dom (F . 0)) ;
then A62: |.((F . 0) . z).| <= 1 / 3 by A8, A22, A61, Def1;
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 abs (h . x) <= 1 by A65, ABSVALUE:5; ::_thesis: 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; ::_thesis: verum
end;
end;
end;
theorem :: TIETZE:24
for T being non empty TopSpace st ( for A being non empty closed Subset of T
for f being continuous Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f ) holds
T is normal
proof
let T be non empty TopSpace; ::_thesis: ( ( for A being non empty closed Subset of T
for f being continuous Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f ) implies T is normal )
assume A1: for A being non empty closed Subset of T
for f being continuous Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f ; ::_thesis: T is normal
for C, D being non empty closed Subset of T st C misses D holds
ex f being continuous Function of T,R^1 st
( f .: C = {0} & f .: D = {1} )
proof
set f2 = T --> (R^1 1);
set f1 = T --> (R^1 0);
let C, D be non empty closed Subset of T; ::_thesis: ( C misses D implies ex f being continuous Function of T,R^1 st
( f .: C = {0} & f .: D = {1} ) )
assume A2: C misses D ; ::_thesis: ex f being continuous Function of T,R^1 st
( f .: C = {0} & f .: D = {1} )
set g1 = (T --> (R^1 0)) | (T | C);
set g2 = (T --> (R^1 1)) | (T | D);
set f = ((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D));
A3: the carrier of (T | D) = D by PRE_TOPC:8;
(T --> (R^1 1)) | (T | D) = (T --> (R^1 1)) | the carrier of (T | D) by TMAP_1:def_4;
then A4: rng ((T --> (R^1 1)) | (T | D)) c= rng (T --> (R^1 1)) by RELAT_1:70;
(T --> (R^1 0)) | (T | C) = (T --> (R^1 0)) | the carrier of (T | C) by TMAP_1:def_4;
then rng ((T --> (R^1 0)) | (T | C)) c= rng (T --> (R^1 0)) by RELAT_1:70;
then A5: (rng ((T --> (R^1 0)) | (T | C))) \/ (rng ((T --> (R^1 1)) | (T | D))) c= (rng (T --> (R^1 0))) \/ (rng (T --> (R^1 1))) by A4, XBOOLE_1:13;
A6: T --> (R^1 0) = the carrier of T --> 0 by TOPREALB:def_2;
then A7: rng (T --> (R^1 0)) = {0} by FUNCOP_1:8;
A8: T --> (R^1 1) = the carrier of T --> 1 by TOPREALB:def_2;
then A9: rng (T --> (R^1 1)) = {1} by FUNCOP_1:8;
A10: the carrier of (T | C) = C by PRE_TOPC:8;
then A11: T | C misses T | D by A2, A3, TSEP_1:def_3;
then rng (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) c= (rng ((T --> (R^1 0)) | (T | C))) \/ (rng ((T --> (R^1 1)) | (T | D))) by Th13;
then A12: rng (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) c= (rng (T --> (R^1 0))) \/ (rng (T --> (R^1 1))) by A5, XBOOLE_1:1;
A13: rng (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) c= [.(- 1),1.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) or x in [.(- 1),1.] )
assume x in rng (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) ; ::_thesis: x in [.(- 1),1.]
then ( x in {0} or x in {1} ) by A12, A7, A9, XBOOLE_0:def_3;
then ( x = 0 or x = 1 ) by TARSKI:def_1;
hence x in [.(- 1),1.] by XXREAL_1:1; ::_thesis: verum
end;
the carrier of (T | (C \/ D)) = C \/ D by PRE_TOPC:8;
then A14: T | (C \/ D) = (T | C) union (T | D) by A10, A3, TSEP_1:def_2;
A15: (T --> (R^1 1)) .: D = {1}
proof
thus (T --> (R^1 1)) .: D c= {1} by A8, FUNCOP_1:81; :: according to XBOOLE_0:def_10 ::_thesis: {1} c= (T --> (R^1 1)) .: D
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {1} or y in (T --> (R^1 1)) .: D )
consider c being set such that
A16: c in D by XBOOLE_0:def_1;
assume y in {1} ; ::_thesis: y in (T --> (R^1 1)) .: D
then A17: y = 1 by TARSKI:def_1;
( dom (T --> (R^1 1)) = the carrier of T & (T --> (R^1 1)) . c = 1 ) by A8, A16, FUNCOP_1:7, FUNCOP_1:13;
hence y in (T --> (R^1 1)) .: D by A17, A16, FUNCT_1:def_6; ::_thesis: verum
end;
A18: D c= D ;
A19: (T --> (R^1 0)) .: C = {0}
proof
thus (T --> (R^1 0)) .: C c= {0} by A6, FUNCOP_1:81; :: according to XBOOLE_0:def_10 ::_thesis: {0} c= (T --> (R^1 0)) .: C
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {0} or y in (T --> (R^1 0)) .: C )
consider c being set such that
A20: c in C by XBOOLE_0:def_1;
assume y in {0} ; ::_thesis: y in (T --> (R^1 0)) .: C
then A21: y = 0 by TARSKI:def_1;
( dom (T --> (R^1 0)) = the carrier of T & (T --> (R^1 0)) . c = 0 ) by A6, A20, FUNCOP_1:7, FUNCOP_1:13;
hence y in (T --> (R^1 0)) .: C by A21, A20, FUNCT_1:def_6; ::_thesis: verum
end;
A22: C \/ D is closed by TOPS_1:9;
the carrier of (Closed-Interval-TSpace ((- 1),1)) = [.(- 1),1.] by TOPMETR:18;
then reconsider h = ((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D)) as Function of (T | (C \/ D)),(Closed-Interval-TSpace ((- 1),1)) by A14, A13, FUNCT_2:6;
((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D)) is continuous Function of ((T | C) union (T | D)),R^1 by A11, TMAP_1:136;
then h is continuous by A14, PRE_TOPC:27;
then consider g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) such that
A23: g | (C \/ D) = ((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D)) by A1, A22;
reconsider F = g as continuous Function of T,R^1 by PRE_TOPC:26, TOPREALA:7;
take F ; ::_thesis: ( F .: C = {0} & F .: D = {1} )
A24: C c= C ;
thus F .: C = (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) .: C by A23, FUNCT_2:97, XBOOLE_1:7
.= ((T --> (R^1 0)) | (T | C)) .: C by A10, A11, A24, Th14
.= ((T --> (R^1 0)) | C) .: C by A10, TMAP_1:def_3
.= {0} by A19, RELAT_1:129 ; ::_thesis: F .: D = {1}
thus F .: D = (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) .: D by A23, FUNCT_2:97, XBOOLE_1:7
.= ((T --> (R^1 1)) | (T | D)) .: D by A3, A11, A18, Th14
.= ((T --> (R^1 1)) | D) .: D by A3, TMAP_1:def_3
.= {1} by A15, RELAT_1:129 ; ::_thesis: verum
end;
hence T is normal by Th18; ::_thesis: verum
end;