:: by Artur Korni{\l}owicz , Grzegorz Bancerek and Adam Naumowicz

::

:: Received September 14, 2005

:: Copyright (c) 2005-2021 Association of Mizar Users

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

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

ex b_{1} being Real_Sequence st

( b_{1} is summable & b_{1} is constant & b_{1} is convergent )
end;

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 b

( b

proof end;

theorem :: TIETZE:4

for T1 being empty TopSpace

for T2 being TopSpace

for f being Function of T1,T2 holds f is continuous

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

Sum f <= Sum g

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

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

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

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

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 )

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

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)

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

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

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

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 )

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

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

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

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

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

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;

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

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

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;