:: 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-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, 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, 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;