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


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.|<e;

theorem :: TIETZE:20
  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;

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

theorem :: TIETZE:22
  f-g, X is_absolutely_bounded_by r implies g-f, X is_absolutely_bounded_by r;

:: Tietze Extension Theorem

::$N Tietze extension theorem
theorem :: TIETZE:23
  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;

theorem :: TIETZE:24
  (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;