:: Homeomorphism between [:TOP-REAL i,TOP-REAL j:] and TOP-REAL (i+j)
:: by Artur Korni{\l}owicz
::
:: Received February 21, 1999
:: Copyright (c) 1999-2016 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, SUBSET_1, FINSEQ_1, XBOOLE_0, METRIC_1, REAL_1,
XXREAL_0, ARYTM_3, RELAT_1, TARSKI, ORDINAL4, NAT_1, ARYTM_1, FUNCT_1,
FINSEQ_2, RVSUM_1, COMPLEX1, EUCLID, SQUARE_1, STRUCT_0, ZFMISC_1,
PRE_TOPC, MCART_1, CARD_1, RELAT_2, PCOMPS_1, SETFAM_1, BORSUK_1,
RCOMP_1, T_0TOPSP, CARD_3, ORDINAL2, TOPREAL7, TOPS_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, FUNCT_1, RELSET_1,
FUNCT_2, XCMPLX_0, COMPLEX1, BINOP_1, MCART_1, ORDINAL1, NUMBERS,
XXREAL_0, DOMAIN_1, XREAL_0, REAL_1, SQUARE_1, NAT_1, FINSEQ_1, RVSUM_1,
STRUCT_0, PRE_TOPC, TOPS_2, PCOMPS_1, BORSUK_1, METRIC_1, EUCLID,
FINSEQ_2, T_0TOPSP;
constructors REAL_1, SQUARE_1, COMPLEX1, TOPS_2, BORSUK_1, T_0TOPSP, GOBOARD1,
RVSUM_1, BINOP_2, PCOMPS_1, XTUPLE_0, BINOP_1;
registrations SUBSET_1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0,
METRIC_1, PCOMPS_1, EUCLID, INT_1, VALUED_0, FINSEQ_2, RELAT_1, NAT_1,
XTUPLE_0;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin
reserve i, j, n for Element of NAT,
f, g, h, k for FinSequence of REAL,
M, N for non empty MetrSpace;
theorem :: TOPREAL7:1 :: !!! do XREAL
for a, b, c, d being Real holds max(a+c,b+d) <= max(a,b) + max(c, d);
theorem :: TOPREAL7:2
for a, b, c, d, e, f being Real st a <= b+c & d <= e+f
holds max(a,d) <= max(b,e) + max(c,f);
theorem :: TOPREAL7:3
for f, g being FinSequence holds dom g c= dom (f^g);
theorem :: TOPREAL7:4
for i being Nat for f, g being FinSequence st len f < i & i <=
len f + len g holds i - len f in dom g;
theorem :: TOPREAL7:5
for f, g, h, k being FinSequence st f^g = h^k & len f = len h &
len g = len k holds f = h & g = k;
theorem :: TOPREAL7:6
len f = len g or dom f = dom g implies len (f+g) = len f & dom (f +g) = dom f
;
theorem :: TOPREAL7:7
len f = len g or dom f = dom g implies len (f-g) = len f & dom (f -g) = dom f
;
theorem :: TOPREAL7:8
len f = len sqr f & dom f = dom sqr f;
theorem :: TOPREAL7:9
len f = len abs f & dom f = dom abs f;
theorem :: TOPREAL7:10
sqr (f^g) = sqr f ^ sqr g;
theorem :: TOPREAL7:11
abs (f^g) = abs f ^ abs g;
theorem :: TOPREAL7:12
len f = len h & len g = len k implies sqr (f^g + h^k) = sqr (f+h) ^
sqr (g +k);
theorem :: TOPREAL7:13
len f = len h & len g = len k implies abs (f^g + h^k) = abs (f+h) ^
abs ( g+k);
theorem :: TOPREAL7:14
len f = len h & len g = len k implies sqr (f^g - h^k) = sqr (f-h) ^
sqr ( g-k);
theorem :: TOPREAL7:15
len f = len h & len g = len k implies abs (f^g - h^k) = abs (f-h
) ^ abs (g-k);
theorem :: TOPREAL7:16
len f = n implies f in the carrier of Euclid n;
theorem :: TOPREAL7:17
len f = n implies f in the carrier of TOP-REAL n;
definition
let M, N be non empty MetrStruct;
func max-Prod2(M,N) -> strict MetrStruct means
:: TOPREAL7:def 1
the carrier of it = [:
the carrier of M,the carrier of N:] & for x, y being Point of it ex x1, y1
being Point of M, x2, y2 being Point of N st x = [x1,x2] & y = [y1,y2] & (the
distance of it).(x,y) = max ((the distance of M).(x1,y1),(the distance of N).(
x2,y2));
end;
registration
let M, N be non empty MetrStruct;
cluster max-Prod2(M,N) -> non empty;
end;
definition
let M, N be non empty MetrStruct, x be Point of M, y be Point of N;
redefine func [x,y] -> Element of max-Prod2(M,N);
end;
definition
let M, N be non empty MetrStruct, x be Point of max-Prod2(M,N);
redefine func x`1 -> Element of M;
redefine func x`2 -> Element of N;
end;
theorem :: TOPREAL7:18
for M, N being non empty MetrStruct, m1, m2 being Point of M, n1
, n2 being Point of N holds dist([m1,n1],[m2,n2]) = max (dist(m1,m2),dist(n1,n2
));
theorem :: TOPREAL7:19
for M, N being non empty MetrStruct, m, n being Point of max-Prod2(M,N
) holds dist(m,n) = max (dist(m`1,n`1),dist(m`2,n`2));
theorem :: TOPREAL7:20
for M, N being Reflexive non empty MetrStruct holds max-Prod2(
M,N) is Reflexive;
registration
let M, N be Reflexive non empty MetrStruct;
cluster max-Prod2(M,N) -> Reflexive;
end;
theorem :: TOPREAL7:21
for M, N being symmetric non empty MetrStruct holds max-Prod2(
M,N) is symmetric;
registration
let M, N be symmetric non empty MetrStruct;
cluster max-Prod2(M,N) -> symmetric;
end;
theorem :: TOPREAL7:22
for M, N being triangle non empty MetrStruct holds max-Prod2(M
,N) is triangle;
registration
let M, N be triangle non empty MetrStruct;
cluster max-Prod2(M,N) -> triangle;
end;
registration
let M, N be non empty MetrSpace;
cluster max-Prod2(M,N) -> discerning;
end;
theorem :: TOPREAL7:23
[:TopSpaceMetr M,TopSpaceMetr N:] = TopSpaceMetr max-Prod2(M,N);
theorem :: TOPREAL7:24
the carrier of M = the carrier of N & (for m being Point of M,
n being Point of N, r being Real st r > 0 & m = n
ex r1 being Real st r1 > 0 & Ball(n,
r1) c= Ball(m,r)) & (for m being Point of M, n being Point of N,
r being Real st r > 0 & m = n
ex r1 being Real st r1 > 0 & Ball(m,r1) c= Ball(n,r)) implies
TopSpaceMetr M = TopSpaceMetr N;
theorem :: TOPREAL7:25
[:TopSpaceMetr Euclid i,TopSpaceMetr Euclid j:],
TopSpaceMetr Euclid (i+j) are_homeomorphic;
theorem :: TOPREAL7:26
ex f be Function of [:TopSpaceMetr Euclid i,TopSpaceMetr Euclid j:],
TopSpaceMetr Euclid (i+j) st f is being_homeomorphism &
for fi,fj be FinSequence st [fi,fj] in dom f holds f.(fi,fj) = fi^fj;