The abstract of the Mizar article:

Some Facts about Union of Two Functions and Continuity of Union of Functions

by

Yatsuka Nakamura, and

Agata Darmochwal

Received November 21, 1991

MML identifier: TOPMETR2

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, RCOMP_1, BOOLE, FUNCT_1, RELAT_1, FUNCT_4, PRE_TOPC,
      SUBSET_1, COMPTS_1, ORDINAL2, EUCLID, BORSUK_1, TOPS_2, ARYTM_3, ARYTM_1,
      TOPMETR, PCOMPS_1, METRIC_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, NAT_1,
      REAL_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, STRUCT_0, PRE_TOPC, TOPS_2,
      COMPTS_1, RCOMP_1, EUCLID, METRIC_1, PCOMPS_1, TOPMETR;
 constructors REAL_1, FUNCT_4, TOPS_2, COMPTS_1, RCOMP_1, EUCLID, TOPMETR,
      MEMBERED, XBOOLE_0;
 clusters FUNCT_1, PRE_TOPC, TOPMETR, STRUCT_0, EUCLID, BORSUK_1, XREAL_0,
      METRIC_1, RELSET_1, SUBSET_1, XBOOLE_0, MEMBERED, ZFMISC_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve x,r,a,b for Real;

theorem :: TOPMETR2:1
 for x,y,z being real number holds
  x <= y & y <= z implies [. x,y .] /\ [. y,z .] = {y};

reserve f,g for Function, x1,x2 for set;

theorem :: TOPMETR2:2
f is one-to-one & g is one-to-one &
 (for x1,x2 st x1 in dom g & x2 in dom f \ dom g holds g.x1 <> f.x2) implies
  f+*g is one-to-one;

theorem :: TOPMETR2:3
f.:(dom f /\ dom g) c= rng g implies rng f \/ rng g = rng(f+*g);

 reserve T, S for non empty TopSpace, p for Point of T;

theorem :: TOPMETR2:4
 for T1,T2 being SubSpace of T,
  f being map of T1,S, g being map of T2,S st
   ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} & T1 is compact &
     T2 is compact & T is_T2 & f is continuous & g is continuous & f.p = g.p
  ex h being map of T,S st h = f+*g & h is continuous;

theorem :: TOPMETR2:5
   for T being non empty TopSpace,
     T1, T2 being SubSpace of T,
     p1,p2 being Point of T
 for f being map of T1,S, g being map of T2,S st
   ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#]
 T2) = {p1,p2} & T1 is compact &
    T2 is compact & T is_T2 & f is continuous & g is continuous &
    f.p1 = g.p1 & f.p2 = g.p2
  ex h being map of T,S st h = f+*g & h is continuous;

theorem :: TOPMETR2:6
   for n being Nat, P, Q being Subset of TOP-REAL n
 for p being Point of TOP-REAL n,
     f being map of I[01], (TOP-REAL n)|P,
     g being map of I[01], (TOP-REAL n)|Q st
      P /\
 Q = {p} & f is_homeomorphism & f.1 = p & g is_homeomorphism & g.0 = p
 ex h being map of I[01], (TOP-REAL n)|(P \/ Q) st
  h is_homeomorphism & h.0 = f.0 & h.1 = g.1;