let n be Nat; for p0 being Point of (TOP-REAL (n + 1)) st p0 = Base_FinSeq ((n + 1),(n + 1)) holds
TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic
let p0 be Point of (TOP-REAL (n + 1)); ( p0 = Base_FinSeq ((n + 1),(n + 1)) implies TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic )
assume A1:
p0 = Base_FinSeq ((n + 1),(n + 1))
; TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic
set T = TOP-REAL n;
set S = TPlane (p0,(0. (TOP-REAL (n + 1))));
defpred S1[ set , set ] means for p being Element of (TOP-REAL n) st $1 = p holds
$2 = p ^ <*0*>;
A2:
for p being Element of (TOP-REAL n) holds p ^ <*0*> is Element of (TPlane (p0,(0. (TOP-REAL (n + 1)))))
proof
let p be
Element of
(TOP-REAL n);
p ^ <*0*> is Element of (TPlane (p0,(0. (TOP-REAL (n + 1)))))
A3:
len p = n
by CARD_1:def 7;
A4:
len (p ^ <*0*>) = n + 1
by CARD_1:def 7;
rng (p ^ <*0*>) c= REAL
;
then
p ^ <*0*> in REAL (n + 1)
by A4, FINSEQ_2:132;
then reconsider q =
p ^ <*0*> as
Point of
(TOP-REAL (n + 1)) by EUCLID:22;
reconsider r0 =
0 as
Real ;
(
dom p0 = Seg (n + 1) &
dom q = Seg (n + 1) )
by FINSEQ_1:89;
then
(dom p0) /\ (dom q) = Seg (n + 1)
;
then A5:
dom (mlt (p0,q)) = Seg (n + 1)
by VALUED_1:def 4;
for
y being
object holds
(
y in rng (mlt (p0,q)) iff
y = r0 )
proof
let y be
object ;
( y in rng (mlt (p0,q)) iff y = r0 )
set f =
mlt (
p0,
q);
hereby ( y = r0 implies y in rng (mlt (p0,q)) )
end;
assume A11:
y = r0
;
y in rng (mlt (p0,q))
consider x being
object such that A12:
x in Seg (n + 1)
by XBOOLE_0:def 1;
y = (mlt (p0,q)) . x
by A11, A12, A6;
hence
y in rng (mlt (p0,q))
by A12, A5, FUNCT_1:def 3;
verum
end;
then
mlt (
p0,
q)
= (Seg (n + 1)) --> r0
by A5, FUNCOP_1:9, TARSKI:def 1;
then A14:
mlt (
p0,
q)
= (n + 1) |-> r0
by FINSEQ_2:def 2;
A15:
|(p0,q)| =
Sum (mlt (p0,q))
by RVSUM_1:def 16
.=
(n + 1) * r0
by A14, RVSUM_1:80
.=
0
;
|(p0,(q - (0. (TOP-REAL (n + 1)))))| =
|(p0,q)| - |(p0,(0. (TOP-REAL (n + 1))))|
by EUCLID_2:27
.=
|(p0,q)| - 0
by EUCLID_2:32
.=
0
by A15
;
then
p ^ <*0*> in Plane (
p0,
(0. (TOP-REAL (n + 1))))
;
then
p ^ <*0*> in [#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))
by PRE_TOPC:def 5;
hence
p ^ <*0*> is
Element of
(TPlane (p0,(0. (TOP-REAL (n + 1)))))
;
verum
end;
A16:
for x being Element of (TOP-REAL n) ex y being Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) st S1[x,y]
consider f being Function of (TOP-REAL n),(TPlane (p0,(0. (TOP-REAL (n + 1))))) such that
A17:
for x being Element of (TOP-REAL n) holds S1[x,f . x]
from FUNCT_2:sch 3(A16);
A18:
dom f = [#] (TOP-REAL n)
by FUNCT_2:def 1;
A19:
for y being object holds
( y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) iff ex x being object st
( x in dom f & y = f . x ) )
proof
let y be
object ;
( y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) iff ex x being object st
( x in dom f & y = f . x ) )
hereby ( ex x being object st
( x in dom f & y = f . x ) implies y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) )
assume
y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))
;
ex x being object st
( x in dom f & y = f . x )then
y in Plane (
p0,
(0. (TOP-REAL (n + 1))))
by PRE_TOPC:def 5;
then consider q being
Point of
(TOP-REAL (n + 1)) such that A20:
(
y = q &
|(p0,(q - (0. (TOP-REAL (n + 1)))))| = 0 )
;
A21:
(
len q = n + 1 &
rng q c= REAL )
by CARD_1:def 7;
then reconsider q1 =
q as
FinSequence of
REAL by FINSEQ_1:def 4;
set p =
q1 | n;
reconsider x =
q1 | n as
object ;
take x =
x;
( x in dom f & y = f . x )
0 + n <= 1
+ n
by XREAL_1:6;
then A22:
len (q1 | n) = n
by A21, FINSEQ_1:59;
A23:
rng (q1 | n) c= REAL
;
A24:
q1 | n in REAL n
by A22, A23, FINSEQ_2:132;
hence
x in dom f
by A18, EUCLID:22;
y = f . xreconsider x1 =
x as
Element of
(TOP-REAL n) by A24, EUCLID:22;
S1[
x1,
f . x1]
by A17;
then A25:
f . x = (q1 | n) ^ <*0*>
;
A26:
q = (q1 | n) ^ <*(q . (n + 1))*>
by CARD_1:def 7, FINSEQ_3:55;
A27:
|(p0,(q - (0. (TOP-REAL (n + 1)))))| =
|(p0,q)| - |(p0,(0. (TOP-REAL (n + 1))))|
by EUCLID_2:27
.=
|(p0,q)| - 0
by EUCLID_2:32
.=
|(p0,q)|
;
reconsider f0 =
0. (TOP-REAL n) as
FinSequence of
REAL by EUCLID:24;
rng <*1*> c= REAL
;
then reconsider f1 =
<*1*> as
FinSequence of
REAL by FINSEQ_1:def 4;
reconsider f3 =
<*(q . (n + 1))*> as
FinSequence of
REAL by RVSUM_1:145;
q1 | n in REAL n
by A22, A23, FINSEQ_2:132;
then reconsider p1 =
q1 | n as
Point of
(TOP-REAL n) by EUCLID:22;
A28:
|((f0 ^ f1),((q1 | n) ^ f3))| = 0
by A1, A26, A27, A20, Th28;
reconsider n1 =
n as
Element of
NAT by ORDINAL1:def 12;
0. (TOP-REAL n) in the
carrier of
(TOP-REAL n)
;
then
f0 in REAL n
by EUCLID:22;
then
f0 in Funcs (
(Seg n1),
REAL)
by FINSEQ_2:93;
then consider g being
Function such that A29:
(
f0 = g &
dom g = Seg n1 &
rng g c= REAL )
by FUNCT_2:def 2;
A30:
len f0 = len (q1 | n)
by A22, A29, FINSEQ_1:def 3;
len f1 =
1
by FINSEQ_1:39
.=
len f3
by FINSEQ_1:39
;
then
|((0. (TOP-REAL n)),p1)| + |(f1,f3)| = 0
by A28, A30, Th15;
then
0 + |(f1,f3)| = 0
by EUCLID_2:33;
then
Sum (mlt (f1,f3)) = 0
by RVSUM_1:def 16;
then
Sum <*(1 * (q . (n + 1)))*> = 0
by RVSUM_1:62;
hence
y = f . x
by A20, A25, A26, RVSUM_1:73;
verum
end;
given x being
object such that A31:
(
x in dom f &
y = f . x )
;
y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))
reconsider p =
x as
Element of
(TOP-REAL n) by A31;
S1[
p,
f . p]
by A17;
hence
y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))
by A31;
verum
end;
then A32:
rng f = [#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))
by FUNCT_1:def 3;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
then A35:
f is one-to-one
;
set T1 = TOP-REAL (n + 1);
A36:
for p1 being Point of (TOP-REAL n) holds f . p1 is Point of (TOP-REAL (n + 1))
A37:
for p1 being Point of (TOP-REAL n)
for q1 being Point of (TOP-REAL (n + 1)) st q1 = f . p1 holds
|.p1.| = |.q1.|
A44:
for p1, p2 being Point of (TOP-REAL n)
for q1, q2 being Point of (TOP-REAL (n + 1)) st q1 = f . p1 & q2 = f . p2 holds
f . (p1 - p2) = q1 - q2
A56:
f .: ([#] (TOP-REAL n)) = [#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))
by A32, RELSET_1:22;
for P being Subset of (TOP-REAL n) holds
( P is closed iff f .: P is closed )
proof
let P be
Subset of
(TOP-REAL n);
( P is closed iff f .: P is closed )
hereby ( f .: P is closed implies P is closed )
assume
P is
closed
;
f .: P is closed then A57:
([#] (TOP-REAL n)) \ P in the
topology of
(TOP-REAL n)
by PRE_TOPC:def 2, PRE_TOPC:def 3;
set FQ =
{ (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } ;
for
x being
object st
x in { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } holds
x in bool ([#] (TOP-REAL (n + 1)))
then reconsider FQ =
{ (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } as
Subset-Family of
(TOP-REAL (n + 1)) by TARSKI:def 3;
B60:
for
Q being
Subset of
(TOP-REAL (n + 1)) st
Q in FQ holds
Q is
open
set Q =
union FQ;
union FQ is
open
by B60, TOPS_2:def 1, TOPS_2:19;
then A61:
union FQ in the
topology of
(TOP-REAL (n + 1))
by PRE_TOPC:def 2;
for
y being
Element of
(TPlane (p0,(0. (TOP-REAL (n + 1))))) holds
(
y in f .: (([#] (TOP-REAL n)) \ P) iff
y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) )
proof
let y be
Element of
(TPlane (p0,(0. (TOP-REAL (n + 1)))));
( y in f .: (([#] (TOP-REAL n)) \ P) iff y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) )
hereby ( y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) implies y in f .: (([#] (TOP-REAL n)) \ P) )
assume
y in f .: (([#] (TOP-REAL n)) \ P)
;
y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1))))))then consider x being
object such that A62:
(
x in dom f &
x in ([#] (TOP-REAL n)) \ P &
y = f . x )
by FUNCT_1:def 6;
reconsider p =
x as
Point of
(TOP-REAL n) by A62;
reconsider q =
y as
Point of
(TOP-REAL (n + 1)) by A62, A36;
consider r being
Real such that A63:
(
r > 0 &
Ball (
p,
r)
c= ([#] (TOP-REAL n)) \ P )
by A62, A57, Th24;
A64:
Ball (
q,
r)
in FQ
by A62, A63;
q in Ball (
q,
r)
by A63, JORDAN:16;
then
y in union FQ
by A64, TARSKI:def 4;
hence
y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1))))))
by XBOOLE_0:def 4;
verum
end;
assume
y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1))))))
;
y in f .: (([#] (TOP-REAL n)) \ P)
then
y in union FQ
by XBOOLE_0:def 4;
then consider Y being
set such that A65:
(
y in Y &
Y in FQ )
by TARSKI:def 4;
consider q being
Point of
(TOP-REAL (n + 1)),
r being
Real such that A66:
Y = Ball (
q,
r)
and A67:
ex
p being
Point of
(TOP-REAL n) st
(
q = f . p &
Ball (
p,
r)
c= ([#] (TOP-REAL n)) \ P )
by A65;
consider p being
Point of
(TOP-REAL n) such that A68:
(
q = f . p &
Ball (
p,
r)
c= ([#] (TOP-REAL n)) \ P )
by A67;
consider x being
object such that A69:
(
x in dom f &
y = f . x )
by A19;
reconsider p1 =
x as
Point of
(TOP-REAL n) by A69;
reconsider q1 =
y as
Point of
(TOP-REAL (n + 1)) by A69, A36;
q1 in { qy where qy is Point of (TOP-REAL (n + 1)) : |.(qy - q).| < r }
by A65, A66, TOPREAL9:def 1;
then consider qy being
Point of
(TOP-REAL (n + 1)) such that A70:
(
qy = q1 &
|.(qy - q).| < r )
;
f . (p1 - p) = q1 - q
by A69, A68, A44;
then
|.(p1 - p).| < r
by A70, A37;
then
p1 in { px where px is Point of (TOP-REAL n) : |.(px - p).| < r }
;
then
p1 in Ball (
p,
r)
by TOPREAL9:def 1;
hence
y in f .: (([#] (TOP-REAL n)) \ P)
by A69, A68, FUNCT_1:def 6;
verum
end; then A71:
f .: (([#] (TOP-REAL n)) \ P) = (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1))))))
by SUBSET_1:3;
([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) = (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1))))))
by A71, A35, A56, FUNCT_1:64;
then
([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) in the
topology of
(TPlane (p0,(0. (TOP-REAL (n + 1)))))
by A61, PRE_TOPC:def 4;
hence
f .: P is
closed
by PRE_TOPC:def 2, PRE_TOPC:def 3;
verum
end;
assume
f .: P is
closed
;
P is closed
then
([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) in the
topology of
(TPlane (p0,(0. (TOP-REAL (n + 1)))))
by PRE_TOPC:def 3, PRE_TOPC:def 2;
then consider Q being
Subset of
(TOP-REAL (n + 1)) such that A72:
(
Q in the
topology of
(TOP-REAL (n + 1)) &
([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) = Q /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) )
by PRE_TOPC:def 4;
for
p being
Point of
(TOP-REAL n) st
p in ([#] (TOP-REAL n)) \ P holds
ex
r being
Real st
(
r > 0 &
Ball (
p,
r)
c= ([#] (TOP-REAL n)) \ P )
proof
let p be
Point of
(TOP-REAL n);
( p in ([#] (TOP-REAL n)) \ P implies ex r being Real st
( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) )
assume
p in ([#] (TOP-REAL n)) \ P
;
ex r being Real st
( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P )
then
f . p in f .: (([#] (TOP-REAL n)) \ P)
by A18, FUNCT_1:def 6;
then A73:
f . p in ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P)
by A56, A35, FUNCT_1:64;
reconsider q =
f . p as
Point of
(TOP-REAL (n + 1)) by A36;
q in Q
by A72, A73, XBOOLE_0:def 4;
then consider r being
Real such that A74:
(
r > 0 &
Ball (
q,
r)
c= Q )
by A72, Th24;
take
r
;
( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P )
thus
r > 0
by A74;
Ball (p,r) c= ([#] (TOP-REAL n)) \ P
let x be
object ;
TARSKI:def 3 ( not x in Ball (p,r) or x in ([#] (TOP-REAL n)) \ P )
assume
x in Ball (
p,
r)
;
x in ([#] (TOP-REAL n)) \ P
then
x in { px where px is Point of (TOP-REAL n) : |.(px - p).| < r }
by TOPREAL9:def 1;
then consider p1 being
Point of
(TOP-REAL n) such that A75:
(
x = p1 &
|.(p1 - p).| < r )
;
reconsider q1 =
f . p1 as
Point of
(TOP-REAL (n + 1)) by A36;
f . (p1 - p) = q1 - q
by A44;
then
|.(q1 - q).| < r
by A75, A37;
then
q1 in { qx where qx is Point of (TOP-REAL (n + 1)) : |.(qx - q).| < r }
;
then
q1 in Ball (
q,
r)
by TOPREAL9:def 1;
then
q1 in Q /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1))))))
by A74, XBOOLE_0:def 4;
then
not
q1 in f .: P
by A72, XBOOLE_0:def 5;
then
not
x in P
by A18, A75, FUNCT_1:def 6;
hence
x in ([#] (TOP-REAL n)) \ P
by A75, XBOOLE_0:def 5;
verum
end;
then
([#] (TOP-REAL n)) \ P is
open
by Th24, PRE_TOPC:def 2;
hence
P is
closed
by PRE_TOPC:def 3;
verum
end;
hence
TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic
by T_0TOPSP:def 1, A18, A32, A35, TOPS_2:58; verum