:: 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-2026 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;
definitions TARSKI, FUNCT_1, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_2, T_0TOPSP,
XBOOLE_0;
equalities STRUCT_0, METRIC_1, XBOOLE_0, EUCLID, BINOP_1;
expansions TARSKI, METRIC_1, PRE_TOPC;
theorems BINOP_1, BORSUK_1, EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCT_1,
FUNCT_2, INT_1, MCART_1, METRIC_1, NAT_1, PCOMPS_1, RVSUM_1, SQUARE_1,
TARSKI, TBSP_1, TOPMETR, TOPREAL3, TOPREAL6, TOPS_2, ZFMISC_1, XREAL_1,
XXREAL_0, ORDINAL1, VALUED_1, CARD_1, XTUPLE_0, XREAL_0;
schemes BINOP_1;
begin
reserve i, j, n for Element of NAT,
f, g, h, k for FinSequence of REAL,
M, N for non empty MetrSpace;
theorem Th1: :: !!! do XREAL
for a, b, c, d being Real holds max(a+c,b+d) <= max(a,b) + max(c, d)
proof
let a, b, c, d be Real;
b <= max(a,b) & d <= max(c,d) by XXREAL_0:25;
then
A1: b+d <= max(a,b) + max(c,d) by XREAL_1:7;
a <= max(a,b) & c <= max(c,d) by XXREAL_0:25;
then a+c <= max(a,b) + max(c,d) by XREAL_1:7;
hence thesis by A1,XXREAL_0:28;
end;
theorem Th2:
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)
proof
let a, b, c, d, e, f be Real;
assume a <= b+c & d <= e+f;
then
A1: max(a,d) <= max(b+c,e+f) by XXREAL_0:26;
max(b+c,e+f) <= max(b,e) + max(c,f) by Th1;
hence thesis by A1,XXREAL_0:2;
end;
theorem
for f, g being FinSequence holds dom g c= dom (f^g)
proof
let f, g be FinSequence;
len g <= len f + len g by NAT_1:11;
then Seg len g c= Seg (len f + len g) by FINSEQ_1:5;
then dom g c= Seg (len f + len g) by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 7;
end;
theorem Th4:
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
proof
let i be Nat;
let f, g be FinSequence such that
A1: len f < i and
A2: i <= len f + len g;
A3: i-len f is Element of NAT by A1,INT_1:5;
A4: i-len f <= len f + len g - len f by A2,XREAL_1:9;
i-len f > len f-len f by A1,XREAL_1:14;
then 1 <= i-len f by A3,NAT_1:14;
hence thesis by A3,A4,FINSEQ_3:25;
end;
theorem Th5:
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
proof
let f, g, h, k be FinSequence such that
A1: f^g = h^k and
A2: len f = len h and
A3: len g = len k;
A4: for i be Nat st 1 <= i & i <= len f holds f.i = h.i
proof
let i be Nat;
assume
A5: 1 <= i & i <= len f;
then
A6: i in dom h by A2,FINSEQ_3:25;
i in dom f by A5,FINSEQ_3:25;
hence f.i = (f^g).i by FINSEQ_1:def 7
.= h.i by A1,A6,FINSEQ_1:def 7;
end;
for i be Nat st 1 <= i & i <= len g holds g.i = k.i
proof
let i be Nat;
assume
A7: 1 <= i & i <= len g;
then
A8: i in dom k by A3,FINSEQ_3:25;
i in dom g by A7,FINSEQ_3:25;
hence g.i = (f^g).(len f +i) by FINSEQ_1:def 7
.= k.i by A1,A2,A8,FINSEQ_1:def 7;
end;
hence thesis by A2,A3,A4,FINSEQ_1:14;
end;
theorem Th6:
len f = len g or dom f = dom g implies len (f+g) = len f & dom (f +g) = dom f
proof
reconsider f1 = f as Element of (len f)-tuples_on REAL by FINSEQ_2:92;
assume len f = len g or dom f = dom g;
then len f = len g by FINSEQ_3:29;
then reconsider g1 = g as Element of (len f)-tuples_on REAL by FINSEQ_2:92;
f1+g1 is Element of (len f)-tuples_on REAL;
hence len (f+g) = len f by CARD_1:def 7;
hence thesis by FINSEQ_3:29;
end;
theorem Th7:
len f = len g or dom f = dom g implies len (f-g) = len f & dom (f -g) = dom f
proof
reconsider f1 = f as Element of (len f)-tuples_on REAL by FINSEQ_2:92;
assume len f = len g or dom f = dom g;
then len f = len g by FINSEQ_3:29;
then reconsider g1 = g as Element of (len f)-tuples_on REAL by FINSEQ_2:92;
f1-g1 is Element of (len f)-tuples_on REAL;
hence len (f-g) = len f by CARD_1:def 7;
hence thesis by FINSEQ_3:29;
end;
theorem Th8:
len f = len sqr f & dom f = dom sqr f by RVSUM_1:143;
theorem Th9:
len f = len abs f & dom f = dom abs f
proof
rng f c= REAL & dom absreal = REAL by FUNCT_2:def 1;
hence len f = len abs f by FINSEQ_2:29;
hence thesis by FINSEQ_3:29;
end;
theorem Th10:
sqr (f^g) = sqr f ^ sqr g by RVSUM_1:144;
theorem
abs (f^g) = abs f ^ abs g
proof
A1: len g = len abs g & len(f^g) = len f + len g by Th9,FINSEQ_1:22;
A2: len abs (f^g) = len (f^g) by Th9;
A3: len f = len abs f by Th9;
A4: for i be Nat st 1 <= i & i <= len abs (f^g) holds (abs (f^g)).i = (abs f
^ abs g).i
proof
let i be Nat;
assume that
A5: 1 <= i and
A6: i <= len abs (f^g);
reconsider i1=i as Element of NAT by ORDINAL1:def 12;
A7: i in dom (f^g) by A2,A5,A6,FINSEQ_3:25;
per cases;
suppose
A8: i in dom f;
then
A9: i in dom abs f by Th9;
thus (abs (f^g)).i = absreal.((f^g).i) by A7,FUNCT_1:13
.= absreal.(f.i) by A8,FINSEQ_1:def 7
.= |.f.i1.| by EUCLID:def 2
.= (abs f).i1 by A9,TOPREAL6:12
.= (abs f ^ abs g).i by A9,FINSEQ_1:def 7;
end;
suppose
not i in dom f;
then
A10: len f < i by A5,FINSEQ_3:25;
then reconsider j = i1 - len f as Element of NAT by INT_1:5;
A11: i <= len(f^g) by A6,Th9;
then
A12: j in dom abs g by A1,A10,Th4;
A13: i <= len(abs f ^ abs g) by A3,A1,A2,A6,FINSEQ_1:22;
thus (abs (f^g)).i = absreal.((f^g).i) by A7,FUNCT_1:13
.= absreal.(g.j) by A10,A11,FINSEQ_1:24
.= |.g.j.| by EUCLID:def 2
.= (abs g).j by A12,TOPREAL6:12
.= (abs f ^ abs g).i by A3,A10,A13,FINSEQ_1:24;
end;
end;
len (abs (f^g)) = len (abs f ^ abs g) by A3,A1,A2,FINSEQ_1:22;
hence thesis by A4,FINSEQ_1:14;
end;
theorem
len f = len h & len g = len k implies sqr (f^g + h^k) = sqr (f+h) ^
sqr (g +k)
proof
assume that
A1: len f = len h and
A2: len g = len k;
A3: len (f^g) = len f + len g by FINSEQ_1:22;
A4: len (h^k) = len h + len k by FINSEQ_1:22;
A5: len sqr (f^g + h^k) = len (f^g + h^k) by Th8
.= len (f^g) by A1,A2,A3,A4,Th6
.= len (f+h) + len g by A1,A3,Th6
.= len (f+h) + len (g+k) by A2,Th6
.= len sqr (f+h) + len (g+k) by Th8
.= len sqr (f+h) + len sqr (g+k) by Th8
.= len (sqr (f+h) ^ sqr (g+k)) by FINSEQ_1:22;
for i be Nat st 1 <= i & i <= len sqr (f^g + h^k) holds (sqr (f^g + h^k)
).i = (sqr (f+h) ^ sqr (g+k)).i
proof
let i be Nat;
assume that
A6: 1 <= i and
A7: i <= len sqr (f^g + h^k);
i in dom sqr (f^g + h^k) by A6,A7,FINSEQ_3:25;
then
A8: i in dom (f^g + h^k) by Th8;
per cases;
suppose
A9: i in dom f;
then
A10: i in dom (f+h) by A1,Th6;
then
A11: i in dom sqr (f+h) by Th8;
A12: i in dom h by A1,A9,FINSEQ_3:29;
thus (sqr (f^g + h^k)).i = ((f^g + h^k).i)^2 by VALUED_1:11
.= ((f^g).i + (h^k).i)^2 by A8,VALUED_1:def 1
.= (f.i + (h^k).i)^2 by A9,FINSEQ_1:def 7
.= (f.i + h.i)^2 by A12,FINSEQ_1:def 7
.= ((f+h).i)^2 by A10,VALUED_1:def 1
.= (sqr (f+h)).i by VALUED_1:11
.= (sqr (f+h) ^ sqr (g+k)).i by A11,FINSEQ_1:def 7;
end;
suppose
not i in dom f;
then
A13: len f < i by A6,FINSEQ_3:25;
then reconsider j = i - len f as Element of NAT by INT_1:5;
A14: len (f+h) < i by A1,A13,Th6;
then
A15: len sqr (f+h) < i by Th8;
i <= len (f^g + h^k) by A7,Th8;
then
A16: i <= len (f^g) by A1,A2,A3,A4,Th6;
then i <= len (f+h) + len g by A1,A3,Th6;
then i <= len (f+h) + len (g+k) by A2,Th6;
then i - len (f+h) in dom (g+k) by A14,Th4;
then
A17: j in dom (g+k) by A1,Th6;
len f = len (f+h) by A1,Th6;
then
A18: j = i - len sqr (f+h) by Th8;
thus (sqr (f^g + h^k)).i = ((f^g + h^k).i)^2 by VALUED_1:11
.= ((f^g).i + (h^k).i)^2 by A8,VALUED_1:def 1
.= (g.j + (h^k).i)^2 by A13,A16,FINSEQ_1:24
.= (g.j + k.j)^2 by A1,A2,A3,A4,A13,A16,FINSEQ_1:24
.= ((g+k).j)^2 by A17,VALUED_1:def 1
.= (sqr (g+k)).j by VALUED_1:11
.= (sqr (f+h) ^ sqr (g+k)).i by A5,A7,A15,A18,FINSEQ_1:24;
end;
end;
hence thesis by A5,FINSEQ_1:14;
end;
theorem
len f = len h & len g = len k implies abs (f^g + h^k) = abs (f+h) ^
abs ( g+k)
proof
assume that
A1: len f = len h and
A2: len g = len k;
A3: len (f^g) = len f + len g by FINSEQ_1:22;
A4: len (h^k) = len h + len k by FINSEQ_1:22;
A5: len abs (f^g + h^k) = len (f^g + h^k) by Th9
.= len (f^g) by A1,A2,A3,A4,Th6
.= len (f+h) + len g by A1,A3,Th6
.= len (f+h) + len (g+k) by A2,Th6
.= len abs (f+h) + len (g+k) by Th9
.= len abs (f+h) + len abs (g+k) by Th9
.= len (abs (f+h) ^ abs (g+k)) by FINSEQ_1:22;
for i be Nat st 1 <= i & i <= len abs (f^g + h^k) holds (abs (f^g + h^k)
).i = (abs (f+h) ^ abs (g+k)).i
proof
let i be Nat;
assume that
A6: 1 <= i and
A7: i <= len abs (f^g + h^k);
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
A8: i in dom abs (f^g + h^k) by A6,A7,FINSEQ_3:25;
then
A9: i in dom (f^g + h^k) by Th9;
per cases;
suppose
A10: i in dom f;
then
A11: i in dom h by A1,FINSEQ_3:29;
A12: i in dom (f+h) by A1,A10,Th6;
then
A13: i in dom abs (f+h) by Th9;
thus (abs (f^g + h^k)).i = |.(f^g + h^k).i1.| by A8,TOPREAL6:12
.= |.(f^g).i + (h^k).i.| by A9,VALUED_1:def 1
.= |.f.i + (h^k).i.| by A10,FINSEQ_1:def 7
.= |.f.i + h.i.| by A11,FINSEQ_1:def 7
.= |.(f+h).i1.| by A12,VALUED_1:def 1
.= (abs (f+h)).i1 by A13,TOPREAL6:12
.= (abs (f+h) ^ abs (g+k)).i by A13,FINSEQ_1:def 7;
end;
suppose
not i in dom f;
then
A14: len f < i by A6,FINSEQ_3:25;
then reconsider j = i - len f as Element of NAT by INT_1:5;
A15: len (f+h) < i by A1,A14,Th6;
then
A16: len abs (f+h) < i by Th9;
i <= len (f^g + h^k) by A7,Th9;
then
A17: i <= len (f^g) by A1,A2,A3,A4,Th6;
then i <= len (f+h) + len g by A1,A3,Th6;
then i <= len (f+h) + len (g+k) by A2,Th6;
then i - len (f+h) in dom (g+k) by A15,Th4;
then
A18: j in dom (g+k) by A1,Th6;
then
A19: j in dom abs (g+k) by Th9;
len f = len (f+h) by A1,Th6;
then
A20: j = i - len abs (f+h) by Th9;
thus (abs (f^g + h^k)).i = |.(f^g + h^k).i1.| by A8,TOPREAL6:12
.= |.(f^g).i + (h^k).i.| by A9,VALUED_1:def 1
.= |.g.j + (h^k).i.| by A14,A17,FINSEQ_1:24
.= |.g.j + k.j.| by A1,A2,A3,A4,A14,A17,FINSEQ_1:24
.= |.(g+k).j.| by A18,VALUED_1:def 1
.= (abs (g+k)).j by A19,TOPREAL6:12
.= (abs (f+h) ^ abs (g+k)).i by A5,A7,A16,A20,FINSEQ_1:24;
end;
end;
hence thesis by A5,FINSEQ_1:14;
end;
theorem
len f = len h & len g = len k implies sqr (f^g - h^k) = sqr (f-h) ^
sqr ( g-k)
proof
assume that
A1: len f = len h and
A2: len g = len k;
A3: len (f^g) = len f + len g by FINSEQ_1:22;
A4: len (h^k) = len h + len k by FINSEQ_1:22;
A5: len sqr (f^g - h^k) = len (f^g - h^k) by Th8
.= len (f^g) by A1,A2,A3,A4,Th7
.= len (f-h) + len g by A1,A3,Th7
.= len (f-h) + len (g-k) by A2,Th7
.= len sqr (f-h) + len (g-k) by Th8
.= len sqr (f-h) + len sqr (g-k) by Th8
.= len (sqr (f-h) ^ sqr (g-k)) by FINSEQ_1:22;
for i be Nat st 1 <= i & i <= len sqr (f^g - h^k) holds (sqr (f^g - h^k)
).i = (sqr (f-h) ^ sqr (g-k)).i
proof
let i be Nat;
assume that
A6: 1 <= i and
A7: i <= len sqr (f^g - h^k);
i in dom sqr (f^g - h^k) by A6,A7,FINSEQ_3:25;
then
A8: i in dom (f^g - h^k) by Th8;
per cases;
suppose
A9: i in dom f;
then
A10: i in dom (f-h) by A1,Th7;
then
A11: i in dom sqr (f-h) by Th8;
A12: i in dom h by A1,A9,FINSEQ_3:29;
thus (sqr (f^g - h^k)).i = ((f^g - h^k).i)^2 by VALUED_1:11
.= ((f^g).i - (h^k).i)^2 by A8,VALUED_1:13
.= (f.i - (h^k).i)^2 by A9,FINSEQ_1:def 7
.= (f.i - h.i)^2 by A12,FINSEQ_1:def 7
.= ((f-h).i)^2 by A10,VALUED_1:13
.= (sqr (f-h)).i by VALUED_1:11
.= (sqr (f-h) ^ sqr (g-k)).i by A11,FINSEQ_1:def 7;
end;
suppose
not i in dom f;
then
A13: len f < i by A6,FINSEQ_3:25;
then reconsider j = i - len f as Element of NAT by INT_1:5;
A14: len (f-h) < i by A1,A13,Th7;
then
A15: len sqr (f-h) < i by Th8;
i <= len (f^g - h^k) by A7,Th8;
then
A16: i <= len (f^g) by A1,A2,A3,A4,Th7;
then i <= len (f-h) + len g by A1,A3,Th7;
then i <= len (f-h) + len (g-k) by A2,Th7;
then i - len (f-h) in dom (g-k) by A14,Th4;
then
A17: j in dom (g-k) by A1,Th7;
len f = len (f-h) by A1,Th7;
then
A18: j = i - len sqr (f-h) by Th8;
thus (sqr (f^g - h^k)).i = ((f^g - h^k).i)^2 by VALUED_1:11
.= ((f^g).i - (h^k).i)^2 by A8,VALUED_1:13
.= (g.j - (h^k).i)^2 by A13,A16,FINSEQ_1:24
.= (g.j - k.j)^2 by A1,A2,A3,A4,A13,A16,FINSEQ_1:24
.= ((g-k).j)^2 by A17,VALUED_1:13
.= (sqr (g-k)).j by VALUED_1:11
.= (sqr (f-h) ^ sqr (g-k)).i by A5,A7,A15,A18,FINSEQ_1:24;
end;
end;
hence thesis by A5,FINSEQ_1:14;
end;
theorem Th15:
len f = len h & len g = len k implies abs (f^g - h^k) = abs (f-h
) ^ abs (g-k)
proof
assume that
A1: len f = len h and
A2: len g = len k;
A3: len (f^g) = len f + len g by FINSEQ_1:22;
A4: len (h^k) = len h + len k by FINSEQ_1:22;
A5: len abs (f^g - h^k) = len (f^g - h^k) by Th9
.= len (f^g) by A1,A2,A3,A4,Th7
.= len (f-h) + len g by A1,A3,Th7
.= len (f-h) + len (g-k) by A2,Th7
.= len abs (f-h) + len (g-k) by Th9
.= len abs (f-h) + len abs (g-k) by Th9
.= len (abs (f-h) ^ abs (g-k)) by FINSEQ_1:22;
for i be Nat st 1 <= i & i <= len abs (f^g - h^k) holds (abs (f^g - h^k)
).i = (abs (f-h) ^ abs (g-k)).i
proof
let i be Nat;
assume that
A6: 1 <= i and
A7: i <= len abs (f^g - h^k);
A8: i in dom abs (f^g - h^k) by A6,A7,FINSEQ_3:25;
then
A9: i in dom (f^g - h^k) by Th9;
per cases;
suppose
A10: i in dom f;
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
A11: i in dom h by A1,A10,FINSEQ_3:29;
A12: i in dom (f-h) by A1,A10,Th7;
then
A13: i in dom abs (f-h) by Th9;
thus (abs (f^g - h^k)).i = |.(f^g - h^k).i1.| by A8,TOPREAL6:12
.= |.(f^g).i - (h^k).i.| by A9,VALUED_1:13
.= |.f.i - (h^k).i.| by A10,FINSEQ_1:def 7
.= |.f.i - h.i.| by A11,FINSEQ_1:def 7
.= |.(f-h).i1.| by A12,VALUED_1:13
.= (abs (f-h)).i1 by A13,TOPREAL6:12
.= (abs (f-h) ^ abs (g-k)).i by A13,FINSEQ_1:def 7;
end;
suppose
A14: not i in dom f;
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
A15: len f < i by A6,A14,FINSEQ_3:25;
then reconsider j = i - len f as Element of NAT by INT_1:5;
A16: len (f-h) < i by A1,A15,Th7;
then
A17: len abs (f-h) < i by Th9;
i <= len (f^g - h^k) by A7,Th9;
then
A18: i <= len (f^g) by A1,A2,A3,A4,Th7;
then i <= len (f-h) + len g by A1,A3,Th7;
then i <= len (f-h) + len (g-k) by A2,Th7;
then i - len (f-h) in dom (g-k) by A16,Th4;
then
A19: j in dom (g-k) by A1,Th7;
then
A20: j in dom abs (g-k) by Th9;
len f = len (f-h) by A1,Th7;
then
A21: j = i - len abs (f-h) by Th9;
thus (abs (f^g - h^k)).i = |.(f^g - h^k).i1.| by A8,TOPREAL6:12
.= |.(f^g).i - (h^k).i.| by A9,VALUED_1:13
.= |.g.j - (h^k).i.| by A15,A18,FINSEQ_1:24
.= |.g.j - k.j.| by A1,A2,A3,A4,A15,A18,FINSEQ_1:24
.= |.(g-k).j.| by A19,VALUED_1:13
.= (abs (g-k)).j by A20,TOPREAL6:12
.= (abs (f-h) ^ abs (g-k)).i by A5,A7,A17,A21,FINSEQ_1:24;
end;
end;
hence thesis by A5,FINSEQ_1:14;
end;
theorem Th16:
len f = n implies f in the carrier of Euclid n by TOPREAL3:45;
theorem
len f = n implies f in the carrier of TOP-REAL n by TOPREAL3:46;
definition
let M, N be non empty MetrStruct;
func max-Prod2(M,N) -> strict MetrStruct means
:Def1:
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));
existence
proof
defpred P[set,set,set] means ex x1, y1 being Point of M, x2, y2 being
Point of N st $1 = [x1,x2] & $2 = [y1,y2] & $3 = max ((the distance of M).(x1,
y1),(the distance of N).(x2,y2));
set C = [:the carrier of M,the carrier of N:];
A1: for x, y being Element of C ex u being Element of REAL st P[x,y,u]
proof
let x, y be Element of C;
set x1 = x`1, x2 = x`2, y1 = y`1, y2 = y`2;
set m = max ((the distance of M).(x1,y1),(the distance of N).(x2,y2));
reconsider m as Element of REAL by XREAL_0:def 1;
take m;
take x1, y1, x2, y2;
thus thesis by MCART_1:21;
end;
consider f being Function of [:C,C:], REAL such that
A2: for x, y being Element of C holds P[x,y,f.(x,y)] from BINOP_1:sch
3(A1 );
take E = MetrStruct(#C,f#);
thus the carrier of E = [:the carrier of M,the carrier of N:];
let x, y be Point of E;
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A3: x = [x1,x2] & y = [y1,y2] & f.(x,y) = max ((the distance of M).(x1
,y1),( the distance of N).(x2, y2)) by A2;
take x1, y1, x2, y2;
thus thesis by A3;
end;
uniqueness
proof
let A, B be strict MetrStruct such that
A4: the carrier of A = [:the carrier of M,the carrier of N:] and
A5: for x, y being Point of A ex x1, y1 being Point of M, x2, y2 being
Point of N st x = [x1,x2] & y = [y1,y2] & (the distance of A).(x,y) = max ((the
distance of M).(x1,y1),(the distance of N).(x2,y2)) and
A6: the carrier of B = [:the carrier of M,the carrier of N:] and
A7: for x, y being Point of B ex x1, y1 being Point of M, x2, y2 being
Point of N st x = [x1,x2] & y = [y1,y2] & (the distance of B).(x,y) = max ((the
distance of M).(x1,y1),(the distance of N).(x2,y2));
set f = the distance of A, g = the distance of B;
for a, b being set st a in the carrier of A & b in the carrier of A
holds f.(a,b) = g.(a,b)
proof
let a, b be set;
assume
A8: a in the carrier of A & b in the carrier of A;
then consider x1, y1 being Point of M, x2, y2 being Point of N such that
A9: a = [x1,x2] and
A10: b = [y1,y2] and
A11: f.(a,b) = max ((the distance of M).(x1,y1),(the distance of N).
(x2,y2)) by A5;
consider m1, n1 being Point of M, m2, n2 being Point of N such that
A12: a = [m1,m2] and
A13: b = [n1,n2] and
A14: g.(a,b) = max ((the distance of M).(m1,n1),(the distance of N).
(m2,n2)) by A4,A6,A7,A8;
A15: y1 = n1 by A10,A13,XTUPLE_0:1;
x1 = m1 & x2 = m2 by A9,A12,XTUPLE_0:1;
hence thesis by A10,A11,A13,A14,A15,XTUPLE_0:1;
end;
hence thesis by A4,A6,BINOP_1:1;
end;
end;
registration
let M, N be non empty MetrStruct;
cluster max-Prod2(M,N) -> non empty;
coherence
proof
the carrier of max-Prod2(M,N) = [:the carrier of M,the carrier of N:]
by Def1;
hence the carrier of max-Prod2(M,N) is non empty;
end;
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); :: redefines [ (TARSKI, definition)
coherence
proof
[x,y] is Element of max-Prod2(M,N) by Def1;
hence thesis;
end;
end;
definition
let M, N be non empty MetrStruct, x be Point of max-Prod2(M,N);
redefine func x`1 -> Element of M; :: redefines `1 (XTUPLE_0, definition)
coherence
proof
the carrier of max-Prod2(M,N) = [:the carrier of M, the carrier of N
:] by Def1;
hence thesis by MCART_1:10;
end;
redefine func x`2 -> Element of N; :: redefines `2 (XTUPLE_0, definition)
coherence
proof
the carrier of max-Prod2(M,N) = [:the carrier of M, the carrier of N
:] by Def1;
hence thesis by MCART_1:10;
end;
end;
theorem Th18:
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
))
proof
let M, N be non empty MetrStruct, m1, m2 be Point of M, n1, n2 be Point of N;
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A1: [m1,n1] = [x1,x2] and
A2: [m2,n2] = [y1,y2] and
A3: (the distance of max-Prod2(M,N)).([m1,n1],[m2,n2]) = max ((the
distance of M).(x1,y1),(the distance of N).(x2,y2)) by Def1;
A4: m2 = y1 by A2,XTUPLE_0:1;
m1 = x1 & n1 = x2 by A1,XTUPLE_0:1;
hence thesis by A2,A3,A4,XTUPLE_0:1;
end;
theorem
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))
proof
let M, N be non empty MetrStruct, m, n be Point of max-Prod2(M,N);
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A1: m = [x1,x2] and
A2: n = [y1,y2] and
A3: (the distance of max-Prod2(M,N)).(m,n) = max ((the distance of M).(
x1,y1),(the distance of N).(x2,y2)) by Def1;
A4: m`2 = x2 by A1;
m`1 = x1 & n`1 = y1 by A1,A2;
hence thesis by A2,A3,A4;
end;
theorem Th20:
for M, N being Reflexive non empty MetrStruct holds max-Prod2(
M,N) is Reflexive
proof
let M, N be Reflexive non empty MetrStruct;
let a be Element of max-Prod2(M,N);
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A1: a = [x1,x2] & a = [y1,y2] and
A2: (the distance of max-Prod2(M,N)).(a,a) = max ((the distance of M).(
x1,y1),(the distance of N).(x2,y2)) by Def1;
the distance of M is Reflexive by METRIC_1:def 6;
then
A3: (the distance of M).(x1,x1) = 0;
the distance of N is Reflexive by METRIC_1:def 6;
then
A4: (the distance of N).(x2,x2) = 0;
x1 = y1 & x2 = y2 by A1,XTUPLE_0:1;
hence thesis by A2,A3,A4;
end;
registration
let M, N be Reflexive non empty MetrStruct;
cluster max-Prod2(M,N) -> Reflexive;
coherence by Th20;
end;
Lm1: for M, N being non empty MetrSpace holds max-Prod2(M,N) is discerning
proof
let M, N be non empty MetrSpace;
let a, b be Element of max-Prod2(M,N);
assume
A1: (the distance of max-Prod2(M,N)).(a,b) = 0;
A2: the distance of M is discerning by METRIC_1:def 7;
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A3: a = [x1,x2] & b = [y1,y2] and
A4: (the distance of max-Prod2(M,N)).(a,b) = max ((the distance of M).(
x1,y1),(the distance of N).(x2,y2)) by Def1;
0 <= dist(x1,y1) by METRIC_1:5;
then (the distance of M).(x1,y1) = 0 by A1,A4,XXREAL_0:49;
then
A5: the distance of N is discerning & x1 = y1 by A2,METRIC_1:def 7;
0 <= dist(x2,y2) by METRIC_1:5;
then (the distance of N).(x2,y2) = 0 by A1,A4,XXREAL_0:49;
hence thesis by A3,A5;
end;
theorem Th21:
for M, N being symmetric non empty MetrStruct holds max-Prod2(
M,N) is symmetric
proof
let M, N be symmetric non empty MetrStruct;
let a, b be Element of max-Prod2(M,N);
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A1: a = [x1,x2] and
A2: b = [y1,y2] and
A3: (the distance of max-Prod2(M,N)).(a,b) = max ((the distance of M).(
x1,y1),(the distance of N).(x2,y2)) by Def1;
consider m1, n1 being Point of M, m2, n2 being Point of N such that
A4: b = [m1,m2] and
A5: a = [n1,n2] and
A6: (the distance of max-Prod2(M,N)).(b,a) = max ((the distance of M).(
m1,n1),(the distance of N).(m2,n2)) by Def1;
A7: x1 = n1 by A1,A5,XTUPLE_0:1;
the distance of N is symmetric by METRIC_1:def 8;
then
A8: (the distance of N).(x2,y2) = (the distance of N).(y2,x2);
the distance of M is symmetric by METRIC_1:def 8;
then
A9: (the distance of M).(x1,y1) = (the distance of M).(y1,x1);
y1 = m1 & y2 = m2 by A2,A4,XTUPLE_0:1;
hence thesis by A1,A3,A5,A6,A9,A8,A7,XTUPLE_0:1;
end;
registration
let M, N be symmetric non empty MetrStruct;
cluster max-Prod2(M,N) -> symmetric;
coherence by Th21;
end;
theorem Th22:
for M, N being triangle non empty MetrStruct holds max-Prod2(M
,N) is triangle
proof
let M, N be triangle non empty MetrStruct;
let a, b, c be Element of max-Prod2(M,N);
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A1: a = [x1,x2] and
A2: b = [y1,y2] and
A3: (the distance of max-Prod2(M,N)).(a,b) = max ((the distance of M).(
x1,y1),(the distance of N).(x2,y2)) by Def1;
consider m1, n1 being Point of M, m2, n2 being Point of N such that
A4: b = [m1,m2] and
A5: c = [n1,n2] and
A6: (the distance of max-Prod2(M,N)).(b,c) = max ((the distance of M).(
m1,n1),(the distance of N).(m2,n2)) by Def1;
A7: y1 = m1 & y2 = m2 by A2,A4,XTUPLE_0:1;
consider p1, q1 being Point of M, p2, q2 being Point of N such that
A8: a = [p1,p2] and
A9: c = [q1,q2] and
A10: (the distance of max-Prod2(M,N)).(a,c) = max ((the distance of M).(
p1,q1),(the distance of N).(p2,q2)) by Def1;
A11: q1 = n1 & q2 = n2 by A5,A9,XTUPLE_0:1;
the distance of N is triangle by METRIC_1:def 9;
then
A12: (the distance of N).(p2,q2) <= (the distance of N).(p2,y2) + (the
distance of N).(y2,q2);
the distance of M is triangle by METRIC_1:def 9;
then
A13: (the distance of M).(p1,q1) <= (the distance of M).(p1,y1) + (the
distance of M).(y1,q1);
x1 = p1 & x2 = p2 by A1,A8,XTUPLE_0:1;
hence thesis by A3,A6,A10,A13,A12,A7,A11,Th2;
end;
registration
let M, N be triangle non empty MetrStruct;
cluster max-Prod2(M,N) -> triangle;
coherence by Th22;
end;
registration
let M, N be non empty MetrSpace;
cluster max-Prod2(M,N) -> discerning;
coherence by Lm1;
end;
theorem Th23:
[:TopSpaceMetr M,TopSpaceMetr N:] = TopSpaceMetr max-Prod2(M,N)
proof
set S = TopSpaceMetr M, T = TopSpaceMetr N;
A1: TopSpaceMetr max-Prod2(M,N) = TopStruct (#the carrier of max-Prod2(M,N),
Family_open_set max-Prod2(M,N) #) by PCOMPS_1:def 5;
A2: TopSpaceMetr M = TopStruct (#the carrier of M, Family_open_set M#) by
PCOMPS_1:def 5;
A3: TopSpaceMetr N = TopStruct (#the carrier of N, Family_open_set N#) by
PCOMPS_1:def 5;
A4: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
BORSUK_1:def 2
.= the carrier of TopSpaceMetr max-Prod2(M,N) by A1,A2,A3,Def1;
A5: the topology of [:S,T:] = { union A where A is Subset-Family of [:S,T:]:
A c= { [:X1,X2:] where X1 is Subset of S, X2 is Subset of T : X1 in the
topology of S & X2 in the topology of T}} by BORSUK_1:def 2;
the topology of [:S,T:] = the topology of TopSpaceMetr max-Prod2(M,N)
proof
thus the topology of [:S,T:] c= the topology of TopSpaceMetr max-Prod2(M,N
)
proof
let X be object;
assume
A6: X in the topology of [:S,T:];
then consider A being Subset-Family of [:S,T:] such that
A7: X = union A and
A8: A c= { [:X1,X2:] where X1 is Subset of S, X2 is Subset of T : X1
in the topology of S & X2 in the topology of T} by A5;
for x being Point of max-Prod2(M,N) st x in union A
ex r being Real st r > 0 & Ball(x,r) c= union A
proof
let x be Point of max-Prod2(M,N);
assume x in union A;
then consider Z being set such that
A9: x in Z and
A10: Z in A by TARSKI:def 4;
Z in { [:X1,X2:] where X1 is Subset of S, X2 is Subset of T : X1
in the topology of S & X2 in the topology of T} by A8,A10;
then consider X1 being Subset of S, X2 being Subset of T such that
A11: Z = [:X1,X2:] and
A12: X1 in the topology of S and
A13: X2 in the topology of T;
consider z1, z2 being object such that
A14: z1 in X1 and
A15: z2 in X2 and
A16: x = [z1,z2] by A9,A11,ZFMISC_1:def 2;
reconsider z2 as Point of N by A3,A15;
consider r2 being Real such that
A17: r2 > 0 and
A18: Ball(z2,r2) c= X2 by A3,A13,A15,PCOMPS_1:def 4;
reconsider z1 as Point of M by A2,A14;
consider r1 being Real such that
A19: r1 > 0 and
A20: Ball(z1,r1) c= X1 by A2,A12,A14,PCOMPS_1:def 4;
take r = min(r1,r2);
thus r > 0 by A19,A17,XXREAL_0:15;
let b be object;
assume
A21: b in Ball(x,r);
then reconsider bb = b as Point of max-Prod2(M,N);
A22: dist(bb,x) < r by A21,METRIC_1:11;
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A23: bb = [x1,x2] and
A24: x = [y1,y2] and
A25: (the distance of max-Prod2(M,N)).(bb,x) = max ((the distance
of M).(x1,y1),(the distance of N).(x2,y2)) by Def1;
z2 = y2 by A16,A24,XTUPLE_0:1;
then
(the distance of N).(x2,z2) <= max ((the distance of M).(x1,y1),(
the distance of N).(x2,y2)) by XXREAL_0:25;
then min(r1,r2) <= r2 & (the distance of N).(x2,z2) < r by A25,A22,
XXREAL_0:2,17;
then dist(x2,z2) < r2 by XXREAL_0:2;
then
A26: x2 in Ball(z2,r2) by METRIC_1:11;
z1 = y1 by A16,A24,XTUPLE_0:1;
then
(the distance of M).(x1,z1) <= max ((the distance of M).(x1,y1),(
the distance of N).(x2,y2)) by XXREAL_0:25;
then min(r1,r2) <= r1 & (the distance of M).(x1,z1) < r by A25,A22,
XXREAL_0:2,17;
then dist(x1,z1) < r1 by XXREAL_0:2;
then x1 in Ball(z1,r1) by METRIC_1:11;
then b in [:X1,X2:] by A20,A18,A23,A26,ZFMISC_1:87;
hence thesis by A10,A11,TARSKI:def 4;
end;
hence thesis by A1,A4,A6,PCOMPS_1:def 4,A7;
end;
let X be object;
assume
A27: X in the topology of TopSpaceMetr max-Prod2(M,N);
then reconsider Y = X as Subset of [:S,T:] by A4;
A28: Base-Appr Y = { [:X1,Y1:] where X1 is Subset of S, Y1 is Subset of T
: [:X1,Y1:] c= Y & X1 is open & Y1 is open} by BORSUK_1:def 3;
A29: union Base-Appr Y = Y
proof
thus union Base-Appr Y c= Y by BORSUK_1:12;
let u be object;
assume
A30: u in Y;
then reconsider uu = u as Point of max-Prod2(M,N) by A1,A4;
consider r being Real such that
A31: r > 0 and
A32: Ball(uu,r) c= Y by A1,A27,A30,PCOMPS_1:def 4;
uu in the carrier of max-Prod2(M,N);
then uu in [:the carrier of M,the carrier of N:] by Def1;
then consider u1, u2 being object such that
A33: u1 in the carrier of M and
A34: u2 in the carrier of N and
A35: u = [u1,u2] by ZFMISC_1:def 2;
reconsider u2 as Point of N by A34;
reconsider u1 as Point of M by A33;
reconsider B2 = Ball(u2,r) as Subset of T by A3;
reconsider B1 = Ball(u1,r) as Subset of S by A2;
u1 in Ball(u1,r) & u2 in Ball(u2,r) by A31,TBSP_1:11;
then
A36: u in [:B1,B2:] by A35,ZFMISC_1:87;
A37: [:B1,B2:] c= Y
proof
let x be object;
assume x in [:B1,B2:];
then consider x1, x2 being object such that
A38: x1 in B1 and
A39: x2 in B2 and
A40: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x2 as Point of N by A39;
reconsider x1 as Point of M by A38;
consider p1, p2 being Point of M, q1, q2 being Point of N such that
A41: uu = [p1,q1] & [x1,x2] = [p2,q2] and
A42: (the distance of max-Prod2(M,N)).(uu,[x1,x2]) = max ((the
distance of M).(p1,p2),(the distance of N).(q1,q2)) by Def1;
u2 = q1 & x2 = q2 by A35,A41,XTUPLE_0:1;
then
A43: dist(q1,q2) < r by A39,METRIC_1:11;
u1 = p1 & x1 = p2 by A35,A41,XTUPLE_0:1;
then dist(p1,p2) < r by A38,METRIC_1:11;
then dist(uu,[x1,x2]) < r by A42,A43,XXREAL_0:16;
then x in Ball(uu,r) by A40,METRIC_1:11;
hence thesis by A32;
end;
B1 is open & B2 is open by TOPMETR:14;
then [:B1,B2:] in Base-Appr Y by A28,A37;
hence thesis by A36,TARSKI:def 4;
end;
Base-Appr Y c= { [:X1,Y1:] where X1 is Subset of S, Y1 is Subset of T
: X1 in the topology of S & Y1 in the topology of T}
proof
let A be object;
assume A in Base-Appr Y;
then consider X1 being Subset of S, Y1 being Subset of T such that
A44: A = [:X1,Y1:] and
[:X1,Y1:] c= Y and
A45: X1 is open & Y1 is open by A28;
X1 in the topology of S & Y1 in the topology of T by A45;
hence thesis by A44;
end;
hence thesis by A5,A29;
end;
hence thesis by A4;
end;
theorem
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
proof
assume that
A1: the carrier of M = the carrier of N and
A2: 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) and
A3: 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);
A4: Family_open_set M = Family_open_set N
proof
thus Family_open_set M c= Family_open_set N
proof
let X be object;
reconsider XX=X as set by TARSKI:1;
assume
A5: X in Family_open_set M;
for n being Point of N st n in XX
ex r being Real st r > 0 & Ball(n,r) c= XX
proof
let n be Point of N such that
A6: n in XX;
reconsider m = n as Point of M by A1;
consider r being Real such that
A7: r > 0 and
A8: Ball(m,r) c= XX by A5,A6,PCOMPS_1:def 4;
consider r1 being Real such that
A9: r1 > 0 & Ball(n,r1) c= Ball(m,r) by A2,A7;
take r1;
thus thesis by A8,A9;
end;
hence thesis by A1,A5,PCOMPS_1:def 4;
end;
let X be object;
reconsider XX=X as set by TARSKI:1;
assume
A10: X in Family_open_set N;
for m being Point of M st m in XX
ex r being Real st r > 0 & Ball(m,r) c= XX
proof
let m be Point of M such that
A11: m in XX;
reconsider n = m as Point of N by A1;
consider r being Real such that
A12: r > 0 and
A13: Ball(n,r) c= XX by A10,A11,PCOMPS_1:def 4;
consider r1 being Real such that
A14: r1 > 0 & Ball(m,r1) c= Ball(n,r) by A3,A12;
take r1;
thus thesis by A13,A14;
end;
hence thesis by A1,A10,PCOMPS_1:def 4;
end;
TopSpaceMetr M = TopStruct (#the carrier of M, Family_open_set M#) by
PCOMPS_1:def 5;
hence thesis by A1,A4,PCOMPS_1:def 5;
end;
Lm2: 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
proof
set ci = the carrier of Euclid i, cj = the carrier of Euclid j, cij = the
carrier of Euclid (i+j);
defpred P[Element of ci,Element of cj,set] means ex fi, fj being
FinSequence of REAL st fi = $1 & fj = $2 & $3 = fi ^ fj;
A1: the carrier of TopSpaceMetr max-Prod2(Euclid i,Euclid j) = the carrier
of max-Prod2(Euclid i,Euclid j) by TOPMETR:12;
A2: for x being Element of ci, y being Element of cj ex u being Element of
cij st P[x,y,u]
proof
let x be Element of ci, y be Element of cj;
x is Element of REAL i & y is Element of REAL j;
then reconsider fi = x, fj = y as FinSequence of REAL;
fi ^ fj is Tuple of i+j, REAL
by FINSEQ_2:107;
then reconsider u = fi ^ fj as Element of cij by FINSEQ_2:131;
take u;
thus thesis;
end;
consider f being Function of [:ci,cj:], cij such that
A3: for x being Element of ci, y being Element of cj holds P[x,y,f.(x,
y)] from BINOP_1:sch 3(A2);
A4: [:ci,cj:] = the carrier of max-Prod2(Euclid i,Euclid j) by Def1;
the carrier of TopSpaceMetr Euclid (i+j) = cij by TOPMETR:12;
then reconsider
f as Function of TopSpaceMetr max-Prod2(Euclid i,Euclid j),
TopSpaceMetr Euclid (i+j) by A4,A1;
A5: [:TopSpaceMetr Euclid i,TopSpaceMetr Euclid j:] =
TopSpaceMetr max-Prod2(Euclid i,Euclid j) by Th23;
then reconsider f as Function of [:TopSpaceMetr Euclid i,
TopSpaceMetr Euclid j:],TopSpaceMetr Euclid (i+j);
take f;
thus dom f = [#] [:TopSpaceMetr Euclid i,TopSpaceMetr Euclid j:]
by FUNCT_2:def 1;
thus
A6: rng f = [#]TopSpaceMetr Euclid (i+j)
proof
thus rng f c= [#]TopSpaceMetr Euclid (i+j);
let y be object;
assume
y in [#]TopSpaceMetr Euclid (i+j);
then reconsider k = y as Element of REAL (i+j) by TOPMETR:12;
len k = i + j by CARD_1:def 7;
then consider g, h being FinSequence of REAL such that
A7: len g = i & len h = j and
A8: k = g^h by FINSEQ_2:23;
A9: g in ci & h in cj by A7,Th16;
then [g,h] in [:ci,cj:] by ZFMISC_1:87;
then
A10: [g,h] in dom f by FUNCT_2:def 1;
ex fi, fj being FinSequence of REAL st fi = g & fj = h & f.(g,h) =
fi ^ fj by A3,A9;
hence thesis by A8,A10,FUNCT_1:def 3;
end;
thus
A11: f is one-to-one
proof
let x1, x2 be object;
assume
x1 in dom f;
then consider x1a, x1b being object such that
A12: x1a in ci and
A13: x1b in cj and
A14: x1 = [x1a,x1b] by A4,A1,A5,ZFMISC_1:def 2;
assume
x2 in dom f;
then consider x2a, x2b being object such that
A15: x2a in ci and
A16: x2b in cj and
A17: x2 = [x2a,x2b] by A4,A1,A5,ZFMISC_1:def 2;
assume
A18: f.x1 = f.x2;
consider fi1, fj1 being FinSequence of REAL such that
A19: fi1 = x1a and
A20: fj1 = x1b and
A21: f.(x1a,x1b) = fi1 ^ fj1 by A3,A12,A13;
consider fi2, fj2 being FinSequence of REAL such that
A22: fi2 = x2a and
A23: fj2 = x2b and
A24: f.(x2a,x2b) = fi2 ^ fj2 by A3,A15,A16;
len fj1 = j by A13,A20,CARD_1:def 7;
then
A25: len fj1 = len fj2 by A16,A23,CARD_1:def 7;
A26: len fi1 = i by A12,A19,CARD_1:def 7;
then len fi1 = len fi2 by A15,A22,CARD_1:def 7;
then fi1 = fi2 by A14,A17,A21,A24,A25,A18,Th5;
hence thesis by A14,A17,A19,A20,A21,A22,A23,A24,A26,A25,A18,Th5;
end;
A27: for P being Subset of TopSpaceMetr max-Prod2(Euclid i,Euclid j) st P
is open holds f""P is open
proof
let P be Subset of TopSpaceMetr max-Prod2(Euclid i,Euclid j);
assume
P is open;
then P in the topology of TopSpaceMetr max-Prod2(Euclid i,Euclid j);
then
A28: P in Family_open_set max-Prod2(Euclid i,Euclid j) by TOPMETR:12;
A29: for x being Point of Euclid (i+j) st x in f.:P
ex r being Real st r > 0 & Ball(x,r) c= f.:P
proof
let x be Point of Euclid (i+j);
assume
x in f.:P;
then consider a being object such that
A30: a in the carrier of TopSpaceMetr max-Prod2(Euclid i,Euclid j) and
A31: a in P and
A32: x = f.a by FUNCT_2:64;
reconsider a as Point of max-Prod2(Euclid i,Euclid j) by A30,TOPMETR:12
;
consider r being Real such that
A33: r > 0 and
A34: Ball(a,r) c= P by A28,A31,PCOMPS_1:def 4;
take r;
thus r > 0 by A33;
let b be object;
assume
A35: b in Ball(x,r);
then reconsider bb = b as Point of Euclid (i+j);
reconsider bb2 = bb, xx2 = x as Element of REAL (i+j);
dist(bb,x) < r by A35,METRIC_1:11;
then |.bb2-xx2.| < r by EUCLID:def 6;
then
A36: sqrt Sum sqr abs (bb2-xx2) < r by EUCLID:25;
reconsider k = bb as Element of REAL (i+j);
len k = i + j by CARD_1:def 7;
then consider g, h being FinSequence of REAL such that
A37: len g = i and
A38: len h = j and
A39: k = g^h by FINSEQ_2:23;
reconsider hh = h as Point of Euclid j by A38,Th16;
reconsider gg = g as Point of Euclid i by A37,Th16;
consider g, h being FinSequence of REAL such that
A40: g = gg and
A41: h = hh and
A42: f.(gg,hh) = g ^ h by A3;
reconsider gg2 = gg, a12 = a`1 as Element of REAL i;
A43: max (dist(gg,a`1),dist(hh,a`2)) = dist(gg,a`1) or max (dist(gg,a
`1),dist(hh,a`2)) = dist(hh,a`2) by XXREAL_0:16;
consider p, q being object such that
A44: p in ci and
A45: q in cj and
A46: a = [p,q] by A4,ZFMISC_1:def 2;
reconsider q as Element of cj by A45;
reconsider p as Element of ci by A44;
consider fi, fj being FinSequence of REAL such that
A47: fi = p and
A48: fj = q and
A49: f.(p,q) = fi ^ fj by A3;
A50: len fi = i & len fj = j by A47,A48,CARD_1:def 7;
len g = i & len h = j by A40,A41,CARD_1:def 7;
then sqrt Sum sqr (abs(g-fi) ^ abs(h-fj)) < r by A32,A39,A46,A49,A40
,A41,A50,A36,Th15;
then sqrt Sum (sqr abs (g-fi) ^ sqr abs (h-fj)) < r by Th10;
then
A51: sqrt (Sum sqr abs (g-fi) + Sum sqr abs (h-fj)) < r by RVSUM_1:75;
reconsider hh2 = hh, a22 = a`2 as Element of REAL j;
A52: a22 = q by A46;
0 <= Sum sqr abs (g-fi) by RVSUM_1:86;
then 0 <= Sum sqr abs (hh2-a22) & Sum sqr abs (hh2-a22) + 0 <= Sum
sqr abs (g-fi) + Sum sqr abs (h-fj) by A48,A41,A52,RVSUM_1:86,XREAL_1:7;
then sqrt Sum sqr abs (hh2-a22) <= sqrt (Sum sqr abs (g-fi) + Sum sqr
abs ( h-fj)) by SQUARE_1:26;
then sqrt Sum sqr abs (hh2-a22) < r by A51,XXREAL_0:2;
then |.hh2-a22.| < r by EUCLID:25;
then
A53: (Pitag_dist j).(hh2,a22) < r by EUCLID:def 6;
A54: a12 = p by A46;
0 <= Sum sqr abs (h-fj) by RVSUM_1:86;
then 0 <= Sum sqr abs (gg2-a12) & Sum sqr abs (gg2-a12) + 0 <= Sum
sqr abs (g-fi) + Sum sqr abs (h-fj) by A47,A40,A54,RVSUM_1:86,XREAL_1:7;
then sqrt Sum sqr abs (gg2-a12) <= sqrt (Sum sqr abs (g-fi) + Sum sqr
abs ( h-fj)) by SQUARE_1:26;
then sqrt Sum sqr abs (gg2-a12) < r by A51,XXREAL_0:2;
then |.gg2-a12.| < r by EUCLID:25;
then
A55: (Pitag_dist i).(gg2,a12) < r by EUCLID:def 6;
dist([gg,hh],[a`1,a`2]) = max (dist(gg,a`1),dist(hh,a`2)) by Th18;
then dist([gg,hh],a) < r by A4,A55,A53,A43,MCART_1:21;
then [g,h] in Ball(a,r) by A40,A41,METRIC_1:11;
then [g,h] in P by A34;
hence thesis by A39,A40,A41,A42,FUNCT_2:35;
end;
f.:P is Subset of Euclid (i+j) by TOPMETR:12;
then f.:P in Family_open_set Euclid (i+j) by A29,PCOMPS_1:def 4;
then f.:P in the topology of TopSpaceMetr Euclid (i+j) by TOPMETR:12;
hence f""P in the topology of TopSpaceMetr Euclid (i+j) by A6,A11,A5,
TOPS_2:54;
end;
A56: for P being Subset of TopSpaceMetr Euclid (i+j) st P is open holds f"
P is open
proof
let P be Subset of TopSpaceMetr Euclid (i+j);
assume
P is open;
then P in the topology of TopSpaceMetr Euclid (i+j);
then
A57: P in Family_open_set Euclid (i+j) by TOPMETR:12;
A58: for x being Point of max-Prod2(Euclid i,Euclid j) st x in f"P ex r
being Real st r > 0 & Ball(x,r) c= f"P
proof
let x be Point of max-Prod2(Euclid i,Euclid j);
assume
A59: x in f"P;
then f.x in the carrier of TopSpaceMetr Euclid (i+j) by FUNCT_2:5;
then reconsider fx = f.x as Point of Euclid (i+j) by TOPMETR:12;
f.x in P by A59,FUNCT_2:38;
then consider r being Real such that
A60: r > 0 and
A61: Ball(fx,r) c= P by A57,PCOMPS_1:def 4;
take r1 = r/2;
thus r1 > 0 by A60,XREAL_1:139;
let b be object;
assume
A62: b in Ball(x,r1);
then reconsider bb = b as Point of max-Prod2(Euclid i,Euclid j);
A63: dist(bb,x) < r1 by A62,METRIC_1:11;
bb in the carrier of max-Prod2(Euclid i,Euclid j);
then
A64: bb in the carrier of TopSpaceMetr max-Prod2(Euclid i, Euclid j)
by TOPMETR:12;
then f.bb in the carrier of TopSpaceMetr Euclid (i+j) by FUNCT_2:5;
then reconsider fb = f.b as Point of Euclid (i+j) by TOPMETR:12;
reconsider fbb = fb, fxx = fx as Element of REAL (i+j);
consider b1, x1 being Point of Euclid i, b2, x2 being Point of Euclid
j such that
A65: bb = [b1,b2] & x = [x1,x2] and
(the distance of max-Prod2(Euclid i,Euclid j)).(bb,x) = max ((the
distance of Euclid i).(b1,x1),( the distance of Euclid j).(b2,x2)) by Def1;
A66: dist([b1,b2],[x1,x2]) = max (dist(b1,x1),dist(b2,x2)) by Th18;
dist(b2,x2) <= max (dist(b1,x1),dist(b2,x2)) by XXREAL_0:25;
then
A67: dist(b2,x2) < r1 by A65,A66,A63,XXREAL_0:2;
reconsider x2i = x2, b2i = b2 as Element of REAL j;
reconsider b1i = b1, x1i = x1 as Element of REAL i;
consider b1f, b2f being FinSequence of REAL such that
A68: b1f = b1 & b2f = b2 and
A69: f.(b1,b2) = b1f ^ b2f by A3;
A70: len b1f = i & len b2f = j by A68,CARD_1:def 7;
dist(b1,x1) <= max (dist(b1,x1),dist(b2,x2)) by XXREAL_0:25;
then dist(b1,x1) < r1 by A65,A66,A63,XXREAL_0:2;
then
A71: (Pitag_dist i).(b1i,x1i) + (Pitag_dist j).(b2i,x2i) < r1 + r1 by A67,
XREAL_1:8;
0 <= Sum sqr (b1i - x1i) & 0 <= Sum sqr (b2i - x2i) by RVSUM_1:86;
then
sqrt (Sum sqr (b1i - x1i) + Sum sqr (b2i - x2i)) <= |.b1i - x1i.|
+ sqrt Sum sqr (b2i - x2i) by SQUARE_1:59;
then
sqrt (Sum sqr (b1i - x1i) + Sum sqr (b2i - x2i)) <= (Pitag_dist i
).(b1i,x1i) + |.b2i - x2i.| by EUCLID:def 6;
then
A72: sqrt (Sum sqr (b1i - x1i) + Sum sqr (b2i - x2i)) <= (Pitag_dist i
).(b1i,x1i) + (Pitag_dist j).(b2i,x2i) by EUCLID:def 6;
consider x1f, x2f being FinSequence of REAL such that
A73: x1f = x1 & x2f = x2 and
A74: f.(x1,x2) = x1f ^ x2f by A3;
A75: len x1f = i & len x2f = j by A73,CARD_1:def 7;
(Pitag_dist (i+j)).(fbb,fxx) = |.fbb - fxx.| by EUCLID:def 6
.= sqrt Sum sqr abs (fbb - fxx) by EUCLID:25
.= sqrt Sum sqr (abs (b1i - x1i) ^ abs (b2i - x2i)) by A65,A68,A69
,A73,A74,A70,A75,Th15
.= sqrt Sum (sqr abs (b1i - x1i) ^ sqr abs (b2i - x2i)) by Th10
.= sqrt (Sum sqr abs (b1i - x1i) + Sum sqr abs (b2i - x2i)) by
RVSUM_1:75
.= sqrt (Sum sqr abs (b1i - x1i) + Sum sqr (b2i - x2i)) by EUCLID:25
.= sqrt (Sum sqr (b1i - x1i) + Sum sqr (b2i - x2i)) by EUCLID:25;
then dist(fb,fx) < r by A72,A71,XXREAL_0:2;
then f.b in Ball(fx,r) by METRIC_1:11;
hence thesis by A61,A64,FUNCT_2:38;
end;
f"P is Subset of max-Prod2(Euclid i,Euclid j) by A5,TOPMETR:12;
then f"P in Family_open_set max-Prod2(Euclid i,Euclid j) by A58,
PCOMPS_1:def 4;
hence
f"P in the topology of [:TopSpaceMetr Euclid i,TopSpaceMetr Euclid j:]
by A5,TOPMETR:12;
end;
[#]TopSpaceMetr Euclid (i+j) <> {};
hence f is continuous by A56,TOPS_2:43;
[#]TopSpaceMetr max-Prod2(Euclid i, Euclid j) <> {};
hence f" is continuous by A27,A5,TOPS_2:43;
let fi,fj be FinSequence;
assume A76:[fi,fj] in dom f;
then reconsider Fi=fi as Element of ci by A1,A5,A4,ZFMISC_1:87;
reconsider Fj=fj as Element of cj by A76,A1,A5,A4,ZFMISC_1:87;
P[Fi,Fj,f.(Fi,Fj)] by A3;
hence f.(fi,fj) = fi^fj;
end;
theorem
[:TopSpaceMetr Euclid i,TopSpaceMetr Euclid j:],
TopSpaceMetr Euclid (i+j) are_homeomorphic
proof
consider f be Function of [:TopSpaceMetr Euclid i,TopSpaceMetr Euclid j:],
TopSpaceMetr Euclid (i+j) such that
A1:f is being_homeomorphism and
for fi,fj be FinSequence st [fi,fj] in dom f holds f.(fi,fj) = fi^fj by Lm2;
take f;
thus thesis by A1;
end;
theorem
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 by Lm2;