Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

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

by
Yatsuka Nakamura, and
Agata Darmochwal

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, (TOP-REAL n)|P,
g being map of I, (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, (TOP-REAL n)|(P \/ Q) st
h is_homeomorphism & h.0 = f.0 & h.1 = g.1;
```