:: Tietze {E}xtension {T}heorem
:: by Artur Korni{\l}owicz , Grzegorz Bancerek and Adam Naumowicz
::
:: Received September 14, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

theorem Th1: :: TIETZE:1
for a, b, c being real number st |.(a - b).| <= c holds
( b - c <= a &amp; a <= b + c )
proofend;

theorem Th2: :: TIETZE:2
for f, g, h being real-valued Function st f c= g holds
h - f c= h - g
proofend;

theorem :: TIETZE:3
for f, g, h being real-valued Function st f c= g holds
f - h c= g - h
proofend;

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 &amp; b1 is constant &amp; b1 is convergent )
proofend;
end;

theorem :: TIETZE:4
for T1 being empty TopSpace
for T2 being TopSpace
for f being Function of T1,T2 holds f is continuous
proofend;

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
proofend;

theorem Th6: :: TIETZE:6
for f being Real_Sequence st f is absolutely_summable holds
abs (Sum f) <= Sum (abs f)
proofend;

theorem Th7: :: TIETZE:7
for f being Real_Sequence
for a, r being positive real number st r < 1 &amp; ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds
( f is convergent &amp; ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) )
proofend;

theorem :: TIETZE:8
for f being Real_Sequence
for a, r being positive real number st r < 1 &amp; ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds
( lim f >= (f . 0) - (a / (1 - r)) &amp; lim f <= (f . 0) + (a / (1 - r)) )
proofend;

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 &amp; ( 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 &amp; ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) )
proofend;

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 &amp; ( 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)) &amp; (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) )
proofend;

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 &amp; ( 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 &amp; lim (F,Z) = f )
proofend;

:: Topology
registration
let T be TopSpace;
let A be closed Subset of T;
clusterT | A ->  closed ;
coherence
 T | A is closed
proofend;
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 ) &amp; ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) )
proofend;

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)
proofend;

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 ) &amp; ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) )
proofend;

theorem Th15: :: TIETZE:15
for r being real number
for X being set
for f, g being real-valued Function st f c= g &amp; g,X is_absolutely_bounded_by r holds
f,X is_absolutely_bounded_by r
proofend;

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 ) &amp; f | X = g | X &amp; f,X is_absolutely_bounded_by r holds
g,X is_absolutely_bounded_by r
proofend;

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 &amp; 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 &amp; f - g,A is_absolutely_bounded_by (2 * r) / 3 )
proofend;

:: Urysohn Lemma, simple case
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} &amp; f .: B = {1} ) ) holds
T is normal
proofend;

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 &amp; x in H &amp; ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) )
proofend;

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 &amp; ( 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
proofend;

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)) )
proofend;

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
proofend;

:: Tietze Extension Theorem
:: [WP: ] Tietze_Extension_Theorem
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
proofend;

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
proofend;