Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### 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;

Back to top