set T = TOP-REAL n;
set E = Euclid n;
set TE = TopSpaceMetr (Euclid n);
A1:
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n)
by EUCLID:def 8;
thus
TOP-REAL n is add-continuous
TOP-REAL n is Mult-continuous proof
let x1,
x2 be
Point of
(TOP-REAL n);
RLTOPSP1:def 8 for b1 being Element of bool the carrier of (TOP-REAL n) holds
( not b1 is open or not x1 + x2 in b1 or ex b2, b3 being Element of bool the carrier of (TOP-REAL n) st
( b2 is open & b3 is open & x1 in b2 & x2 in b3 & b2 + b3 c= b1 ) )let V be
Subset of
(TOP-REAL n);
( not V is open or not x1 + x2 in V or ex b1, b2 being Element of bool the carrier of (TOP-REAL n) st
( b1 is open & b2 is open & x1 in b1 & x2 in b2 & b1 + b2 c= V ) )
assume that A2:
V is
open
and A3:
x1 + x2 in V
;
ex b1, b2 being Element of bool the carrier of (TOP-REAL n) st
( b1 is open & b2 is open & x1 in b1 & x2 in b2 & b1 + b2 c= V )
reconsider X1 =
x1,
X2 =
x2,
X12 =
x1 + x2 as
Point of
(Euclid n) by A1, TOPMETR:12;
reconsider v =
V as
Subset of
(TopSpaceMetr (Euclid n)) by A1;
V in the
topology of
(TOP-REAL n)
by A2, PRE_TOPC:def 2;
then
v is
open
by A1, PRE_TOPC:def 2;
then consider r being
Real such that A4:
r > 0
and A5:
Ball (
X12,
r)
c= v
by A3, TOPMETR:15;
set r2 =
r / 2;
reconsider B1 =
Ball (
X1,
(r / 2)),
B2 =
Ball (
X2,
(r / 2)) as
Subset of
(TOP-REAL n) by A1, TOPMETR:12;
take
B1
;
ex b1 being Element of bool the carrier of (TOP-REAL n) st
( B1 is open & b1 is open & x1 in B1 & x2 in b1 & B1 + b1 c= V )
take
B2
;
( B1 is open & B2 is open & x1 in B1 & x2 in B2 & B1 + B2 c= V )
thus
(
B1 is
open &
B2 is
open &
x1 in B1 &
x2 in B2 )
by A4, GOBOARD6:1, GOBOARD6:3, XREAL_1:215;
B1 + B2 c= V
let x be
object ;
TARSKI:def 3 ( not x in B1 + B2 or x in V )
assume
x in B1 + B2
;
x in V
then
x in { (b1 + b2) where b1, b2 is Element of (TOP-REAL n) : ( b1 in B1 & b2 in B2 ) }
by RUSUB_4:def 9;
then consider b1,
b2 being
Element of
(TOP-REAL n) such that A6:
x = b1 + b2
and A7:
b1 in B1
and A8:
b2 in B2
;
reconsider e1 =
b1,
e2 =
b2,
e12 =
b1 + b2 as
Point of
(Euclid n) by A1, TOPMETR:12;
reconsider y1 =
x1,
y2 =
x2,
c1 =
b1,
c2 =
b2 as
Element of
REAL n by EUCLID:22;
dist (
X2,
e2)
< r / 2
by A8, METRIC_1:11;
then A9:
|.(y2 - c2).| < r / 2
by SPPOL_1:5;
dist (
X1,
e1)
< r / 2
by A7, METRIC_1:11;
then
|.(y1 - c1).| < r / 2
by SPPOL_1:5;
then A10:
|.(y1 - c1).| + |.(y2 - c2).| < (r / 2) + (r / 2)
by A9, XREAL_1:8;
A11:
(y1 + y2) - (c1 + c2) =
(y1 + y2) + (- (c2 + c1))
by RVSUM_1:31
.=
(y1 + y2) + ((- c2) + (- c1))
by RVSUM_1:26
.=
((y1 + y2) + (- c2)) + (- c1)
by RVSUM_1:15
.=
((y2 + (- c2)) + y1) + (- c1)
by RVSUM_1:15
.=
(y2 + (- c2)) + (y1 + (- c1))
by RVSUM_1:15
.=
(y2 - c2) + (y1 + (- c1))
by RVSUM_1:31
.=
(y2 - c2) + (y1 - c1)
by RVSUM_1:31
;
A12:
dist (
X12,
e12)
= |.((y1 - c1) + (y2 - c2)).|
by A11, SPPOL_1:5;
|.((y1 - c1) + (y2 - c2)).| <= |.(y1 - c1).| + |.(y2 - c2).|
by EUCLID:12;
then
dist (
X12,
e12)
< r
by A10, A12, XXREAL_0:2;
then
e12 in Ball (
X12,
r)
by METRIC_1:11;
hence
x in V
by A5, A6;
verum
end;
let a be Real; RLTOPSP1:def 9 for b1 being Element of the carrier of (TOP-REAL n)
for b2 being Element of bool the carrier of (TOP-REAL n) holds
( not b2 is open or not a * b1 in b2 or ex b3 being object ex b4 being Element of bool the carrier of (TOP-REAL n) st
( b4 is open & b1 in b4 & ( for b5 being object holds
( b3 <= |.(b5 - a).| or b5 * b4 c= b2 ) ) ) )
let x be Point of (TOP-REAL n); for b1 being Element of bool the carrier of (TOP-REAL n) holds
( not b1 is open or not a * x in b1 or ex b2 being object ex b3 being Element of bool the carrier of (TOP-REAL n) st
( b3 is open & x in b3 & ( for b4 being object holds
( b2 <= |.(b4 - a).| or b4 * b3 c= b1 ) ) ) )
let V be Subset of (TOP-REAL n); ( not V is open or not a * x in V or ex b1 being object ex b2 being Element of bool the carrier of (TOP-REAL n) st
( b2 is open & x in b2 & ( for b3 being object holds
( b1 <= |.(b3 - a).| or b3 * b2 c= V ) ) ) )
assume that
A13:
V is open
and
A14:
a * x in V
; ex b1 being object ex b2 being Element of bool the carrier of (TOP-REAL n) st
( b2 is open & x in b2 & ( for b3 being object holds
( b1 <= |.(b3 - a).| or b3 * b2 c= V ) ) )
reconsider X = x, AX = a * x as Point of (Euclid n) by A1, TOPMETR:12;
reconsider v = V as Subset of (TopSpaceMetr (Euclid n)) by A1;
V in the topology of (TOP-REAL n)
by A13, PRE_TOPC:def 2;
then
v is open
by A1, PRE_TOPC:def 2;
then consider r being Real such that
A15:
r > 0
and
A16:
Ball (AX,r) c= v
by A14, TOPMETR:15;
set r2 = r / 2;
A17:
r / 2 > 0
by A15, XREAL_1:215;
then A18:
(r / 2) / 2 > 0
by XREAL_1:215;
ex m being positive Real st |.a.| * m < r / 2
then consider m being positive Real such that
A20:
|.a.| * m < r / 2
;
reconsider B = Ball (X,m) as Subset of (TOP-REAL n) by A1, TOPMETR:12;
reconsider nr = (r / 2) / (|.x.| + m) as positive Real by A17, XREAL_1:139;
take
nr
; ex b1 being Element of bool the carrier of (TOP-REAL n) st
( b1 is open & x in b1 & ( for b2 being object holds
( nr <= |.(b2 - a).| or b2 * b1 c= V ) ) )
take
B
; ( B is open & x in B & ( for b1 being object holds
( nr <= |.(b1 - a).| or b1 * B c= V ) ) )
thus
( B is open & x in B )
by GOBOARD6:1, GOBOARD6:3; for b1 being object holds
( nr <= |.(b1 - a).| or b1 * B c= V )
let s be Real; ( nr <= |.(s - a).| or s * B c= V )
assume A21:
|.(s - a).| < nr
; s * B c= V
let z be object ; TARSKI:def 3 ( not z in s * B or z in V )
assume
z in s * B
; z in V
then
z in { (s * b) where b is Element of (TOP-REAL n) : b in B }
by CONVEX1:def 1;
then consider b being Element of (TOP-REAL n) such that
A22:
z = s * b
and
A23:
b in B
;
reconsider e = b, se = s * b as Point of (Euclid n) by A1, TOPMETR:12;
reconsider y = x, c = b as Element of REAL n by EUCLID:22;
reconsider Y = y, C = c as Element of n -tuples_on REAL by EUCLID:def 1;
c =
C - (n |-> 0)
by RVSUM_1:32
.=
C - (Y - Y)
by RVSUM_1:37
.=
(C - Y) + Y
by RVSUM_1:41
;
then A24:
|.c.| <= |.(c - y).| + |.y.|
by EUCLID:12;
A25:
dist (X,e) < m
by A23, METRIC_1:11;
then
|.(c - y).| < m
by SPPOL_1:5;
then
|.(c - y).| + |.y.| <= m + |.x.|
by XREAL_1:6;
then
|.c.| <= m + |.x.|
by A24, XXREAL_0:2;
then A26:
nr * |.c.| <= nr * (m + |.x.|)
by XREAL_1:64;
(a * y) + (- (a * c)) =
(a * y) + ((- 1) * (a * c))
by RVSUM_1:54
.=
(a * y) + (((- 1) * a) * c)
by RVSUM_1:49
.=
(a * y) + (a * ((- 1) * c))
by RVSUM_1:49
.=
a * (y + ((- 1) * c))
by RVSUM_1:51
.=
a * (y + (- c))
by RVSUM_1:54
.=
a * (y - c)
by RVSUM_1:31
;
then A27:
|.((a * y) + (- (a * c))).| = |.a.| * |.(y - c).|
by EUCLID:11;
( |.a.| >= 0 & |.(y - c).| = dist (X,e) )
by COMPLEX1:46, SPPOL_1:5;
then
|.((a * y) + (- (a * c))).| <= |.a.| * m
by A25, A27, XREAL_1:64;
then A28:
|.((a * y) + (- (a * c))).| < r / 2
by A20, XXREAL_0:2;
(a * c) + (- (s * c)) =
(a * c) + ((- 1) * (s * c))
by RVSUM_1:54
.=
(a * c) + (((- 1) * s) * c)
by RVSUM_1:49
.=
(a + ((- 1) * s)) * c
by RVSUM_1:50
;
then |.((a * c) + (- (s * c))).| =
|.(a - s).| * |.c.|
by EUCLID:11
.=
|.(- (a - s)).| * |.c.|
by COMPLEX1:52
;
then
( nr * (|.x.| + m) = r / 2 & |.((a * c) + (- (s * c))).| <= nr * |.c.| )
by A21, XCMPLX_1:87, XREAL_1:64;
then
|.((a * c) + (- (s * c))).| <= r / 2
by A26, XXREAL_0:2;
then A29:
( |.(((a * y) + (- (a * c))) + ((a * c) + (- (s * c)))).| <= |.((a * y) + (- (a * c))).| + |.((a * c) + (- (s * c))).| & |.((a * y) + (- (a * c))).| + |.((a * c) + (- (s * c))).| < (r / 2) + (r / 2) )
by A28, EUCLID:12, XREAL_1:8;
(a * y) - (s * c) =
((a * Y) - (n |-> 0)) - (s * C)
by RVSUM_1:32
.=
((a * y) - ((a * C) - (a * C))) - (s * c)
by RVSUM_1:37
.=
(((a * y) - (a * C)) + (a * C)) - (s * c)
by RVSUM_1:41
.=
(((a * y) - (a * C)) + (a * C)) + (- (s * c))
by RVSUM_1:31
.=
((a * y) - (a * C)) + ((a * c) + (- (s * c)))
by RVSUM_1:15
.=
((a * y) + (- (a * c))) + ((a * c) + (- (s * c)))
by RVSUM_1:31
;
then
dist (AX,se) = |.(((a * y) + (- (a * c))) + ((a * c) + (- (s * c)))).|
by SPPOL_1:5;
then
dist (AX,se) < r
by A29, XXREAL_0:2;
then
se in Ball (AX,r)
by METRIC_1:11;
hence
z in V
by A16, A22; verum