let i, j be Element of NAT ; [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], TopSpaceMetr (Euclid (i + j)) are_homeomorphic
TopSpaceMetr (max-Prod2 (Euclid i),(Euclid j)), TopSpaceMetr (Euclid (i + j)) are_homeomorphic
proof
set ci = the
carrier of
(Euclid i);
set cj = the
carrier of
(Euclid j);
set cij = the
carrier of
(Euclid (i + j));
defpred S1[
Element of the
carrier of
(Euclid i),
Element of the
carrier of
(Euclid j),
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:16;
A2:
for
x being
Element of the
carrier of
(Euclid i) for
y being
Element of the
carrier of
(Euclid j) ex
u being
Element of the
carrier of
(Euclid (i + j)) st
S1[
x,
y,
u]
proof
let x be
Element of the
carrier of
(Euclid i);
for y being Element of the carrier of (Euclid j) ex u being Element of the carrier of (Euclid (i + j)) st S1[x,y,u]let y be
Element of the
carrier of
(Euclid j);
ex u being Element of the carrier of (Euclid (i + j)) st S1[x,y,u]
(
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:127;
then reconsider u =
fi ^ fj as
Element of the
carrier of
(Euclid (i + j)) by FINSEQ_2:151;
take
u
;
S1[x,y,u]
thus
S1[
x,
y,
u]
;
verum
end;
consider f being
Function of
[:the carrier of (Euclid i),the carrier of (Euclid j):],the
carrier of
(Euclid (i + j)) such that A3:
for
x being
Element of the
carrier of
(Euclid i) for
y being
Element of the
carrier of
(Euclid j) holds
S1[
x,
y,
f . x,
y]
from BINOP_1:sch 3(A2);
A4:
[:the carrier of (Euclid i),the carrier of (Euclid j):] = the
carrier of
(max-Prod2 (Euclid i),(Euclid j))
by Def1;
the
carrier of
(TopSpaceMetr (Euclid (i + j))) = the
carrier of
(Euclid (i + j))
by TOPMETR:16;
then reconsider f =
f as
Function of
(TopSpaceMetr (max-Prod2 (Euclid i),(Euclid j))),
(TopSpaceMetr (Euclid (i + j))) by A4, A1;
take
f
;
T_0TOPSP:def 1 f is V71( TopSpaceMetr (max-Prod2 (Euclid i),(Euclid j)), TopSpaceMetr (Euclid (i + j)))
thus
dom f = [#] (TopSpaceMetr (max-Prod2 (Euclid i),(Euclid j)))
by FUNCT_2:def 1;
TOPS_2:def 5 ( rng f = [#] (TopSpaceMetr (Euclid (i + j))) & f is one-to-one & f is continuous & f " is continuous )
thus A5:
rng f = [#] (TopSpaceMetr (Euclid (i + j)))
( f is one-to-one & f is continuous & f " is continuous )proof
thus
rng f c= [#] (TopSpaceMetr (Euclid (i + j)))
;
XBOOLE_0:def 10 [#] (TopSpaceMetr (Euclid (i + j))) c= rng f
let y be
set ;
TARSKI:def 3 ( not y in [#] (TopSpaceMetr (Euclid (i + j))) or y in rng f )
assume
y in [#] (TopSpaceMetr (Euclid (i + j)))
;
y in rng f
then reconsider k =
y as
Element of
REAL (i + j) by TOPMETR:16;
len k = i + j
by FINSEQ_1:def 18;
then consider g,
h being
FinSequence of
REAL such that A6:
(
len g = i &
len h = j )
and A7:
k = g ^ h
by FINSEQ_2:26;
A8:
(
g in the
carrier of
(Euclid i) &
h in the
carrier of
(Euclid j) )
by A6, Th17;
then
[g,h] in [:the carrier of (Euclid i),the carrier of (Euclid j):]
by ZFMISC_1:106;
then A9:
[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, A8;
hence
y in rng f
by A7, A9, FUNCT_1:def 5;
verum
end;
thus A10:
f is
one-to-one
( f is continuous & f " is continuous )proof
let x1,
x2 be
set ;
FUNCT_1:def 8 ( not x1 in K74(f) or not x2 in K74(f) or not f . x1 = f . x2 or x1 = x2 )
assume
x1 in dom f
;
( not x2 in K74(f) or not f . x1 = f . x2 or x1 = x2 )
then consider x1a,
x1b being
set such that A11:
x1a in the
carrier of
(Euclid i)
and A12:
x1b in the
carrier of
(Euclid j)
and A13:
x1 = [x1a,x1b]
by A4, A1, ZFMISC_1:def 2;
assume
x2 in dom f
;
( not f . x1 = f . x2 or x1 = x2 )
then consider x2a,
x2b being
set such that A14:
x2a in the
carrier of
(Euclid i)
and A15:
x2b in the
carrier of
(Euclid j)
and A16:
x2 = [x2a,x2b]
by A4, A1, ZFMISC_1:def 2;
assume A17:
f . x1 = f . x2
;
x1 = x2
consider fi1,
fj1 being
FinSequence of
REAL such that A18:
fi1 = x1a
and A19:
fj1 = x1b
and A20:
f . x1a,
x1b = fi1 ^ fj1
by A3, A11, A12;
consider fi2,
fj2 being
FinSequence of
REAL such that A21:
fi2 = x2a
and A22:
fj2 = x2b
and A23:
f . x2a,
x2b = fi2 ^ fj2
by A3, A14, A15;
len fj1 = j
by A12, A19, FINSEQ_1:def 18;
then A24:
len fj1 = len fj2
by A15, A22, FINSEQ_1:def 18;
A25:
len fi1 = i
by A11, A18, FINSEQ_1:def 18;
then
len fi1 = len fi2
by A14, A21, FINSEQ_1:def 18;
then
fi1 = fi2
by A13, A16, A20, A23, A24, A17, Th6;
hence
x1 = x2
by A13, A16, A18, A19, A20, A21, A22, A23, A25, A24, A17, Th6;
verum
end;
A26:
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)));
( P is open implies (f " ) " P is open )
assume
P is
open
;
(f " ) " P is open
then
P in the
topology of
(TopSpaceMetr (max-Prod2 (Euclid i),(Euclid j)))
by PRE_TOPC:def 5;
then A27:
P in Family_open_set (max-Prod2 (Euclid i),(Euclid j))
by TOPMETR:16;
A28:
for
x being
Point of
(Euclid (i + j)) st
x in f .: P holds
ex
r being
Real st
(
r > 0 &
Ball x,
r c= f .: P )
proof
let x be
Point of
(Euclid (i + j));
( x in f .: P implies ex r being Real st
( r > 0 & Ball x,r c= f .: P ) )
assume
x in f .: P
;
ex r being Real st
( r > 0 & Ball x,r c= f .: P )
then consider a being
set such that A29:
a in the
carrier of
(TopSpaceMetr (max-Prod2 (Euclid i),(Euclid j)))
and A30:
a in P
and A31:
x = f . a
by FUNCT_2:115;
reconsider a =
a as
Point of
(max-Prod2 (Euclid i),(Euclid j)) by A29, TOPMETR:16;
consider r being
Real such that A32:
r > 0
and A33:
Ball a,
r c= P
by A27, A30, PCOMPS_1:def 5;
take
r
;
( r > 0 & Ball x,r c= f .: P )
thus
r > 0
by A32;
Ball x,r c= f .: P
let b be
set ;
TARSKI:def 3 ( not b in Ball x,r or b in f .: P )
assume A34:
b in Ball x,
r
;
b in f .: P
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 A34, METRIC_1:12;
then
|.(bb2 - xx2).| < r
by EUCLID:def 6;
then A35:
sqrt (Sum (sqr (abs (bb2 - xx2)))) < r
by EUCLID:29;
reconsider k =
bb as
Element of
REAL (i + j) ;
len k = i + j
by FINSEQ_1:def 18;
then consider g,
h being
FinSequence of
REAL such that A36:
len g = i
and A37:
len h = j
and A38:
k = g ^ h
by FINSEQ_2:26;
reconsider hh =
h as
Point of
(Euclid j) by A37, Th17;
reconsider gg =
g as
Point of
(Euclid i) by A36, Th17;
consider g,
h being
FinSequence of
REAL such that A39:
g = gg
and A40:
h = hh
and A41:
f . gg,
hh = g ^ h
by A3;
reconsider gg2 =
gg,
a12 =
a `1 as
Element of
REAL i ;
A42:
(
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
set such that A43:
p in the
carrier of
(Euclid i)
and A44:
q in the
carrier of
(Euclid j)
and A45:
a = [p,q]
by A4, ZFMISC_1:def 2;
reconsider q =
q as
Element of the
carrier of
(Euclid j) by A44;
reconsider p =
p as
Element of the
carrier of
(Euclid i) by A43;
consider fi,
fj being
FinSequence of
REAL such that A46:
fi = p
and A47:
fj = q
and A48:
f . p,
q = fi ^ fj
by A3;
A49:
(
len fi = i &
len fj = j )
by A46, A47, FINSEQ_1:def 18;
(
len g = i &
len h = j )
by A39, A40, FINSEQ_1:def 18;
then
sqrt (Sum (sqr ((abs (g - fi)) ^ (abs (h - fj))))) < r
by A31, A38, A45, A48, A39, A40, A49, A35, Th16;
then
sqrt (Sum ((sqr (abs (g - fi))) ^ (sqr (abs (h - fj))))) < r
by Th11;
then A50:
sqrt ((Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj))))) < r
by RVSUM_1:105;
reconsider hh2 =
hh,
a22 =
a `2 as
Element of
REAL j ;
A51:
a22 = q
by A45, MCART_1:7;
0 <= Sum (sqr (abs (g - fi)))
by RVSUM_1:116;
then
(
0 <= Sum (sqr (abs (hh2 - a22))) &
(Sum (sqr (abs (hh2 - a22)))) + 0 <= (Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj)))) )
by A47, A40, A51, RVSUM_1:116, XREAL_1:9;
then
sqrt (Sum (sqr (abs (hh2 - a22)))) <= sqrt ((Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj)))))
by SQUARE_1:94;
then
sqrt (Sum (sqr (abs (hh2 - a22)))) < r
by A50, XXREAL_0:2;
then
|.(hh2 - a22).| < r
by EUCLID:29;
then A52:
(Pitag_dist j) . hh2,
a22 < r
by EUCLID:def 6;
A53:
a12 = p
by A45, MCART_1:7;
0 <= Sum (sqr (abs (h - fj)))
by RVSUM_1:116;
then
(
0 <= Sum (sqr (abs (gg2 - a12))) &
(Sum (sqr (abs (gg2 - a12)))) + 0 <= (Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj)))) )
by A46, A39, A53, RVSUM_1:116, XREAL_1:9;
then
sqrt (Sum (sqr (abs (gg2 - a12)))) <= sqrt ((Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj)))))
by SQUARE_1:94;
then
sqrt (Sum (sqr (abs (gg2 - a12)))) < r
by A50, XXREAL_0:2;
then
|.(gg2 - a12).| < r
by EUCLID:29;
then A54:
(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 Th20;
then
dist [gg,hh],
a < r
by A4, A54, A52, A42, MCART_1:23;
then
[g,h] in Ball a,
r
by A39, A40, METRIC_1:12;
then
[g,h] in P
by A33;
hence
b in f .: P
by A38, A39, A40, A41, FUNCT_2:43;
verum
end;
f .: P is
Subset of
(Euclid (i + j))
by TOPMETR:16;
then
f .: P in Family_open_set (Euclid (i + j))
by A28, PCOMPS_1:def 5;
then
f .: P in the
topology of
(TopSpaceMetr (Euclid (i + j)))
by TOPMETR:16;
hence
(f " ) " P in the
topology of
(TopSpaceMetr (Euclid (i + j)))
by A5, A10, TOPS_2:67;
PRE_TOPC:def 5 verum
end;
A55:
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)));
( P is open implies f " P is open )
assume
P is
open
;
f " P is open
then
P in the
topology of
(TopSpaceMetr (Euclid (i + j)))
by PRE_TOPC:def 5;
then A56:
P in Family_open_set (Euclid (i + j))
by TOPMETR:16;
A57:
for
x being
Point of
(max-Prod2 (Euclid i),(Euclid j)) st
x in f " P holds
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));
( x in f " P implies ex r being Real st
( r > 0 & Ball x,r c= f " P ) )
assume A58:
x in f " P
;
ex r being Real st
( r > 0 & Ball x,r c= f " P )
then
f . x in the
carrier of
(TopSpaceMetr (Euclid (i + j)))
by FUNCT_2:7;
then reconsider fx =
f . x as
Point of
(Euclid (i + j)) by TOPMETR:16;
f . x in P
by A58, FUNCT_2:46;
then consider r being
Real such that A59:
r > 0
and A60:
Ball fx,
r c= P
by A56, PCOMPS_1:def 5;
take r1 =
r / 2;
( r1 > 0 & Ball x,r1 c= f " P )
thus
r1 > 0
by A59, XREAL_1:141;
Ball x,r1 c= f " P
let b be
set ;
TARSKI:def 3 ( not b in Ball x,r1 or b in f " P )
assume A61:
b in Ball x,
r1
;
b in f " P
then reconsider bb =
b as
Point of
(max-Prod2 (Euclid i),(Euclid j)) ;
A62:
dist bb,
x < r1
by A61, METRIC_1:12;
bb in the
carrier of
(max-Prod2 (Euclid i),(Euclid j))
;
then A63:
bb in the
carrier of
(TopSpaceMetr (max-Prod2 (Euclid i),(Euclid j)))
by TOPMETR:16;
then
f . bb in the
carrier of
(TopSpaceMetr (Euclid (i + j)))
by FUNCT_2:7;
then reconsider fb =
f . b as
Point of
(Euclid (i + j)) by TOPMETR:16;
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 A64:
(
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;
A65:
dist [b1,b2],
[x1,x2] = max (dist b1,x1),
(dist b2,x2)
by Th20;
dist b2,
x2 <= max (dist b1,x1),
(dist b2,x2)
by XXREAL_0:25;
then A66:
dist b2,
x2 < r1
by A64, A65, A62, 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 A67:
(
b1f = b1 &
b2f = b2 )
and A68:
f . b1,
b2 = b1f ^ b2f
by A3;
A69:
(
len b1f = i &
len b2f = j )
by A67, FINSEQ_1:def 18;
dist b1,
x1 <= max (dist b1,x1),
(dist b2,x2)
by XXREAL_0:25;
then
dist b1,
x1 < r1
by A64, A65, A62, XXREAL_0:2;
then A70:
((Pitag_dist i) . b1i,x1i) + ((Pitag_dist j) . b2i,x2i) < r1 + r1
by A66, XREAL_1:10;
(
0 <= Sum (sqr (b1i - x1i)) &
0 <= Sum (sqr (b2i - x2i)) )
by RVSUM_1:116;
then
sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) <= |.(b1i - x1i).| + (sqrt (Sum (sqr (b2i - x2i))))
by TOPREAL6:6;
then
sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) <= ((Pitag_dist i) . b1i,x1i) + |.(b2i - x2i).|
by EUCLID:def 6;
then A71:
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 A72:
(
x1f = x1 &
x2f = x2 )
and A73:
f . x1,
x2 = x1f ^ x2f
by A3;
A74:
(
len x1f = i &
len x2f = j )
by A72, FINSEQ_1:def 18;
(Pitag_dist (i + j)) . fbb,
fxx =
|.(fbb - fxx).|
by EUCLID:def 6
.=
sqrt (Sum (sqr (abs (fbb - fxx))))
by EUCLID:29
.=
sqrt (Sum (sqr ((abs (b1i - x1i)) ^ (abs (b2i - x2i)))))
by A64, A67, A68, A72, A73, A69, A74, Th16
.=
sqrt (Sum ((sqr (abs (b1i - x1i))) ^ (sqr (abs (b2i - x2i)))))
by Th11
.=
sqrt ((Sum (sqr (abs (b1i - x1i)))) + (Sum (sqr (abs (b2i - x2i)))))
by RVSUM_1:105
.=
sqrt ((Sum (sqr (abs (b1i - x1i)))) + (Sum (sqr (b2i - x2i))))
by EUCLID:29
.=
sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i))))
by EUCLID:29
;
then
dist fb,
fx < r
by A71, A70, XXREAL_0:2;
then
f . b in Ball fx,
r
by METRIC_1:12;
hence
b in f " P
by A60, A63, FUNCT_2:46;
verum
end;
f " P is
Subset of
(max-Prod2 (Euclid i),(Euclid j))
by TOPMETR:16;
then
f " P in Family_open_set (max-Prod2 (Euclid i),(Euclid j))
by A57, PCOMPS_1:def 5;
hence
f " P in the
topology of
(TopSpaceMetr (max-Prod2 (Euclid i),(Euclid j)))
by TOPMETR:16;
PRE_TOPC:def 5 verum
end;
[#] (TopSpaceMetr (Euclid (i + j))) <> {}
;
hence
f is
continuous
by A55, TOPS_2:55;
f " is continuous
[#] (TopSpaceMetr (max-Prod2 (Euclid i),(Euclid j))) <> {}
;
hence
f " is
continuous
by A26, TOPS_2:55;
verum
end;
hence
[:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], TopSpaceMetr (Euclid (i + j)) are_homeomorphic
by Th25; verum