:: Tietze {E}xtension {T}heorem
:: by Artur Korni{\l}owicz , Grzegorz Bancerek and Adam Naumowicz
::
:: Received September 14, 2005
:: Copyright (c) 2005-2018 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, NAT_1;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
begin
reserve r for Real,
X for set,
f, g, h for real-valued Function;
theorem :: TIETZE:1
for a,b,c being Real st |.a-b.| <= c holds b-c <= a & a <= b+c;
theorem :: TIETZE:2
f c= g implies h-f c= h-g;
theorem :: TIETZE:3
f c= g implies f-h c= g-h;
definition
let f be real-valued Function, r be Real, X be set;
pred f,X is_absolutely_bounded_by r means
:: TIETZE:def 1
for x being set st x in X /\ dom f holds |.f.x.| <= r;
end;
registration
cluster summable constant convergent for Real_Sequence;
end;
theorem :: TIETZE:4
for T1 being empty TopSpace, T2 being TopSpace for f being Function of
T1,T2 holds f is continuous;
theorem :: TIETZE:5
for f,g being summable Real_Sequence st for n being Nat
holds f.n <= g.n holds Sum f <= Sum g;
theorem :: TIETZE:6
for f being Real_Sequence st f is absolutely_summable holds
|.Sum f.| <= Sum abs f;
theorem :: TIETZE:7
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);
theorem :: TIETZE:8
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);
theorem :: TIETZE:9
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);
theorem :: TIETZE:10
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);
theorem :: TIETZE:11
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;
:: Topology
registration
let T be TopSpace, A be closed Subset of T;
cluster T|A -> closed;
end;
theorem :: TIETZE:12
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);
theorem :: TIETZE:13
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;
theorem :: TIETZE:14
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;
theorem :: TIETZE:15
f c= g & g,X is_absolutely_bounded_by r implies f,X
is_absolutely_bounded_by r;
theorem :: TIETZE:16
(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;
reserve T for non empty TopSpace,
A for closed Subset of T;
theorem :: TIETZE:17
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;
:: Urysohn Lemma, simple case
theorem :: TIETZE:18
(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;
theorem :: TIETZE:19
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.|