:: Some Facts about Union of Two Functions and Continuity of Union of Functions
:: by Yatsuka Nakamura and Agata Darmochwa{\l}
::
:: Received November 21, 1991
:: Copyright (c) 1991-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, REAL_1, FUNCT_1, RELAT_1, XBOOLE_0, FUNCT_4, TARSKI,
PRE_TOPC, SUBSET_1, BORSUK_1, TOPS_2, CARD_1, ARYTM_3, XXREAL_0,
XXREAL_1, TOPMETR, STRUCT_0, ORDINAL2, RCOMP_1, ARYTM_1, PCOMPS_1,
METRIC_1, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4, STRUCT_0,
PRE_TOPC, TOPS_2, COMPTS_1, RCOMP_1, METRIC_1, PCOMPS_1, TOPMETR,
XXREAL_0;
constructors FUNCT_4, REAL_1, MEMBERED, RCOMP_1, TOPS_2, COMPTS_1, TOPMETR,
XXREAL_2, PCOMPS_1;
registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, MEMBERED, STRUCT_0,
PRE_TOPC, METRIC_1, PCOMPS_1, BORSUK_1, TOPMETR, XXREAL_2, XREAL_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin
reserve x,r,a for Real;
reserve f,g for Function,
x1,x2 for set;
theorem :: TOPMETR2:1
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:2
f.:(dom f /\ dom g) c= rng g implies rng f \/ rng g = rng(f+*g);
reserve T for T_2 TopSpace;
theorem :: TOPMETR2:3
for P, Q being Subset of T for p being Point of T, f being Function of
I[01], T|P, g being Function of I[01], T|Q st P /\ Q = {p} & f is
being_homeomorphism & f.1 = p & g is being_homeomorphism & g.0 = p ex h being
Function of I[01], T|(P \/ Q) st h is being_homeomorphism & h.0 = f.0 & h.1 = g
.1;