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


theorem Th1: :: TIETZE:1
for a, b, c being Real st |.(a - b).| <= c holds
( b - c <= a & a <= b + c )
proof end;

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

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

definition
let f be real-valued Function;
let r be Real;
let 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;

:: deftheorem defines is_absolutely_bounded_by TIETZE:def 1 :
for f being real-valued Function
for r being Real
for X being set holds
( f,X is_absolutely_bounded_by r iff for x being set st x in X /\ (dom f) holds
|.(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 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 end;

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
proof end;

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

theorem Th7: :: 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) ) )
proof end;

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)) )
proof 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 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 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 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 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
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 end;

:: Topology
registration
let T be TopSpace;
let A be closed Subset of T;
cluster T | A -> closed ;
coherence
T | A is closed by PRE_TOPC:8;
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 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 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 end;

theorem Th15: :: TIETZE:15
for r being Real
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 end;

theorem Th16: :: TIETZE:16
for r being Real
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 end;

theorem Th17: :: TIETZE:17
for r being Real
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 end;

:: 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} & f .: B = {1} ) ) holds
T is normal
proof 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 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
|.((f . y) - (f . x)).| < e ) ) )
proof 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 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 end;

theorem Th21: :: TIETZE:21
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 end;

theorem Th22: :: TIETZE:22
for r being Real
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 end;

:: 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
proof 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 end;