:: Tietze {E}xtension {T}heorem
:: by Artur Korni{\l}owicz , Grzegorz Bancerek and Adam Naumowicz
::
:: Received September 14, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, VALUED_0, FUNCT_1, COMPLEX1, ARYTM_1, XXREAL_0, ARYTM_3,
CARD_1, NAT_1, TARSKI, RELAT_1, XBOOLE_0, SERIES_1, SEQ_2, SEQ_1,
FUNCOP_1, SUBSET_1, PRE_TOPC, ORDINAL2, CARD_3, POWER, REAL_1, PREPOWER,
NEWTON, VALUED_1, SEQFUNC, PBOOLE, PARTFUN1, RCOMP_1, SETFAM_1, STRUCT_0,
TOPMETR, LIMFUNC1, TOPS_2, XXREAL_1, TMAP_1, METRIC_1, FUNCT_2, PSCOMP_1,
TIETZE, FUNCT_7, ASYMPT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, NUMBERS, XXREAL_0,
XREAL_0, COMPLEX1, REAL_1, NAT_1, NEWTON, PREPOWER, POWER, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, VALUED_0, VALUED_1, SEQ_1, SEQ_2, FUNCT_2,
FUNCOP_1, SERIES_1, LIMFUNC1, RCOMP_1, SEQFUNC, STRUCT_0, PRE_TOPC,
TOPS_2, BORSUK_1, TOPMETR, TSEP_1, TMAP_1, PSCOMP_1, TOPREALB, METRIC_1;
constructors PROB_1, LIMFUNC1, NEWTON, PREPOWER, SERIES_1, TMAP_1, TOPREALB,
PARTFUN3, SEQFUNC, MEASURE6, PCOMPS_1, PSCOMP_1, WAYBEL18, COMSEQ_2,
REAL_1, URYSOHN3, SUPINF_2, SEQ_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2,
NUMBERS, XXREAL_0, XREAL_0, MEMBERED, NEWTON, FCONT_3, STRUCT_0,
PRE_TOPC, METRIC_1, BORSUK_1, TOPMETR, TOPREALB, VALUED_0, VALUED_1,
SEQ_4, RELAT_1, TMAP_1, PARTFUN4, SERIES_1, SEQ_1, SEQ_2;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
definitions TARSKI, XBOOLE_0, SEQFUNC, PRE_TOPC, COMPTS_1;
equalities STRUCT_0, LIMFUNC1, PROB_1;
expansions TARSKI, XBOOLE_0, SEQFUNC, BORSUK_1;
theorems PRE_TOPC, RCOMP_1, XBOOLE_0, TARSKI, FUNCT_1, RELAT_1, TOPREALB,
URYSOHN3, TSEP_1, JGRAPH_5, TOPREALA, TOPMETR, ABSVALUE, FUNCT_2,
XREAL_1, TOPS_2, SEQ_1, TMAP_1, TOPS_1, XBOOLE_1, FUNCOP_1, NEWTON,
GRFUNC_1, RFUNCT_1, SEQFUNC, METRIC_1, GOBOARD6, RSSPACE, SEQ_2, SEQ_4,
XCMPLX_1, SERIES_1, COMPLEX1, XCMPLX_0, ORDINAL1, POWER, PREPOWER, NAT_1,
UNIFORM1, MESFUNC1, RELSET_1, XXREAL_0, VALUED_0, VALUED_1, XXREAL_1,
JORDAN5A;
schemes NAT_1, RECDEF_1, FUNCT_2;
begin
reserve r for Real,
X for set,
f, g, h for real-valued Function;
theorem Th1:
for a,b,c being Real st |.a-b.| <= c holds b-c <= a & a <= b+c
proof
let a,b,c be Real;
assume
A1: |.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;
per cases;
suppose
a-b >= 0;
then |.a-b.| = a-b & a >= 0 qua Nat + b by ABSVALUE:def 1,XREAL_1:19;
hence thesis by A1,A4,XREAL_1:20,XXREAL_0:2;
end;
suppose
a-b < 0;
then
A5: |.a-b.| = -(a-b) by ABSVALUE:def 1
.= b-a;
then 0 qua Nat+a <= b by A2,XREAL_1:19;
hence thesis by A1,A3,A5,XREAL_1:12,XXREAL_0:2;
end;
end;
theorem Th2:
f c= g implies h-f c= h-g
proof
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;
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
let x be object;
assume
A5: x in dom(h-f);
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;
end;
hence thesis by A4,GRFUNC_1:2;
end;
theorem
f c= g implies f-h c= g-h
proof
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;
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
let x be object;
assume
A5: x in dom(f-h);
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;
end;
hence thesis by A4,GRFUNC_1:2;
end;
definition
let f be real-valued Function, r be Real, X be set;
pred f,X is_absolutely_bounded_by r means
for x being set st x in X /\ dom f holds |.f.x.| <= r;
end;
registration
cluster summable constant convergent for Real_Sequence;
existence
proof
take f = seq_const 0;
for n being Nat holds f.n = 0;
hence f is summable by RSSPACE:16;
thus f is constant;
thus thesis;
end;
end;
theorem
for T1 being empty TopSpace, T2 being TopSpace for f being Function of
T1,T2 holds f is continuous
proof
let T1 be empty TopSpace, T2 being TopSpace;
let f be Function of T1,T2;
let A be Subset of T2;
thus thesis;
end;
theorem
for f,g being summable Real_Sequence st for n being Nat
holds f.n <= g.n holds Sum f <= Sum g
proof
let f,g be summable Real_Sequence;
A1: Sum f = lim Partial_Sums f & Sum g = lim Partial_Sums g by SERIES_1:def 3;
assume for n being Nat holds f.n <= g.n;
then
A2: for n being 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 thesis by A1,A2,SEQ_2:18;
end;
theorem Th6:
for f being Real_Sequence st f is absolutely_summable holds
|.Sum f.| <= Sum abs f
proof
let f be Real_Sequence;
defpred P[Nat] means
(abs Partial_Sums f).$1 <= (Partial_Sums abs f).$1;
A1: now
let n be Nat;
assume P[n];
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 P[n+1] by SERIES_1:def 1;
end;
(abs Partial_Sums f).0 = |.(Partial_Sums f).0.| by SEQ_1:12
.= |.f.0.| by SERIES_1:def 1
.= (abs f).0 by SEQ_1:12;
then
A2: P[ 0 ] by SERIES_1:def 1;
A3: for n being Nat holds P[n] from NAT_1:sch 2(A2,A1);
assume
A4: f is absolutely_summable;
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 |.lim Partial_Sums f.| <= lim Partial_Sums abs f by A6,SEQ_4:14;
then |.lim Partial_Sums f.| <= Sum abs f by SERIES_1:def 3;
hence thesis by SERIES_1:def 3;
end;
theorem Th7:
for f being Real_Sequence for a,r being positive Real 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;
let a,r be positive Real;
deffunc S(Nat, Real) = In(f.($1+1)-f.$1,REAL);
consider g being sequence of REAL such that
A1: g.0 = f.0 & for n being Nat holds g.(n+1) = S(n,g.n) from NAT_1:sch
12;
now
let n be Nat;
A2: g.(n+1) = S(n,g.n) by A1;
thus f.(n+1) = f.(n+1)-f.n+f.n .= f.n+g.(n+1) by A2;
end;
then
A3: f = Partial_Sums g by A1,SERIES_1:def 1;
A4: now
let n be Nat;
(abs g).n = |.g.n.| by SEQ_1:12;
hence 0 <= (abs g).n by COMPLEX1:46;
end;
A5: |.r.| = r by COMPLEX1:43;
assume
A6: r < 1;
then
A7: r GeoSeq is summable by A5,SERIES_1:24;
assume
A8: for n being Nat holds |.f.n-f.(n+1).| <= a*(r to_power n);
A9: now
let n be Nat;
set m = 1;
assume m <= n;
then consider k being Nat such that
A10: n = 1+k by NAT_1:10;
g.n = S(k,g.k) by A1,A10;
then (abs g).n = |.f.n-f.k.| by A10,SEQ_1:12
.= |.f.k-f.n.| by COMPLEX1:60;
then
A11: (abs g).n <= a*(r to_power k) by A8,A10;
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 A10,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 A11,SEQ_1:9;
end;
(a*r")(#)(r GeoSeq) is summable by A7,SERIES_1:10;
then abs g is summable by A4,A9,SERIES_1:19;
then
A12: g is absolutely_summable by SERIES_1:def 4;
then g is summable;
hence f is convergent by A3,SERIES_1:def 2;
let n be Nat;
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
A13: now
let k be Nat;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
(abs (g^\(n9+1))).k = |.(g^\(n9+1)).k.| by SEQ_1:12;
hence 0 <= (abs (g^\(n9+1))).k by COMPLEX1:46;
(abs (g^\(n9+1))).k = |.(g^\(n9+1)).k.| by SEQ_1:12
.= |.g.(n9+1+k).| by NAT_1:def 3
.= |.S(n9+kk,g.n9).| by A1
.= |.f.(n9+k+1)-f.(n9+k).|
.= |.f.(n9+k)-f.(n9+k+1).| by UNIFORM1:11;
then (abs (g^\(n9+1))).k <= a*(r to_power (n9+kk)) by A8;
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
;
end;
A14: (a*(r to_power n))(#)(r GeoSeq) is summable by A7,SERIES_1:10;
then abs (g^\(n9+1)) is summable by A13,SERIES_1:20;
then
A15: (g^\(n9+1)) is absolutely_summable by SERIES_1:def 4;
lim f = Sum g by A3,SERIES_1:def 3;
then lim f = f.n+Sum(g^\(n9+1)) by A3,A12,SERIES_1:15;
then
A16: |.(lim f)-(f.n).| <= Sum abs (g^\(n9+1)) by A15,Th6;
A17: Sum abs (g^\(n9+1)) <= Sum ((a*(r to_power n))(#)(r GeoSeq)) by A14,A13,
SERIES_1:20;
Sum ((a*(r to_power n))(#)(r GeoSeq)) = (a*(r to_power n))*Sum (r
GeoSeq) by A7,SERIES_1:10
.= (a*(r to_power n))*(1/(1-r)) by A6,A5,SERIES_1:24
.= (a*(r to_power n))/(1-r) by XCMPLX_1:99;
hence thesis by A17,A16,XXREAL_0:2;
end;
theorem
for f being Real_Sequence for a,r being positive Real 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;
let a,r be positive Real;
assume
A1: r < 1;
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);
then |.(lim f)-(f.0).| <= a*1/(1-r) by A1,A2,Th7;
hence thesis by Th1;
end;
theorem Th9:
for X,Z being non empty set for F being Functional_Sequence of X
,REAL st Z common_on_dom F for a,r being positive Real 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;
let F be Functional_Sequence of X,REAL such that
A1: Z common_on_dom F;
Z c= dom(F.0) by A1;
then reconsider Z9 = Z as non empty Subset of X by XBOOLE_1:1;
deffunc ff(Element of Z9) = In(lim(F # $1),REAL);
let a,r be positive Real such that
A2: r < 1;
consider f being Function of Z9,REAL such that
A3: for x being Element of Z9 holds f.x = ff(x) from FUNCT_2:sch 4;
reconsider 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);
thus F is_unif_conv_on Z
proof
thus Z common_on_dom F by A1;
take f;
thus Z = dom f by FUNCT_2:def 1;
A5: 1-r > 0 by A2,XREAL_1:50;
let p be Real;
assume p > 0;
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,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;
let n be Nat, x be Element of X;
assume that
A10: n>=k and
A11: x in Z;
A12: (F.n).x = (F#x).n & |.(F.n).x - f.x.| = |.(f.x) - (F.n).x.| by COMPLEX1:60
,SEQFUNC:def 10;
now
let n be Nat;
A13: (F#x).n = (F.n).x by SEQFUNC:def 10;
A14: Z c= dom (F.(n+1)) by A1;
Z c= dom (F.n) by A1;
then x in dom (F.n) /\ dom (F.(n+1)) by A11,A14,XBOOLE_0:def 4;
then x in dom ((F.n)-(F.(n+1))) by VALUED_1:12;
then
A15: ((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 A15;
hence |.(F#x).n-(F#x).(n+1).| <= a*(r to_power n) by A13,SEQFUNC:def 10;
end;
then
A16: |.(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
A17: 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 A17,XREAL_1:72;
then
A18: |.(lim (F#x)) - ((F#x).n).| <= a*(r to_power k)/(1-r) by A16,XXREAL_0:2;
reconsider xx=x as Element of Z9 by A11;
f.x =ff(xx) by A3;
hence |.(F.n).x - f.x.| < p by A9,A18,A12,XXREAL_0:2;
end;
then
A19: F is_point_conv_on Z by SEQFUNC:22;
let n9 be Nat, z being set;
reconsider n = n9 as Element of NAT by ORDINAL1:def 12;
assume
A20: z in Z /\ dom (lim(F,Z)-(F.n9));
then reconsider x = z as Element of X;
A21: z in Z9 by A20,XBOOLE_0:def 4;
now
let n be Nat;
A22: (F#x).(n+1) = F.(n+1).x by SEQFUNC:def 10;
A23: Z c= dom (F.(n+1)) by A1;
Z c= dom (F.n) by A1;
then z in dom (F.n) /\ dom (F.(n+1)) by A21,A23,XBOOLE_0:def 4;
then
A24: x in dom ((F.n)-(F.(n+1))) by VALUED_1:12;
then
A25: x in Z /\ dom ((F.n)-(F.(n+1))) by A21,XBOOLE_0:def 4;
A26: (F.n)-(F.(n+1)), Z is_absolutely_bounded_by a*(r to_power n) by A4;
(F#x).n = (F.n).x by SEQFUNC:def 10;
then ((F.n)-(F.(n+1))).x = (F#x).n-(F#x).(n+1) by A24,A22,VALUED_1:13;
hence |.(F#x).n-(F#x).(n+1).| <= a*(r to_power n) by A25,A26;
end;
then
A27: |.(lim (F#x)) - ((F#x).n).| <= a*(r to_power n)/(1-r) by A2,Th7;
Z = dom lim(F,Z) by A19,SEQFUNC:def 13;
then |.lim(F,Z).x-(F#x).n.| <= a*(r to_power n)/(1-r) by A19,A21,A27,
SEQFUNC:def 13;
then
A28: |.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 A20,XBOOLE_0:def 4;
hence thesis by A28,VALUED_1:13;
end;
theorem Th10:
for X,Z being non empty set for F being Functional_Sequence of X
,REAL st Z common_on_dom F for a,r being positive Real st r < 1 & for
n being Nat holds (F.n)-(F.(n+1)), Z is_absolutely_bounded_by a*(r
to_power n) 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;
let F be Functional_Sequence of X,REAL;
assume
A1: Z common_on_dom F;
let a,r be positive Real;
assume
A2: r < 1;
assume
A3: for n being Nat holds (F.n)-(F.(n+1)), Z
is_absolutely_bounded_by a*(r to_power n);
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;
z in Z & Z c= dom (F.0) by A1;
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;
then |.lim(F,Z).z-(F.0).z.| <= a*1/(1-r) by A6,VALUED_1:13;
hence thesis by Th1;
end;
theorem Th11:
for X,Z being non empty set for F being Functional_Sequence of X
,REAL st Z common_on_dom F for a,r being positive Real 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;
let F be Functional_Sequence of X,REAL;
assume
A1: Z common_on_dom F;
let a,r be positive Real;
let f be Function of Z, REAL;
A2: dom f = Z by FUNCT_2:def 1;
Z c= dom (F.0) by A1;
then reconsider g = f as PartFunc of X,REAL by A2,RELSET_1:5,XBOOLE_1:1;
assume
A3: r < 1;
assume
A4: for n being Nat holds (F.n)-f, Z is_absolutely_bounded_by
a*(r to_power n);
A5: now
let x be Element of X such that
A6: x in Z;
let p be Real such that
A7: p > 0;
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,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;
reconsider k as Nat;
take k;
let n be Nat;
Z c= dom (F.n) by A1;
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;
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,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;
then |.(F.n).x - g.x.| <= a*(r to_power k)/(1-r) by A18,XXREAL_0:2;
hence |.(F.n).x - g.x.| < p by A12,XXREAL_0:2;
end;
thus
A19: F is_point_conv_on Z
proof
thus Z common_on_dom F by A1;
take g;
thus Z = dom g by FUNCT_2:def 1;
thus thesis by A5;
end;
now
let x be Element of X;
assume
A20: x in dom g;
A21: for p being Real st 0 < p ex n being Nat st for m
being Nat st n <= m holds |.(F#x).m-g.x.| < p
proof
let p be Real;
reconsider p9 = p as Real;
assume 0 < p;
then consider n being Nat such that
A22: for m being Nat st n <= m holds |.(F.m).x-g.x.| <
p9 by A2,A5,A20;
reconsider n as Nat;
take n;
let m be Nat;
(F.m).x = (F#x).m by SEQFUNC:def 10;
hence thesis by A22;
end;
F#x is convergent by A2,A19,A20,SEQFUNC:20;
hence g.x = lim(F#x) by A21,SEQ_2:def 7;
end;
hence thesis by A2,A19,SEQFUNC:def 13;
end;
:: Topology
registration
let T be TopSpace, A be closed Subset of T;
cluster T|A -> closed;
coherence
by PRE_TOPC:8;
end;
theorem Th12:
for X, Y being non empty TopSpace, X1, X2 being non empty
SubSpace of X for f1 being Function of X1,Y, f2 being Function of X2,Y st X1
misses X2 or f1|(X1 meet X2) = f2|(X1 meet X2) 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, X1, X2 be non empty SubSpace of X;
let f1 be Function of X1,Y, f2 be Function of X2,Y;
assume
A1: X1 misses X2 or f1|(X1 meet X2) = f2|(X1 meet X2);
let x be Point of X;
set F = f1 union f2;
A2: X1 is SubSpace of X1 union X2 by TSEP_1:22;
hereby
assume x in the carrier of X1;
hence F.x = (F|the carrier of X1).x by FUNCT_1:49
.= (F|X1).x by A2,TMAP_1:def 5
.= f1.x by A1,TMAP_1:def 12;
end;
A3: X2 is SubSpace of X1 union X2 by TSEP_1:22;
assume x in the carrier of X2;
hence F.x = (F|the carrier of X2).x by FUNCT_1:49
.= (F|X2).x by A3,TMAP_1:def 5
.= f2.x by A1,TMAP_1:def 12;
end;
theorem Th13:
for X, Y being non empty TopSpace, X1, X2 being non empty
SubSpace of X for f1 being Function of X1,Y, 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, X1, X2 be non empty SubSpace of X;
let f1 be Function of X1,Y, f2 be Function of X2,Y;
set F = f1 union f2;
assume
A1: X1 misses X2 or f1|(X1 meet X2) = f2|(X1 meet X2);
thus rng F c= rng f1 \/ rng f2
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 object;
A4: the carrier of X1 = dom f1 by FUNCT_2:def 1;
assume y in rng F;
then consider x being object such that
A5: x in dom F and
A6: F.x = y by FUNCT_1:def 3;
A7: x is Point of X by A5,PRE_TOPC:25;
per cases by A5,A2,XBOOLE_0:def 3;
suppose
x in the carrier of X1;
then f1.x in rng f1 & F.x = f1.x by A1,A4,A7,Th12,FUNCT_1:def 3;
hence thesis by A6,XBOOLE_0:def 3;
end;
suppose
x in the carrier of X2;
then f2.x in rng f2 & F.x = f2.x by A1,A3,A7,Th12,FUNCT_1:def 3;
hence thesis by A6,XBOOLE_0:def 3;
end;
end;
end;
theorem Th14:
for X, Y being non empty TopSpace, X1, X2 being non empty
SubSpace of X for f1 being Function of X1,Y, 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, X1, X2 be non empty SubSpace of X;
let f1 be Function of X1,Y, f2 be Function of X2,Y;
assume
A1: X1 misses X2 or f1|(X1 meet X2) = f2|(X1 meet X2);
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
let A be Subset of X1;
thus (f1 union f2).:A = f1.:A
proof
hereby
let y be object;
assume y in (f1 union f2).:A;
then consider x being Element of X1 union X2 such that
A3: x in A and
A4: y = F.x by FUNCT_2:65;
x is Point of X by PRE_TOPC:25;
then F.x = f1.x by A1,A3,Th12;
hence y in f1.:A by A3,A4,FUNCT_2:35;
end;
let y be object;
assume y in f1.: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: F.x = f1.x by A1,Th12;
x in the carrier of X1 union X2 by A2,XBOOLE_0:def 3;
hence thesis by A5,A6,FUNCT_2:35;
end;
end;
let A be Subset of X2;
hereby
let y be object;
assume y in (f1 union f2).:A;
then consider x being Element of X1 union X2 such that
A7: x in A and
A8: y = F.x by FUNCT_2:65;
x is Point of X by PRE_TOPC:25;
then F.x = f2.x by A1,A7,Th12;
hence y in f2.:A by A7,A8,FUNCT_2:35;
end;
let y be object;
assume y in 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: F.x = f2.x by A1,Th12;
x in the carrier of X1 union X2 by A2,XBOOLE_0:def 3;
hence thesis by A9,A10,FUNCT_2:35;
end;
theorem Th15:
f c= g & g,X is_absolutely_bounded_by r implies f,X
is_absolutely_bounded_by r
proof
assume that
A1: f c= g and
A2: g,X is_absolutely_bounded_by r;
let x be set;
assume
A3: x in X /\ dom f;
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 |.g.x.| <= r by A2;
hence thesis by A1,A4,GRFUNC_1:2;
end;
theorem Th16:
(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
proof
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;
let x be set;
assume
A4: x in X /\ dom g;
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 thesis by A3,A6;
end;
reserve T for non empty TopSpace,
A for closed Subset of T;
theorem Th17:
r > 0 & T is normal implies for f being continuous Function of T
|A, R^1 st f,A is_absolutely_bounded_by r 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
assume that
A1: r > 0 and
A2: T is normal;
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 such that
A3: for x being set st x in A /\ dom f holds |.f.x.| <= r;
reconsider r1 = r as Real;
set e = 2*r1/3;
0 < 2*r by A1,XREAL_1:129;
then e > 0 by XREAL_1:139;
then consider h being Function of Closed-Interval-TSpace(0,1),
Closed-Interval-TSpace(e*0+-r1/3,e*1+-r1/3) such that
A4: h is being_homeomorphism and
A5: for w being Real st w in [. 0,1 .] holds h.w = e*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"C1 is closed & f"C2 is closed by PRE_TOPC:def 6;
then reconsider D1 = f"C1, D2 = f"C2 as closed Subset of T by PRE_TOPC:11
,TSEP_1:12;
A8: A1 = C1 by TOPREALB:def 3;
A9: A2 = C2 by TOPREALB:def 3;
A10: --r/3 > 0 by A1,XREAL_1:139;
then f"A1 misses f"A2 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 object;
assume y in rng F;
then consider x being object 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 thesis by A15,XXREAL_1:1;
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 g1 c= the carrier of Closed-Interval-TSpace(-r/3,r/3)
by RELAT_1:def 19;
dom F = the carrier of T & dom h = the carrier of
Closed-Interval-TSpace(0,1 ) by FUNCT_2:def 1;
then
A18: dom g1 = the carrier of T by A7,A13,RELAT_1:27;
then reconsider g1 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 as continuous Function of T, R^1 by A6,PRE_TOPC:26;
take g;
A19: rng g1 c= the carrier of Closed-Interval-TSpace(-r/3,r/3);
thus g,dom g is_absolutely_bounded_by r/3
proof
let x be set;
assume x in dom g /\ dom g;
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 thesis by ABSVALUE:5;
end;
thus f-g,A is_absolutely_bounded_by 2*r/3
proof
A20: 1 in [. 0,1 .] by XXREAL_1:1;
A21: 0 in [. 0,1 .] by XXREAL_1:1;
let x be set such that
A22: x in A /\ dom(f-g);
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: |.f.x.| <= r by A3;
then
A27: -r <= f.x by ABSVALUE:5;
per cases;
suppose
A28: f.x <= -r/3;
then f.x in A1 by XXREAL_1:234;
then x in f"A1 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 thesis by A1,A24,A29,A30,ABSVALUE:5;
end;
suppose
A31: r/3 <= f.x;
then f.x in A2 by XXREAL_1:236;
then x in f"A2 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 thesis by A24,A32,A33,ABSVALUE:5;
end;
suppose
A34: -r/3 < f.x & f.x < 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 thesis by A24,A36,ABSVALUE:5;
end;
end;
end;
:: Urysohn Lemma, simple case
theorem Th18:
(for A, B being non empty closed Subset of T st A misses B ex f
being continuous Function of T, R^1 st f.:A = {0} & f.:B = {1}) implies T is
normal
proof
assume
A1: for A, B being non empty closed Subset of T st A misses B ex f being
continuous Function of T, R^1 st f.:A = {0} & f.:B = {1};
let W, V be Subset of T;
assume W <> {} & V <> {} & W is closed & V is closed & W misses V;
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 P, Q;
[#]R^1 <> {};
hence P is open & Q is open by TOPS_2:43;
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= P
proof
let a be object;
A6: 0 in left_open_halfline(1/2) by XXREAL_1:233;
assume
A7: a in W;
then f.a in f.:W by FUNCT_2:35;
then f.a = 0 by A2,TARSKI:def 1;
hence thesis by A4,A5,A7,A6,FUNCT_1:def 7;
end;
A8: R^1(right_open_halfline(1/2)) = right_open_halfline(1/2) by TOPREALB:def 3;
thus V c= Q
proof
let a be object;
A9: 1 in right_open_halfline(1/2) by XXREAL_1:235;
assume
A10: a in V;
then f.a in f.:V by FUNCT_2:35;
then f.a = 1 by A3,TARSKI:def 1;
hence thesis by A8,A5,A10,A9,FUNCT_1:def 7;
end;
thus thesis by A4,A8,FUNCT_1:71,XXREAL_1:275;
end;
theorem Th19:
for f being Function of T,R^1, x being Point of T holds f
is_continuous_at x iff for e being Real st e>0 ex H being Subset of T st
H is open & x in H & for y being Point of T st y in H holds |.f.y-f.x.|<e
proof
let f be Function of T,R^1, x be Point of T;
thus f is_continuous_at x implies for e being Real st e>0 ex H being
Subset of T st H is open & x in H & for y being Point of T st y in H
holds |.f.y-f.x.|<e
proof
reconsider fx=f.x as Point of RealSpace by TOPMETR:12,def 6;
assume
A1: f is_continuous_at x;
let e be Real such that
A2: e>0;
reconsider G=Ball(fx,e) as Subset of R^1 by TOPMETR:12,def 6;
G is open & fx in G by A2,GOBOARD6:1,TOPMETR:14,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;
thus H is open & x in H by A3;
A5: dom f=the carrier of T by FUNCT_2:def 1;
let y be Point of T;
assume y in H;
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 thesis by TOPMETR:11;
end;
assume
A7: for e being Real st e>0 ex H being Subset of T st H is open
& x in H & for y being Point of T st y in H holds |.f.y-f.x.|<e;
now
reconsider fx=f.x as Point of RealSpace by TOPMETR:12,def 6;
let G be Subset of R^1;
assume G is open & f.x in G;
then consider r being Real such that
A8: r>0 and
A9: Ball(fx,r) c= G by TOPMETR:15,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 |.f.y-f.x.|<r by A7,A8;
take H;
thus H is open & x in H by A10;
thus f.:H c= G
proof
let a be object;
assume a in f.:H;
then consider y being object such that
A12: y in dom f and
A13: y in H and
A14: a=f.y by FUNCT_1:def 6;
reconsider y as Point of T by A12;
reconsider fy=f.y as Point of RealSpace by TOPMETR:12,def 6;
|.f.y-f.x.|<r by A11,A13;
then |.-(f.y-f.x).|< r by COMPLEX1:52;
then |.f.x-f.y.|<r;
then dist(fx,fy)<r by TOPMETR:11;
then fy in Ball(fx,r) by METRIC_1:11;
hence thesis by A9,A14;
end;
end;
hence thesis by TMAP_1:43;
end;
theorem Th20:
for F being Functional_Sequence of the carrier of T, REAL st F
is_unif_conv_on the carrier of T & for i being 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 F be Functional_Sequence of the carrier of T, REAL such that
A1: F is_unif_conv_on the carrier of T and
A2: for i being Nat holds F.i 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
let p be Point of T;
now
let e be Real such that
A3: e>0;
reconsider e3=e/3 as Real;
A4: e3>0 by A3,XREAL_1:139;
then consider k being Nat such that
A5: for n being Nat for x being Point of T st n>=k & x in
the carrier of T holds |.(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: |.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 |.Fk.y-Fk.p.|<e3 by A4,Th19;
take H;
thus H is open & p in H by A7;
let y be Point of T such that
A9: y in H;
|.Fk.y-l.y.|<e3 by A5;
then |.-(Fk.y-l.y).|<e3 by COMPLEX1:52;
then
|.(Fk.p-l.p)+(-Fk.y+l.y).| <= |.Fk.p-l.p.|+|.-(Fk.y-l.y).| &
|.Fk.p-l.p.|+|.-(Fk.y-l.y).| < e3+e3 by A6,COMPLEX1:56,XREAL_1:8;
then |.(Fk.p-l.p)+(-Fk.y+l.y).| < 2*e3 by XXREAL_0:2;
then
|.Fk.y-Fk.p+((Fk.p-l.p)+(-Fk.y+l.y)).| <= |.Fk.y-Fk.p.|+
|.(Fk.p-l.p)+(-Fk .y+l.y).| &
|.Fk.y-Fk.p.|+|.(Fk.p-l.p)+(-Fk.y+l.y).| < e3+2*e3 by
A8,A9,COMPLEX1:56,XREAL_1:8;
hence |.l.y-l.p.|<e by XXREAL_0:2;
end;
hence l is_continuous_at p by Th19;
end;
hence thesis by TMAP_1:44;
end;
theorem Th21:
for T being non empty TopSpace for f being Function of T, R^1
for r being positive Real 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;
let f be Function of T, R^1;
let r be positive Real;
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)
proof
assume
A2: f, the carrier of T is_absolutely_bounded_by r;
now
let x be object;
assume x in the carrier of T;
then x in (the carrier of T) /\ dom f by A1;
then |.f.x.|<=r by A2;
then 2*|.f.x.|<=2*r by XREAL_1:64;
then |.2.|*|.f.x.|<=2*r by ABSVALUE:def 1;
then |.-2.|*|.f.x.|<=2*r by COMPLEX1:52;
then |.(-2)*f.x.|<=r--r by COMPLEX1:65;
then |.-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;
end;
hence thesis by A1,FUNCT_2:3;
end;
assume
A3: f is Function of T, Closed-Interval-TSpace(-r,r);
let x be set;
assume x in (the carrier of T) /\ dom f;
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 |.-r+r-2*f.x.|<=r--r by RCOMP_1:2;
then |.(-2)*f.x.|<=r--r;
then |.-2.|*|.f.x.|<=2*r by COMPLEX1:65;
then |.2.|*|.f.x.|<=2*r by COMPLEX1:52;
then 2*|.f.x.|<=2*r by ABSVALUE:def 1;
then (2*|.f.x.|)/2<=(2*r)/2 by XREAL_1:72;
hence thesis;
end;
theorem Th22:
f-g, X is_absolutely_bounded_by r implies g-f, X is_absolutely_bounded_by r
proof
assume
A1: f-g, X is_absolutely_bounded_by r;
let x be set;
assume
A2: x in X /\ dom (g-f);
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 |.(f-g).x.| <= r by A1,A2;
then |.f.x-g.x.| <= r by A4,A3,VALUED_1:13;
then |.-(f.x-g.x).| <= r by COMPLEX1:52;
then |.g.x-f.x.| <= r;
hence thesis by A3,VALUED_1:13;
end;
::$N Tietze extension theorem
::$L https://en.wikipedia.org/wiki/Tietze_extension_theorem Tietze extension theorem
theorem
T is normal implies
for A for f being Function of T|A,Closed-Interval-TSpace(-1,1)
st f is continuous
ex g being continuous Function of T, Closed-Interval-TSpace(-1,1) st g|A = f
proof
assume
A1: T is normal;
let A;
let f be Function of T|A, Closed-Interval-TSpace(-1,1) such that
A2: f is continuous;
A3: the carrier of T|A = A by PRE_TOPC:8;
A4: the carrier of Closed-Interval-TSpace(-1,1) = [. -1,1 .] by TOPMETR:18;
per cases;
suppose
A is empty;
then reconsider A1 = A as empty Subset of T;
set g = T --> R^1(0);
g = (the carrier of T) --> 0 by TOPREALB:def 2;
then
A5: rng g = {0} by FUNCOP_1:8;
rng g c= the carrier of Closed-Interval-TSpace(-1,1)
proof
let y be object;
assume y in rng g;
then y = 0 by A5,TARSKI:def 1;
hence thesis by A4,XXREAL_1:1;
end;
then reconsider g as Function of T, Closed-Interval-TSpace(-1,1) by
FUNCT_2:6;
reconsider g as continuous Function of T, Closed-Interval-TSpace(-1,1) by
PRE_TOPC:27;
take g;
g|A1 is empty;
hence thesis;
end;
suppose
A is non empty;
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 DF: q is continuous Function of T,R^1};
reconsider f1 = f as Function of T|A1,R^1 by TOPREALA:7;
defpred Z[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 DF by FUNCT_2:8;
then T --> R^1(0) in D;
then reconsider D as non empty set;
f1,A is_absolutely_bounded_by 1
proof
let x be set;
assume x in A /\ dom f1;
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 thesis by ABSVALUE:5;
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 DF by FUNCT_2:8;
then g0 in D;
then reconsider g0d = g0 as Element of D;
A10: for n being Nat for x being Element of D ex y being
Element of D st Z[n,x,y]
proof
let n be Nat, x be Element of D;
x in D;
then consider E2 being Element of DF such that
A11: E2 = x and
A12: E2 is continuous Function of T, R^1;
reconsider E2 as continuous Function of T, R^1 by A12;
per cases;
suppose
A13: not f-E2,A is_absolutely_bounded_by 2/3*(2/3)|^n;
take x, E2;
thus thesis by A11,A13;
end;
suppose
A14: f-E2,A is_absolutely_bounded_by 2/3*(2/3)|^n;
reconsider E2b = E2|A as Function of T|A1, R^1 by PRE_TOPC:9;
reconsider 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 as continuous RealMap of T by JORDAN5A:27;
f1c - E2c is continuous RealMap of T|A1;
then reconsider k as continuous Function of T|A1, R^1
by JORDAN5A:27,TOPMETR:17;
reconsider f1c, 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 r > (2/3)*0 by XREAL_1:68;
then r > 0;
then consider g being continuous Function of T, R^1 such that
A17: g,dom g is_absolutely_bounded_by r/3 and
A18: k-g,A is_absolutely_bounded_by 2*r/3 by A1,A15,Th17;
reconsider ga = g as RealMap of T by TOPMETR:17;
reconsider ga as continuous RealMap of T by JORDAN5A:27;
set y = E2a+ga;
reconsider y1 = y as continuous Function of T, R^1
by JORDAN5A:27,TOPMETR:17;
y1 in DF & y1 is continuous Function of T, R^1 by FUNCT_2:8;
then y in D;
then reconsider y as Element of D;
take y, E2;
thus E2 = x by A11;
assume f-E2,A is_absolutely_bounded_by 2/3*(2/3)|^n;
take g;
thus y = E2+g;
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;
A20: dom g = the carrier of T by FUNCT_2:def 1;
A21: (f-E2b-g)|A = ((f-E2b)|A) - g by RFUNCT_1:47
.= f - E2b|A - g
.= f - E2|A - g
.= (f-E2)|A - g by RFUNCT_1:47
.= (f-E2-g)|A by RFUNCT_1:47;
dom(f-E2b-g) = dom(f-E2b) /\ dom g by VALUED_1:12
.= dom f /\ dom E2b /\ dom g by VALUED_1:12
.= A by A3,A16,A20,XBOOLE_1:28;
hence thesis by A18,A19,A21,Th16;
end;
end;
consider F being sequence of D such that
A22: F.0 = g0d and
A23: for n being Nat holds Z[n,F.n,F.(n+1)] from RECDEF_1:
sch 2(A10);
A24: now
let n be Nat;
Z[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,def 6;
end;
dom F = NAT by FUNCT_2:def 1;
then reconsider 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 qua Nat+1) = E2+g & g,the carrier of T
is_absolutely_bounded_by 1/3*(2/3)|^(0 qua Nat+1) & f-E2-g,A
is_absolutely_bounded_by 2/3*(2/3)|^(0 qua Nat+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 qua Nat+1) = E2+g1 and
A28: g1,the carrier of T is_absolutely_bounded_by 1/3*(2/3)|^(0 qua Nat+ 1) and
f-E2-g1,A is_absolutely_bounded_by 2/3*(2/3)|^(0 qua Nat+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 P[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
let n be Nat;
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 P[n];
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,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
let a be object;
assume
A41: a in 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;
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,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
let a be object;
assume
A47: a in dom gx;
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;
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 P[n+1]
by A33,A43,A45,A48,Th22,JORDAN5A:27,METRIC_1:def 13,TOPMETR:12,def 6;
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
let a be object;
assume
A50: a in dom g1;
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;
end;
then
A51: F.(0 qua Nat+1)-F.0 = g1 by A25,A27,A49,FUNCT_1:2;
(2/3) to_power 0 = 1 & 1/3*(2/3)|^1 = 1/3*(2/3) by POWER:24;
then
A52: P[ 0 ] by A9,A22,A28,A51,Th22;
A53: for n being Nat holds P[n] from NAT_1:sch 2(A52,A30);
A54: for n being Nat holds
(F.n)-(F.(n+1)), the carrier of T is_absolutely_bounded_by (2/9)*((
2/3) to_power n) by A53;
dom f = the carrier of T|A1 & rng f c= REAL by FUNCT_2:def 1,VALUED_0:def 3
;
then
A55: f is Function of A1,REAL by A3,FUNCT_2:2;
now
let n be Nat;
Z[n,F.n,F.(n+1)] by A23;
hence the carrier of T c= dom(F.n) by FUNCT_2:def 1;
end;
then
A56: the carrier of T common_on_dom F;
then
A57: A1 common_on_dom F by SEQFUNC:23;
A58: for n being Nat holds
(F.n)-f, A1 is_absolutely_bounded_by (2/3)*((2/3) to_power n) by A53;
A59: 2/9 > 0;
then F is_unif_conv_on the carrier of T by A56,A6,A54,Th9;
then reconsider
h = lim(F, the carrier of T) as continuous Function of T, R^1
by A53,Th20;
F is_point_conv_on the carrier of T by A56,A59,A6,A54,Th9,SEQFUNC:22;
then
A60: h|A1 = lim(F, A1) by SEQFUNC:24
.= f by A6,A58,A57,A55,Th11;
h, the carrier of T is_absolutely_bounded_by 1
proof
let x be set;
assume x in (the carrier of T) /\ dom h;
then reconsider z = x as Element of T;
A61: dom (F.0) = the carrier of T by A22,FUNCT_2:def 1;
A62: |.F.0 .z.| <= 1/3 by A8,A22,A61;
then F.0 .z >= -1/3 by ABSVALUE:5;
then
A63: F.0 .z-(2/9)/(1-2/3) >= -1/3-(2/9)/(1-2/3) by XREAL_1:9;
F.0 .z <= 1/3 by A62,ABSVALUE:5;
then
A64: F.0 .z+(2/9)/(1-2/3) <= 1/3+(2/9)/(1-2/3) by XREAL_1:7;
h.z <= F.0 .z+(2/9)/(1-2/3) by A56,A59,A6,A54,Th10;
then
A65: h.z <= 1 by A64,XXREAL_0:2;
h.z >= F.0 .z-(2/9)/(1-2/3) by A56,A59,A6,A54,Th10;
then h.z >= -1 by A63,XXREAL_0:2;
hence thesis by A65,ABSVALUE:5;
end;
then reconsider 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 thesis by A60;
end;
end;
theorem
(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
proof
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;
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 being non empty closed Subset of T such that
A2: C misses D;
set g1 = f1|(T|C), g2 = f2|(T|D);
set f = g1 union g2;
A3: the carrier of T|D = D by PRE_TOPC:8;
g2 = f2|the carrier of T|D by TMAP_1:def 4;
then
A4: rng g2 c= rng f2 by RELAT_1:70;
g1 = f1|the carrier of T|C by TMAP_1:def 4;
then rng g1 c= rng f1 by RELAT_1:70;
then
A5: rng g1 \/ rng g2 c= rng f1 \/ rng f2 by A4,XBOOLE_1:13;
A6: f1 = (the carrier of T) --> 0 by TOPREALB:def 2;
then
A7: rng f1 = {0} by FUNCOP_1:8;
A8: f2 = (the carrier of T) --> 1 by TOPREALB:def 2;
then
A9: rng f2 = {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 f c= rng g1 \/ rng g2 by Th13;
then
A12: rng f c= rng f1 \/ rng f2 by A5;
A13: rng f c= [. -1,1 .]
proof
let x be object;
assume x in rng f;
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 thesis by XXREAL_1:1;
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: f2.:D = {1}
proof
thus f2.:D c= {1} by A8,FUNCOP_1:81;
let y be object;
consider c being object such that
A16: c in D by XBOOLE_0:def 1;
assume y in {1};
then
A17: y = 1 by TARSKI:def 1;
dom f2 = the carrier of T & f2.c = 1 by A8,A16,FUNCOP_1:7,13;
hence thesis by A17,A16,FUNCT_1:def 6;
end;
A18: f1.:C = {0}
proof
thus f1.:C c= {0} by A6,FUNCOP_1:81;
let y be object;
consider c being object such that
A19: c in C by XBOOLE_0:def 1;
assume y in {0};
then
A20: y = 0 by TARSKI:def 1;
dom f1 = the carrier of T & f1.c = 0 by A6,A19,FUNCOP_1:7,13;
hence thesis by A20,A19,FUNCT_1:def 6;
end;
A21: C \/ D is closed by TOPS_1:9;
the carrier of Closed-Interval-TSpace(-1,1) = [. -1,1 .] by TOPMETR:18;
then reconsider
h = f as Function of T|(C\/D), Closed-Interval-TSpace(-1,1) by A14,A13,
FUNCT_2:6;
f 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
A22: g|(C\/D) = f by A1,A21;
reconsider F = g as continuous Function of T, R^1 by PRE_TOPC:26,TOPREALA:7
;
take F;
thus F.:C = f.:C by A22,FUNCT_2:97,XBOOLE_1:7
.= g1.:C by A10,A11,Th14
.= (f1|C).:C by A10,TMAP_1:def 3
.= {0} by A18,RELAT_1:129;
thus F.:D = f.:D by A22,FUNCT_2:97,XBOOLE_1:7
.= g2.:D by A3,A11,Th14
.= (f2|D).:D by A3,TMAP_1:def 3
.= {1} by A15,RELAT_1:129;
end;
hence thesis by Th18;
end;