The abstract of the Mizar article:

Homeomorphism between [:$\cal E^i_\rm T, \cal E^j_\rm T$:] and $\cal E^i+j_\rm T$

by

Artur Kornilowicz

Received February 21, 1999

MML identifier: TOPREAL7

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, METRIC_1, SQUARE_1, RELAT_1, ARYTM_1, FUNCT_1, FINSEQ_2,
      RVSUM_1, ABSVALUE, EUCLID, PRE_TOPC, MCART_1, RELAT_2, PCOMPS_1, TARSKI,
      SETFAM_1, BORSUK_1, T_0TOPSP, SUBSET_1, ARYTM_3, COMPLEX1, RLVECT_1,
      ORDINAL2, TOPREAL7;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
      BINOP_1, MCART_1, DOMAIN_1, NUMBERS, XREAL_0, REAL_1, ABSVALUE, SQUARE_1,
      NAT_1, FINSEQ_1, RVSUM_1, FINSEQOP, STRUCT_0, PRE_TOPC, TOPS_2, PCOMPS_1,
      BORSUK_1, METRIC_1, EUCLID, FINSEQ_2, T_0TOPSP, GOBOARD1;
 constructors ABSVALUE, DOMAIN_1, FINSEQOP, GOBOARD1, INT_1, NAT_1, REAL_1,
      SEQ_1, SQUARE_1, T_0TOPSP, TOPS_2, BORSUK_1, MEMBERED;
 clusters SUBSET_1, INT_1, METRIC_1, PCOMPS_1, RELSET_1, STRUCT_0, EUCLID,
      MEMBERED;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin

reserve i, j, n for Nat,
        f, g, h, k for FinSequence of REAL,
        M, N for non empty MetrSpace;

theorem :: TOPREAL7:1
 for a, b being Real st max(a,b) <= a holds max(a,b) = a;

theorem :: TOPREAL7:2
 for a, b, c, d being Real holds max(a+c,b+d) <= max(a,b) + max(c,d);

theorem :: TOPREAL7:3
 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:4
   for f, g being FinSequence holds dom g c= dom (f^g);

theorem :: TOPREAL7:5
 for f, g being FinSequence st len f < i & i <= len f + len g holds
  i - len f in dom g;

theorem :: TOPREAL7:6
 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: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 g or dom f = dom g implies len (f-g) = len f & dom (f-g) = dom f;

theorem :: TOPREAL7:9
 len f = len sqr f & dom f = dom sqr f;

theorem :: TOPREAL7:10
 len f = len abs f & dom f = dom abs f;

theorem :: TOPREAL7:11
 sqr (f^g) = sqr f ^ sqr g;

theorem :: TOPREAL7:12
   abs (f^g) = abs f ^ abs g;

theorem :: TOPREAL7:13
   len f = len h & len g = len k implies sqr (f^g + h^k) = sqr (f+h) ^ sqr (g+k
);

theorem :: TOPREAL7:14
   len f = len h & len g = len k implies abs (f^g + h^k) = abs (f+h) ^ abs (g+k
);

theorem :: TOPREAL7:15
   len f = len h & len g = len k implies sqr (f^g - h^k) = sqr (f-h) ^ sqr (g-k
);

theorem :: TOPREAL7:16
 len f = len h & len g = len k implies abs (f^g - h^k) = abs (f-h) ^ abs (g-k);

theorem :: TOPREAL7:17
 len f = n implies f in the carrier of Euclid n;

theorem :: TOPREAL7:18
   len f = n implies f in the carrier of TOP-REAL n;

theorem :: TOPREAL7:19
 for f being FinSequence st f in the carrier of Euclid n holds len f = 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;

definition 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:20
 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:21
   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:22
 for M, N being Reflexive (non empty MetrStruct) holds
  max-Prod2(M,N) is Reflexive;

definition let M, N be Reflexive (non empty MetrStruct);
 cluster max-Prod2(M,N) -> Reflexive;
end;

theorem :: TOPREAL7:23
 for M, N being symmetric (non empty MetrStruct) holds
  max-Prod2(M,N) is symmetric;

definition let M, N be symmetric (non empty MetrStruct);
 cluster max-Prod2(M,N) -> symmetric;
end;

theorem :: TOPREAL7:24
 for M, N being triangle (non empty MetrStruct) holds
  max-Prod2(M,N) is triangle;

definition let M, N be triangle (non empty MetrStruct);
 cluster max-Prod2(M,N) -> triangle;
end;

definition let M, N be non empty MetrSpace;
 cluster max-Prod2(M,N) -> discerning;
end;

theorem :: TOPREAL7:25
 [:TopSpaceMetr M,TopSpaceMetr N:] = TopSpaceMetr max-Prod2(M,N);

theorem :: TOPREAL7:26
   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:27
   [:TOP-REAL i,TOP-REAL j:], TOP-REAL (i+j) are_homeomorphic;