:: Baire's Category Theorem and Some Spaces Generated from Real Normed Space
:: by Noboru Endou , Yasunari Shidama and Katsumasa Okamura
::
:: Received November 21, 2006
:: Copyright (c) 2006-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, XBOOLE_0, METRIC_1, PROB_1, REWRITE1, TARSKI, RELAT_1,
STRUCT_0, SUBSET_1, FUNCT_1, PCOMPS_1, REAL_1, PRE_TOPC, CARD_1, ARYTM_3,
NEWTON, XXREAL_0, NAT_1, SEQ_1, ZFMISC_1, MCART_1, ARYTM_1, BHSP_3,
SEQ_2, ORDINAL2, NORMSP_1, RELAT_2, ORDINAL1, METRIC_6, RCOMP_1,
COMPTS_1, WAYBEL_3, YELLOW_8, FRECHET, CONNSP_2, PARTFUN1, FCONT_1,
TMAP_1, CFCONT_1, RLTOPSP1, SUPINF_2, ALGSTR_0, RLVECT_1, SETFAM_1,
COMPLEX1, RLVECT_3, CARD_3, NORMSP_2, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS,
XCMPLX_0, XREAL_0, XXREAL_0, SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2,
BINOP_1, COMPLEX1, REAL_1, NAT_1, STRUCT_0, ALGSTR_0, PRE_TOPC, FRECHET,
NEWTON, FRECHET2, YELLOW_8, DOMAIN_1, WAYBEL_3, RLVECT_1, CONVEX1,
COMPTS_1, TBSP_1, TMAP_1, CONNSP_2, CARD_3, METRIC_1, METRIC_6, PCOMPS_1,
RUSUB_4, RLTOPSP1, NFCONT_1, SEQ_1, KURATO_2, NORMSP_0, NORMSP_1;
constructors SETFAM_1, DOMAIN_1, REAL_1, SQUARE_1, NEWTON, CONNSP_2, TBSP_1,
RUSUB_4, CONVEX1, TMAP_1, METRIC_6, WAYBEL_3, YELLOW_8, FRECHET,
FRECHET2, NFCONT_1, RLTOPSP1, RELSET_1, TOPS_2, BINOP_1, VFUNCT_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0,
STRUCT_0, TOPS_1, METRIC_1, PCOMPS_1, HAUSDORF, KURATO_2, RLTOPSP1,
FRECHET, NEWTON, NAT_1, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, RLVECT_1, RLTOPSP1, ALGSTR_0, PRE_TOPC;
equalities RLVECT_1, METRIC_1, PCOMPS_1, CONVEX1, RUSUB_4, SUBSET_1, STRUCT_0,
ALGSTR_0;
expansions TARSKI, RLVECT_1, METRIC_1, PRE_TOPC;
theorems TARSKI, XBOOLE_1, RLVECT_1, FRECHET, FRECHET2, YELLOW_8, WAYBEL12,
ZFMISC_1, TMAP_1, CONNSP_2, FUNCT_2, XBOOLE_0, XREAL_1, COMPLEX1,
XCMPLX_1, NORMSP_1, METRIC_1, METRIC_6, PCOMPS_1, SUBSET_1, PRE_TOPC,
BINOP_1, TOPS_1, NFCONT_1, NEWTON, XXREAL_0, FUNCT_1, TBSP_1, NAT_1,
ORDINAL1, TOPREAL6, PREPOWER, PARTFUN1, RELSET_1, TOPS_2, XREAL_0;
schemes BINOP_1, RECDEF_1, NAT_1;
begin :: Baire's Category Theorem
theorem
for X be non empty MetrSpace, Y be SetSequence of X st X is complete &
union rng Y = the carrier of X & for n be Nat holds (Y.n)` in
Family_open_set X holds ex n0 be Nat,
r be Real, x0 be Point of X st
0 < r & Ball(x0,r) c= Y.n0
proof
let X be non empty MetrSpace, Y be SetSequence of X;
assume that
A1: X is complete and
A2: union rng Y = the carrier of X and
A3: for n be Nat holds (Y.n)` in Family_open_set X;
defpred P[Nat,Point of X,Real,Point of X,Real] means ( 0 < $3 &
$3 < 1/(2|^$1) & Ball($2,$3) /\ Y.($1) = {}) implies ( 0 < $5 & $5 < 1/(2|^($1+
1)) & Ball($4,$5) c= Ball($2,($3)/2) & Ball($4,$5) /\ Y.($1+1) = {} );
assume
A4: not ex n0 be Nat, r be Real,x0 be Point of X st 0 < r &
Ball(x0,r) c= Y.n0;
now
set x0 = the Point of X;
A5: (Y.0)`` = (the carrier of X) \ ((Y.0)`) & Ball(x0,1) c= the carrier of X;
assume (Y.0)` = {};
hence contradiction by A4,A5;
end;
then consider z0 be object such that
A6: z0 in (Y.0)` by XBOOLE_0:def 1;
reconsider z0 as Element of X by A6;
(Y.0)` in Family_open_set X by A3;
then consider t01 be Real such that
A7: 0 < t01 and
A8: Ball(z0,t01) c= (Y.0)` by A6,PCOMPS_1:def 4;
reconsider t0=min(t01,1/2) as Element of REAL by XREAL_0:def 1;
t0 <= 1/2 by XXREAL_0:17;
then t0 < 1/1 by XXREAL_0:2;
then
A9: t0 < 1/(2 |^0) by NEWTON:4;
Ball(z0,t0) c= Ball(z0,t01) by PCOMPS_1:1,XXREAL_0:17;
then Ball(z0,t0) c= (Y.0)` by A8;
then Ball(z0,t0) misses (Y.0) by SUBSET_1:23;
then
A10: Ball(z0,t0) /\ Y.0 ={} by XBOOLE_0:def 7;
A11: for n being Nat, x be Point of X, r be Real ex x1 be Point
of X,r1 be Real st 0 < r & r < 1/(2|^n) & Ball(x,r) /\ Y.n = {} implies 0 < r1
& r1 < 1/(2|^(n+1)) & Ball(x1,r1) c= Ball(x,r/2) & Ball(x1,r1) /\ Y.(n+1) = {}
proof
let n be Nat, x be Point of X, r be Real;
now
0 < 2|^(n+2) by NEWTON:83;
then
A12: 0 < 1/(2|^(n+2)) by XREAL_1:139;
0 < 2|^(n+1) by NEWTON:83;
then
A13: 1/(2|^(n+1))/2 < 1/(2|^(n+1)) by XREAL_1:139,216;
2|^(n+2) = 2|^((n+1)+1) .= 2|^(n+1)*2 by NEWTON:6;
then
A14: 1/(2|^(n+2)) = 1/(2|^(n+1))/2 by XCMPLX_1:78;
assume that
A15: 0 < r and
r < 1/(2|^n) and
Ball(x,r) /\ Y.n ={};
not Ball(x,r/2) c= Y.(n+1) by A4,A15,XREAL_1:215;
then Ball(x,r/2) meets (Y.(n+1))` by SUBSET_1:24;
then consider z0 be object such that
A16: z0 in Ball(x,r/2) /\ (Y.(n+1))` by XBOOLE_0:4;
reconsider x1=z0 as Point of X by A16;
A17: (Y.(n+1))` in Family_open_set X by A3;
Ball(x,r/2) in Family_open_set X & (Y.(n+1))` in Family_open_set X
by A3,PCOMPS_1:29;
then Ball(x,r/2) /\ (Y.(n+1))` in Family_open_set X by PCOMPS_1:31;
then consider t02 be Real such that
A18: 0 < t02 and
A19: Ball(x1,t02) c= Ball(x,r/2) /\ (Y.(n+1))` by A16,PCOMPS_1:def 4;
A20: Ball(x1,t02) c= Ball(x,r/2) by A19,XBOOLE_1:18;
x1 in (Y.(n+1))` by A16,XBOOLE_0:def 4;
then consider t01 be Real such that
A21: 0 < t01 and
A22: Ball(x1,t01) c= (Y.(n+1))` by A17,PCOMPS_1:def 4;
reconsider r1=min(min(t01,t02),1/(2|^(n+2))) as Real;
A23: r1 <= min(t01,t02) by XXREAL_0:17;
min(t01,t02) <= t02 by XXREAL_0:17;
then
A24: Ball(x1,r1) c= Ball(x1,t02) by A23,PCOMPS_1:1,XXREAL_0:2;
min(t01,t02) <= t01 by XXREAL_0:17;
then Ball(x1,r1) c= Ball(x1,t01) by A23,PCOMPS_1:1,XXREAL_0:2;
then Ball(x1,r1) c= (Y.(n+1))` by A22;
then
A25: Ball(x1,r1) misses (Y.(n+1)) by SUBSET_1:23;
take x1,r1;
A26: r1 <= 1/(2|^(n+2)) by XXREAL_0:17;
0 < min(t01,t02) by A21,A18,XXREAL_0:15;
hence P[n,x,r,x1,r1] by A20,A14,A12,A13,A24,A25,A26,XBOOLE_0:def 7
,XBOOLE_1:1,XXREAL_0:2,15;
end;
hence thesis;
end;
ex x0 be sequence of X, r0 be Real_Sequence st x0.0=z0 & r0.0=t0 & for
n be Nat holds ( 0 < r0.n & r0.n < 1/(2|^n) & Ball(x0.n,r0.n) /\ Y.n
= {} implies 0 < r0.(n+1) & r0.(n+1) < 1/(2|^(n+1)) & Ball(x0.(n+1),r0.(n+1))
c= Ball(x0.n,(r0.n)/2) & Ball(x0.(n+1),r0.(n+1)) /\ Y.(n+1) = {} )
proof
defpred P1[Nat,Element of [:the carrier of X,REAL:], Element of
[:the carrier of X,REAL:]] means ( 0 < $2`2 & $2`2 < 1/(2|^$1) & Ball($2`1,$2`2
) /\ Y.($1) = {}) implies ( 0 < $3`2 & $3`2 < 1/(2|^($1+1)) & Ball($3`1,$3`2)
c= Ball($2`1,($2`2)/2) & Ball($3`1,$3`2) /\ Y.($1+1) = {} );
A27: for n being Nat for u being Element of [:the carrier of X,
REAL:] ex v being Element of [:the carrier of X,REAL:] st P1[n,u,v]
proof
let n be Nat, u be Element of [:the carrier of X,REAL:];
consider v1 being Element of X, v2 being Real such that
A28: P[n,u`1,u`2,v1,v2] by A11;
reconsider v2 as Element of REAL by XREAL_0:def 1;
take [v1,v2];
thus thesis by A28;
end;
consider f being sequence of [:the carrier of X,REAL:] such that
A29: f.0 = [z0,t0] & for n being Nat holds P1[n,f.n,f.(n+1)
] from RECDEF_1:sch 2(A27);
take pr1 f, pr2 f;
thus (pr1 f).0 = (f.0)`1 by FUNCT_2:def 5
.= z0 by A29;
thus (pr2 f).0 = (f.0)`2 by FUNCT_2:def 6
.= t0 by A29;
hereby
let i be Nat;
A30: i in NAT by ORDINAL1:def 12;
A31: (f.(i+1))`1 = (pr1 f).(i+1) & (f.(i+1))`2 = (pr2 f).(i+1) by
FUNCT_2:def 5,def 6;
(f.i)`1 = (pr1 f).i & (f.i)`2 = (pr2 f).i by FUNCT_2:def 5,def 6,A30;
hence P[i,(pr1 f).i,(pr2 f).i,(pr1 f).(i+1),(pr2 f).(i+1)] by A29,A31;
end;
end;
then consider x0 be sequence of X, r0 be Real_Sequence such that
A32: x0.0=z0 & r0.0=t0 and
A33: for n be Nat holds ( 0 < r0.n & r0.n < 1/(2|^n) & Ball(
x0.n,r0.n) /\ Y.n = {} implies 0 < r0.(n+1) & r0.(n+1) < 1/(2|^(n+1)) & Ball (
x0.(n+1),r0.(n+1)) c= Ball(x0.n,(r0.n)/2) & Ball(x0.(n+1),r0.(n+1)) /\ Y.(n+1)
= {} );
0 < 1/2;
then
A34: 0 < t0 by A7,XXREAL_0:15;
A35: for n be Nat holds 0 < r0.n & r0.n < 1/(2|^n) & Ball(x0.(n+1
),r0.(n+1)) c= Ball(x0.n,(r0.n)/2) & Ball(x0.n,r0.n) /\ Y.n ={}
proof
defpred PN[Nat] means
0 < r0.$1 & r0.$1 < 1/(2|^$1) & Ball(x0.(
$1+1),r0.($1+1)) c= Ball(x0.$1,(r0.$1)/2) & Ball(x0.$1,r0.$1) /\ Y.$1 = {};
A36: now
let n be Nat;
assume
A37: PN[n];
then
A38: Ball(x0.(n+1),r0.(n+1)) /\ Y.(n+1) = {} by A33;
0 < r0.(n+1) & r0.(n+1) < 1/(2|^(n+1)) by A33,A37;
hence PN[n+1] by A33,A38;
end;
A39: PN[0] by A34,A9,A10,A32,A33;
thus for n be Nat holds PN[n] from NAT_1:sch 2(A39,A36);
end;
A40: for m,k be Nat holds dist(x0.(m+k),x0.m) <= 1/(2|^m)*(1-1/(2
|^k))
proof
let m be Nat;
defpred PN[Nat] means
dist(x0.(m+$1),x0.m) <= 1/(2|^m)*(1-1/(2|^$1));
A41: now
let k be Nat;
assume PN[k];
then
A42: dist(x0.((m+k)+1),x0.(m+k)) + dist(x0.(m+k),x0.m) <= dist(x0.((m+k)
+1),x0.(m+k)) + 1/(2|^m)*(1-1/(2|^k)) by XREAL_1:6;
0 < r0.(m+k+1) & dist(x0.(m+k+1),x0.(m+k+1)) = 0 by A35,METRIC_1:1;
then
A43: x0.(m+k+1) in Ball(x0.(m+k+1),r0.(m+k+1)) by METRIC_1:11;
r0.(m+k) < 1/(2|^(m+k)) by A35;
then r0.(m+k)/2 < 1/(2|^(m+k))/2 by XREAL_1:74;
then r0.(m+k)/2 < 1/(2|^(m+k)*2) by XCMPLX_1:78;
then
A44: r0.(m+k)/2 < 1/(2|^(m+k+1)) by NEWTON:6;
Ball(x0.(m+k+1),r0.(m+k+1)) c= Ball(x0.(m+k),r0.(m+k)/2) by A35;
then dist(x0.(m+k+1),x0.(m+k)) < r0.(m+k)/2 by A43,METRIC_1:11;
then dist(x0.(m+k+1),x0.(m+k)) <= 1/(2|^(m+k+1)) by A44,XXREAL_0:2;
then
A45: dist(x0.((m+k)+1),x0.(m+k)) + 1/(2|^m)*(1-1/(2|^k)) <= 1/(2|^(m+k+1
)) + 1/(2|^m)*(1-1/(2|^k)) by XREAL_1:6;
2|^(m+(k+1)) = 2|^m * 2|^(k+1) by NEWTON:8;
then 1/(2|^(m+k+1)) = 1/(2|^m)/((2|^(k+1))/1) by XCMPLX_1:78
.= 1/(2|^m)*(1/(2|^(k+1))) by XCMPLX_1:79;
then
A46: 1/(2|^(m+k+1)) + 1/(2|^m)*(1-1/(2|^k)) = 1/(2|^m)*( 1 + ( 1/(2|^(k+
1)) - 1/(2|^k) ) )
.= 1/(2|^m)*( 1 + ( 1/((2|^k)*2) - 1/(2|^k) ) ) by NEWTON:6
.= 1/(2|^m)*( 1 + ( 1/(2|^k)/2 - 1/(2|^k) ) ) by XCMPLX_1:78
.= 1/(2|^m)*( 1 - 1/(2|^k)/2 )
.= 1/(2|^m)*( 1 - 1/((2|^k)*2) ) by XCMPLX_1:78;
dist(x0.((m+k)+1),x0.m) <= dist(x0.((m+k)+1),x0.(m+k)) + dist(x0.(m
+k),x0.m) by METRIC_1:4;
then
dist(x0.(m+(k+1)),x0.m) <= dist(x0.((m+k)+1),x0.(m+k)) + 1/(2|^m)*(
1-1/(2|^k)) by A42,XXREAL_0:2;
then dist(x0.(m+(k+1)),x0.m) <= 1/(2|^(m+k+1) ) + 1/(2|^m)*(1-1/(2|^k))
by A45,XXREAL_0:2;
hence PN[k+1] by A46,NEWTON:6;
end;
2|^0 = 1 by NEWTON:4;
then
A47: PN[0] by METRIC_1:1;
for k be Nat holds PN[k] from NAT_1:sch 2(A47,A41);
hence thesis;
end;
A48: now
let m be Nat;
hereby
let k be Nat;
A49: dist(x0.(m+k),x0.m) <= 1/(2|^m)*(1-1/(2|^k)) by A40;
0 < 2|^k by NEWTON:83;
then 0 < 1/(2|^k) by XREAL_1:139;
then
A50: 1-1/(2|^k) < 1-0 by XREAL_1:10;
0 < 2|^m by NEWTON:83;
then 0 < 1/(2|^m) by XREAL_1:139;
then 1/(2|^m)*(1-1/(2|^k)) < 1/(2|^m)*1 by A50,XREAL_1:68;
hence dist(x0.(m+k),x0.m) < 1/(2|^m) by A49,XXREAL_0:2;
end;
end;
now
let r be Real;
assume 0 < r;
then consider p1 be Nat such that
A51: 1/(2|^p1) <= r by PREPOWER:92;
reconsider p=p1+1 as Nat;
take p;
hereby
let n,m be Nat;
assume that
A52: n >= p and
A53: m >= p;
consider k1 be Nat such that
A54: n = p + k1 by A52,NAT_1:10;
reconsider k1 as Nat;
n = p + k1 by A54;
then
A55: dist(x0.n,x0.p) < 1/(2|^p) by A48;
consider k2 be Nat such that
A56: m = p + k2 by A53,NAT_1:10;
reconsider k2 as Nat;
A57: 1/(2|^p) = 1/((2|^p1)*2) by NEWTON:6
.= 1/(2|^p1)/2 by XCMPLX_1:78;
m = p + k2 by A56;
then
A58: dist(x0.n,x0.p) + dist(x0.p,x0.m) < 1/(2|^p) + 1/(2|^p) by A48,A55,
XREAL_1:8;
dist(x0.n,x0.m) <= dist(x0.n,x0.p) + dist(x0.p,x0.m) by METRIC_1:4;
then dist(x0.n,x0.m) < 1/(2|^p1) by A58,A57,XXREAL_0:2;
hence dist(x0.n,x0.m)<r by A51,XXREAL_0:2;
end;
end;
then x0 is Cauchy by TBSP_1:def 4;
then
A59: x0 is convergent by A1,TBSP_1:def 5;
A60: for m,k be Nat holds Ball(x0.(m+1+k),r0.(m+1+k)) c= Ball(x0
.m,(r0.m)/2)
proof
let m be Nat;
defpred PN[Nat] means
Ball(x0.(m+1+$1),r0.(m+1+$1)) c= Ball(x0.m,(r0.m)/2);
A61: now
let k be Nat;
assume
A62: PN[k];
0 < r0.(m+1+k) by A35;
then (r0.(m+1+k))/2 < r0.(m+1+k) by XREAL_1:216;
then
A63: Ball(x0.(m+1+k),(r0.(m+1+k))/2) c=Ball(x0.(m+1+k),r0.(m+1+k)) by
PCOMPS_1:1;
Ball(x0.(m+1+(k+1)),r0.(m+1+(k+1)))=Ball(x0.(m+1+k+1),r0.(m+1+k+1) );
then Ball(x0.(m+1+(k+1)),r0.(m+1+(k+1))) c= Ball(x0.(m+1+k),(r0.(m+ 1+k
))/ 2) by A35;
then Ball(x0.(m+1+(k+1)),r0.(m+1+(k+1))) c= Ball(x0.(m+1+k),r0.(m+1+k))
by A63;
hence PN[k+1] by A62,XBOOLE_1:1;
end;
A64: PN[0] by A35;
thus for k be Nat holds PN[k] from NAT_1:sch 2(A64,A61);
end;
A65: now
let m be Nat;
set m1 = m+1;
0 < r0.m by A35;
then 0 < (r0.m)/2 by XREAL_1:215;
then consider n1 be Nat such that
A66: for l be Nat st n1 <= l holds dist(x0.l,lim x0) < (r0
.m)/2 by A59,TBSP_1:def 3;
reconsider n = max(n1,m+1) as Nat by TARSKI:1;
A67: dist(x0.n,lim x0) < (r0.m)/2 by A66,XXREAL_0:25;
consider k be Nat such that
A68: n = m1 + k by NAT_1:10,XXREAL_0:25;
dist(x0.n,x0.n) = 0 & 0 < r0.n by A35,METRIC_1:1;
then
A69: x0.n in Ball(x0.n,r0.n) by METRIC_1:11;
reconsider k as Nat;
n = m1 + k by A68;
then Ball(x0.n,r0.n) c= Ball(x0.m,(r0.m)/2) by A60;
then dist(x0.n,x0.m) < (r0.m)/2 by A69,METRIC_1:11;
then
A70: dist(lim x0,x0.n) + dist(x0.n,x0.m) < (r0.m)/2 + (r0.m)/2 by A67,XREAL_1:8
;
dist(lim x0,x0.m) <= dist(lim x0,x0.n) +dist(x0.n,x0.m) by METRIC_1:4;
then dist(lim x0,x0.m) < (r0.m)/2 + (r0.m)/2 by A70,XXREAL_0:2;
hence lim x0 in Ball(x0.m,r0.m) by METRIC_1:11;
end;
A71: now
let n be Nat;
thus not lim x0 in Y.n
proof
assume
A72: lim x0 in Y.n;
lim x0 in Ball(x0.n,r0.n) by A65;
then lim x0 in Ball(x0.n,r0.n) /\ Y.n by A72,XBOOLE_0:def 4;
hence contradiction by A35;
end;
end;
not lim x0 in union rng Y
proof
assume lim x0 in union rng Y;
then consider A be set such that
A73: lim x0 in A and
A74: A in rng Y by TARSKI:def 4;
ex k be object st k in dom Y & A = Y.k by A74,FUNCT_1:def 3;
hence contradiction by A71,A73;
end;
hence contradiction by A2;
end;
begin :: Metric Space generated from Real Normed Space
reserve X for RealNormSpace;
definition
let X be RealNormSpace;
func distance_by_norm_of X -> Function of [:the carrier of X,the carrier of
X:],REAL means
:Def1:
for x, y be Point of X holds it.(x,y) = ||.x-y.||;
existence
proof
set CX = the carrier of X;
deffunc F(Element of CX,Element of CX) = In(||.$1-$2.||,REAL);
consider f be Function of [:CX,CX:],REAL such that
A1: for x being Element of CX for y
being Element of CX holds f.(x,y)=F(x,y) from BINOP_1:sch 4;
take f;
let x,y be Point of X;
f.(x,y)=F(x,y) by A1;
hence thesis;
end;
uniqueness
proof
let dist1,dist2 be Function of [:the carrier of X,the carrier of X:],REAL;
assume that
A2: for x,y be Point of X holds dist1.(x,y) = ||.x-y.|| and
A3: for x,y be Point of X holds dist2.(x,y) = ||.x-y.||;
now
let x,y be Point of X;
dist1.(x,y) = ||.x-y.|| by A2;
hence dist1.(x,y) = dist2.(x,y) by A3;
end;
hence thesis by BINOP_1:2;
end;
end;
Lm1: the distance of MetrStruct(# the carrier of X,distance_by_norm_of X #) is
Reflexive
proof
now
let a be Element of X;
thus (distance_by_norm_of X).(a,a) = ||.a-a.|| by Def1
.=0 by NORMSP_1:6;
end;
hence thesis;
end;
Lm2: the distance of MetrStruct(# the carrier of X,distance_by_norm_of X #) is
discerning
proof
now
let a,b be Element of X;
assume
A1: (distance_by_norm_of X).(a,b) = 0;
(distance_by_norm_of X).(a,b) = ||.a-b.|| by Def1;
hence a= b by A1,NORMSP_1:6;
end;
hence thesis;
end;
Lm3: the distance of MetrStruct(# the carrier of X,distance_by_norm_of X #) is
symmetric
proof
now
let a,b be Element of X;
thus (distance_by_norm_of X).(a,b) = ||.a-b.|| by Def1
.= ||.b-a.|| by NORMSP_1:7
.= (distance_by_norm_of X).(b,a) by Def1;
end;
hence thesis;
end;
Lm4: the distance of MetrStruct(# the carrier of X,distance_by_norm_of X #) is
triangle
proof
now
let a,b,c be Element of X;
A1: ||.a-c.|| <= ||.a-b.|| + ||.b-c.|| by NORMSP_1:10;
||.a-b.|| + ||.b-c.|| = ||.a-b.|| + (distance_by_norm_of X).(b,c) by Def1
.= (distance_by_norm_of X).(a,b) + (distance_by_norm_of X).(b,c) by Def1;
hence (distance_by_norm_of X).(a,c) <= (distance_by_norm_of X).(a,b) + (
distance_by_norm_of X).(b,c) by A1,Def1;
end;
hence thesis;
end;
definition
let X be RealNormSpace;
func MetricSpaceNorm X -> non empty MetrSpace equals
MetrStruct(# the
carrier of X,distance_by_norm_of X #);
coherence
by Lm1,Lm2,Lm3,Lm4,METRIC_1:def 6,METRIC_1:def 7,METRIC_1:def 8,METRIC_1:def 9;
end;
theorem Th2:
for X be RealNormSpace, z be Element of MetricSpaceNorm X, r be
Real holds ex x be Point of X st x = z & Ball(z,r) = {y where y is Point
of X:||.x-y.|| < r}
proof
let X be RealNormSpace, z be Element of MetricSpaceNorm X, r be Real;
set M = MetricSpaceNorm X;
reconsider x=z as Point of X;
A1: Ball(z,r) = {q where q is Element of M:dist(z,q) < r} by METRIC_1:def 14;
now
let a be object;
assume a in {y where y is Point of X: ||.x-y.|| < r};
then consider y be Point of X such that
A2: a=y & ||.x-y.|| < r;
reconsider t=y as Element of M;
||.x-y.|| = dist(z,t) by Def1;
hence a in {q where q is Element of M : dist(z,q) < r} by A2;
end;
then
A3: {y where y is Point of X: ||.x-y.|| < r} c= {q where q is Element of M
: dist(z,q) < r};
now
let a be object;
assume a in {q where q is Element of M:dist(z,q) < r};
then consider q be Element of M such that
A4: a=q & dist(z,q) < r;
reconsider t=q as Point of X;
||.x-t.|| = dist(z,q) by Def1;
hence a in {y where y is Point of X: ||.x-y.|| < r} by A4;
end;
then
{q where q is Element of M : dist(z,q) < r} c= {y where y is Point of
X: ||.x-y.|| < r};
then {q where q is Element of M:dist(z,q) < r} = {y where y is Point of X
:||.x -y.|| < r} by A3,XBOOLE_0:def 10;
hence thesis by A1;
end;
theorem Th3:
for X be RealNormSpace, z be Element of MetricSpaceNorm X, r be
Real holds ex x be Point of X st x = z & cl_Ball(z,r) = {y where y is
Point of X: ||.x-y.|| <= r}
proof
let X be RealNormSpace, z be Element of MetricSpaceNorm X, r be Real;
reconsider x=z as Point of X;
set M = MetricSpaceNorm X;
A1: cl_Ball(z,r) = {q where q is Element of M : dist(z,q) <= r} by
METRIC_1:def 15;
now
let a be object;
assume a in {y where y is Point of X: ||.x-y.|| <= r};
then consider y be Point of X such that
A2: a=y & ||.x-y.|| <= r;
reconsider t=y as Element of M;
||.x-y.|| = dist(z,t) by Def1;
hence a in {q where q is Element of M : dist(z,q) <= r} by A2;
end;
then
A3: {y where y is Point of X: ||.x-y.|| <= r}
c= {q where q is Element of M: dist(z,q) <= r};
now
let a be object;
assume a in {q where q is Element of M : dist(z,q) <= r};
then consider q be Element of M such that
A4: a=q & dist(z,q) <= r;
reconsider t=q as Point of X;
||.x-t.|| = dist(z,q) by Def1;
hence a in {y where y is Point of X: ||.x-y.|| <= r} by A4;
end;
then
{q where q is Element of M : dist(z,q) <= r} c= {y where y is Point of
X: ||.x-y.|| <= r};
then
{q where q is Element of M : dist(z,q) <= r} = {y where y is Point of
X: ||.x-y.|| <= r} by A3,XBOOLE_0:def 10;
hence thesis by A1;
end;
theorem Th4:
for X be RealNormSpace, S be sequence of X, St be sequence of
MetricSpaceNorm X, x be Point of X, xt be Point of MetricSpaceNorm X st S = St
& x = xt holds St is_convergent_in_metrspace_to xt iff
for r be Real st 0 < r
ex m be Nat st for n be Nat st m <= n holds ||. S.n - x
.|| < r
proof
let X be RealNormSpace, S be sequence of X, St be sequence of
MetricSpaceNorm X, x be Point of X, xt be Point of MetricSpaceNorm X;
assume
A1: S=St & x=xt;
A2: now
assume
A3: for r be Real st 0 < r ex m be Nat st
for n be Nat st m <= n holds ||. S.n - x.|| < r;
now
let r be Real;
assume r>0;
then consider m be Nat such that
A4: for n be Nat st m <= n holds ||. S.n - x.|| < r by A3;
take m;
let n be Nat;
assume m <= n;
then ||. S.n - x.|| < r by A4;
hence dist(St.n,xt) < r by A1,Def1;
end;
hence St is_convergent_in_metrspace_to xt by METRIC_6:def 2;
end;
now
assume
A5: St is_convergent_in_metrspace_to xt;
let r be Real;
assume 0 < r;
then consider m be Nat such that
A6: for n being Nat st m <= n holds dist(St.n,xt) < r by A5,
METRIC_6:def 2;
take m;
let n be Nat;
assume m <= n;
then dist(St.n,xt) < r by A6;
hence ||. S.n - x.|| < r by A1,Def1;
end;
hence thesis by A2;
end;
theorem Th5:
for X be RealNormSpace, S be sequence of X, St be sequence of
MetricSpaceNorm X st S = St holds St is convergent iff S is convergent
proof
let X be RealNormSpace, S be sequence of X, St be sequence of
MetricSpaceNorm X;
assume
A1: S=St;
A2: now
assume S is convergent;
then consider x be Point of X such that
A3: for r be Real st 0 < r ex m be Nat st
for n be Nat st m <= n holds ||. S.n - x.|| < r by NORMSP_1:def 6;
reconsider xt=x as Point of MetricSpaceNorm X;
St is_convergent_in_metrspace_to xt by A1,A3,Th4;
hence St is convergent by METRIC_6:9;
end;
now
assume St is convergent;
then consider xt be Point of MetricSpaceNorm X such that
A4: St is_convergent_in_metrspace_to xt by METRIC_6:10;
reconsider x=xt as Point of X;
for r be Real st 0 < r ex m be Nat st
for n be Nat st m <= n holds ||. S.n - x.|| < r by A1,A4,Th4;
hence S is convergent by NORMSP_1:def 6;
end;
hence thesis by A2;
end;
theorem Th6:
for X be RealNormSpace, S be sequence of X, St be sequence of
MetricSpaceNorm X st S = St & St is convergent holds lim St = lim S
proof
let X be RealNormSpace, S be sequence of X, St be sequence of
MetricSpaceNorm X;
assume that
A1: S=St and
A2: St is convergent;
reconsider xt=lim S as Point of MetricSpaceNorm X;
S is convergent by A1,A2,Th5;
then
for r be Real st 0 < r
ex m be Nat st for n be Nat
st m <= n holds ||. S.n - lim S.|| < r by NORMSP_1:def 7;
then St is_convergent_in_metrspace_to xt by A1,Th4;
hence thesis by METRIC_6:11;
end;
begin :: Topological Space generated from Real Normed Space
definition
let X be RealNormSpace;
func TopSpaceNorm X -> non empty TopSpace equals
TopSpaceMetr
MetricSpaceNorm X;
coherence;
end;
theorem Th7:
for X be RealNormSpace, V be Subset of TopSpaceNorm X holds V is
open iff for x be Point of X st x in V
ex r be Real st r>0 & {y where y
is Point of X: ||.x-y.|| < r} c= V
proof
let X be RealNormSpace, V be Subset of TopSpaceNorm X;
A1: now
assume
A2: for x be Point of X st x in V holds
ex r be Real st r>0 & {y where
y is Point of X: ||.x-y.|| < r} c= V;
now
let z be Element of MetricSpaceNorm X;
reconsider x = z as Point of X;
assume z in V;
then consider r be Real such that
A3: r > 0 & {y where y is Point of X: ||.x-y.|| < r} c= V by A2;
take r;
ex t be Point of X st t = z & Ball(z,r) = {y where y is Point of X:
||.t-y.|| < r} by Th2;
hence r > 0 & Ball(z,r) c= V by A3;
end;
hence V in the topology of TopSpaceNorm X by PCOMPS_1:def 4;
hence V is open;
end;
now
assume
A4: V is open;
hereby
let x be Point of X such that
A5: x in V;
reconsider z=x as Element of MetricSpaceNorm X;
V in the topology of TopSpaceNorm X by A4;
then consider r be Real such that
A6: r > 0 & Ball(z,r) c= V by A5,PCOMPS_1:def 4;
take r;
ex t be Point of X st t = z & Ball(z,r) = {y where y is Point of X:
||.t-y.|| < r} by Th2;
hence r > 0 & {y where y is Point of X: ||.x-y.|| < r} c= V by A6;
end;
end;
hence thesis by A1;
end;
theorem Th8:
for X be RealNormSpace, x be Point of X,
r be Real holds {y where
y is Point of X:||.x-y.|| < r} is open Subset of TopSpaceNorm X
proof
let X be RealNormSpace, x be Point of X, r be Real;
reconsider z=x as Element of MetricSpaceNorm X;
( ex t be Point of X st t=x & Ball(z,r) = {y where y is Point of X: ||.t
-y.|| < r})& Ball(z,r) in Family_open_set(MetricSpaceNorm X) by Th2,PCOMPS_1:29
;
hence thesis by PRE_TOPC:def 2;
end;
theorem
for X be RealNormSpace, x be Point of X, r be Real
holds {y where y is
Point of X: ||.x-y.|| <= r} is closed Subset of TopSpaceNorm X
proof
let X be RealNormSpace, x be Point of X, r be Real;
reconsider z=x as Element of MetricSpaceNorm X;
ex t be Point of X st t = x & cl_Ball(z,r) = {y where y is Point of X:
||.t-y.|| <= r} by Th3;
hence thesis by TOPREAL6:57;
end;
::$N Baire Category Theorem (Hausdorff spaces)
::$L https://en.wikipedia.org/wiki/Baire_category_theorem Baire Category Theorem (Hausdorff spaces)
theorem
for X be Hausdorff non empty TopSpace st X is locally-compact
holds X is Baire
proof
let X be Hausdorff non empty TopSpace;
assume X is locally-compact;
then X is sober locally-compact by YELLOW_8:22;
hence thesis by WAYBEL12:44;
end;
theorem
for X be RealNormSpace holds TopSpaceNorm(X) is sequential;
registration
let X be RealNormSpace;
cluster TopSpaceNorm(X) -> sequential;
coherence;
end;
theorem Th12:
for X be RealNormSpace, S be sequence of X, St be sequence of
TopSpaceNorm X, x be Point of X, xt be Point of TopSpaceNorm X st S = St & x =
xt holds St is_convergent_to xt iff
for r be Real st 0 < r ex m be Nat
st for n be Nat st m <= n holds ||. S.n - x.|| < r
proof
let X be RealNormSpace, S be sequence of X, St be sequence of TopSpaceNorm X
, x be Point of X, xt be Point of TopSpaceNorm X;
assume that
A1: S=St and
A2: x=xt;
reconsider Sm=St as sequence of MetricSpaceNorm X;
reconsider xm=x as Point of MetricSpaceNorm X;
St is_convergent_to xt iff Sm is_convergent_in_metrspace_to xm by A2,
FRECHET2:28;
hence thesis by A1,Th4;
end;
theorem Th13:
for X be RealNormSpace, S be sequence of X, St be sequence of
TopSpaceNorm X st S = St holds St is convergent iff S is convergent
proof
let X be RealNormSpace, S be sequence of X, St be sequence of TopSpaceNorm X;
reconsider Sm=St as sequence of MetricSpaceNorm X;
A1: St is convergent iff Sm is convergent by FRECHET2:29;
assume S = St;
hence thesis by A1,Th5;
end;
theorem Th14:
for X be RealNormSpace, S be sequence of X, St be sequence of
TopSpaceNorm X st S = St & St is convergent holds Lim St = {lim S} & lim St=lim
S
proof
let X be RealNormSpace, S be sequence of X, St be sequence of TopSpaceNorm X;
assume that
A1: S = St and
A2: St is convergent;
consider x being Point of TopSpaceNorm X such that
A3: Lim St = {x} by A2,FRECHET2:24;
reconsider Sm=St as sequence of MetricSpaceNorm X;
A4: Sm is convergent by A2,FRECHET2:29;
then
A5: lim St=lim Sm by FRECHET2:30
.=lim S by A1,A4,Th6;
x in Lim St by A3,TARSKI:def 1;
then St is_convergent_to x by FRECHET:def 5;
hence Lim St = {lim S} by A5,A3,FRECHET2:25;
thus thesis by A5;
end;
theorem Th15:
for X be RealNormSpace, V be Subset of X, Vt be Subset of
TopSpaceNorm X st V = Vt holds V is closed iff Vt is closed
proof
let X be RealNormSpace, V be Subset of X, Vt be Subset of TopSpaceNorm X;
assume
A1: V = Vt;
hereby
assume
A2: V is closed;
now
let St be sequence of TopSpaceNorm X;
assume that
A3: St is convergent and
A4: rng St c= Vt;
reconsider S = St as sequence of X;
S is convergent by A3,Th13;
then lim S in V by A1,A2,A4,NFCONT_1:def 3;
then {lim S} c= V by ZFMISC_1:31;
hence Lim St c= Vt by A1,A3,Th14;
end;
hence Vt is closed by FRECHET:def 7;
end;
assume
A5: Vt is closed;
now
let S be sequence of X;
assume that
A6: rng S c= V and
A7: S is convergent;
reconsider St = S as sequence of TopSpaceNorm X;
A8: St is convergent by A7,Th13;
then Lim St c= Vt by A1,A5,A6,FRECHET:def 7;
then {lim S} c= V by A1,A8,Th14;
hence lim S in V by ZFMISC_1:31;
end;
hence thesis by NFCONT_1:def 3;
end;
theorem Th16:
for X be RealNormSpace, V be Subset of X, Vt be Subset of
TopSpaceNorm X st V = Vt holds V is open iff Vt is open
proof
let X be RealNormSpace, V be Subset of X, Vt be Subset of TopSpaceNorm X;
A1: V is open iff V` is closed by NFCONT_1:def 4;
assume V = Vt;
then V is open iff Vt` is closed by A1,Th15;
hence thesis by TOPS_1:4;
end;
Lm5: for X be RealNormSpace, r be Real,
x be Point of X holds {y where y is
Point of X: ||.x-y.|| < r} = {y where y is Point of X: ||.y-x.|| < r}
proof
let X be RealNormSpace, r be Real, x be Point of X;
now
let s be object;
assume s in {y where y is Point of X: ||.y-x.|| < r};
then consider z be Point of X such that
A1: s = z and
A2: ||.z-x.|| < r;
||.x-z.|| < r by A2,NORMSP_1:7;
hence s in {y where y is Point of X: ||.x-y.|| < r} by A1;
end;
then
A3: {y where y is Point of X: ||.y-x.|| < r} c= {y where y is Point of X:
||.x-y.|| < r};
now
let s be object;
assume s in {y where y is Point of X: ||.x-y.|| < r};
then consider z be Point of X such that
A4: s = z and
A5: ||.x-z.|| < r;
||.z-x.|| < r by A5,NORMSP_1:7;
hence s in {y where y is Point of X: ||.y-x.|| < r} by A4;
end;
then {y where y is Point of X: ||.x-y.|| < r} c= {y where y is Point of X:
||.y-x.|| < r};
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th17:
for X be RealNormSpace, U be Subset of X, Ut be Subset of
TopSpaceNorm X, x be Point of X, xt be Point of TopSpaceNorm X st U = Ut & x =
xt holds U is Neighbourhood of x iff Ut is a_neighborhood of xt
proof
let X be RealNormSpace, U be Subset of X, Ut be Subset of TopSpaceNorm X, x
be Point of X, xt be Point of TopSpaceNorm X;
assume that
A1: U=Ut and
A2: x=xt;
A3: now
assume U is Neighbourhood of x;
then consider r be Real such that
A4: r > 0 and
A5: {y where y is Point of X: ||.y-x.|| < r} c= U by NFCONT_1:def 1;
now
let s be object;
assume s in {y where y is Point of X: ||.y-x.|| < r};
then ex z be Point of X st s = z & ||.z-x.|| < r;
hence s in the carrier of X;
end;
then reconsider Vt={y where y is Point of X: ||.y-x.|| < r} as Subset of
TopSpaceNorm X by TARSKI:def 3;
Vt={y where y is Point of X: ||.x-y.|| < r} by Lm5;
then
A6: Vt is open by Th8;
||.x-x.|| =0 by NORMSP_1:6;
then xt in Vt by A2,A4;
hence Ut is a_neighborhood of xt by A1,A5,A6,CONNSP_2:6;
end;
now
assume Ut is a_neighborhood of xt;
then consider Vt being Subset of TopSpaceNorm X such that
A7: Vt is open and
A8: Vt c= Ut and
A9: xt in Vt by CONNSP_2:6;
consider r be Real such that
A10: r > 0 and
A11: {y where y is Point of X: ||.x-y.|| < r} c= Vt by A2,A7,A9,Th7;
A12: {y where y is Point of X: ||.x-y.|| < r} = {y where y is Point of X:
||.y-x.|| < r} by Lm5;
{y where y is Point of X: ||.x-y.|| < r} c=U by A1,A8,A11;
hence U is Neighbourhood of x by A10,A12,NFCONT_1:def 1;
end;
hence thesis by A3;
end;
theorem Th18:
for X,Y be RealNormSpace, f be PartFunc of X,Y, ft be Function
of TopSpaceNorm X,TopSpaceNorm Y, x be Point of X, xt be Point of TopSpaceNorm
X st f = ft & x = xt holds f is_continuous_in x iff ft is_continuous_at xt
proof
let X,Y be RealNormSpace, f be PartFunc of X,Y, ft be Function of
TopSpaceNorm X,TopSpaceNorm Y, x be Point of X, xt be Point of TopSpaceNorm X;
assume that
A1: f = ft and
A2: x = xt;
A3: dom f = the carrier of X by A1,FUNCT_2:def 1;
then
A4: ft.xt = f/.x by A1,A2,PARTFUN1:def 6;
hereby
assume
A5: f is_continuous_in x;
now
let G be a_neighborhood of ft.xt;
reconsider N1 = G as Subset of Y;
N1 is Neighbourhood of f/.x by A4,Th17;
then consider N being Neighbourhood of x such that
A6: f.:N c= N1 by A5,NFCONT_1:10;
reconsider H=N as a_neighborhood of xt by A2,Th17;
take H;
thus ft.:H c= G by A1,A6;
end;
hence ft is_continuous_at xt by TMAP_1:def 2;
end;
assume
A7: ft is_continuous_at xt;
now
let N1 be Neighbourhood of f/.x;
reconsider G=N1 as Subset of Y;
G is a_neighborhood of ft.xt by A4,Th17;
then consider H being a_neighborhood of xt such that
A8: ft.:H c= G by A7,TMAP_1:def 2;
reconsider N=H as Subset of X;
reconsider N as Neighbourhood of x by A2,Th17;
take N;
thus f.:N c= N1 by A1,A8;
end;
hence thesis by A3,NFCONT_1:10;
end;
theorem
for X,Y be RealNormSpace, f be PartFunc of X,Y, ft be Function of
TopSpaceNorm X,TopSpaceNorm Y st f = ft holds f is_continuous_on the carrier of
X iff ft is continuous
proof
let X,Y be RealNormSpace, f be PartFunc of X,Y, ft be Function of
TopSpaceNorm X,TopSpaceNorm Y;
assume
A1: f=ft;
A2: f|(the carrier of X)=f by RELSET_1:19;
hereby
assume
A3: f is_continuous_on the carrier of X;
now
let xt be Point of TopSpaceNorm X;
reconsider x=xt as Point of X;
f|(the carrier of X) is_continuous_in x by A3,NFCONT_1:def 7;
hence ft is_continuous_at xt by A1,A2,Th18;
end;
hence ft is continuous by TMAP_1:44;
end;
assume
A4: ft is continuous;
A5: now
let x be Point of X;
assume x in the carrier of X;
reconsider xt=x as Point of TopSpaceNorm X;
ft is_continuous_at xt by A4,TMAP_1:44;
hence f|(the carrier of X) is_continuous_in x by A1,A2,Th18;
end;
dom f =the carrier of X by A1,FUNCT_2:def 1;
hence thesis by A5,NFCONT_1:def 7;
end;
begin :: Linear Topological Space generated from Real Normed Space
definition
let X be RealNormSpace;
func LinearTopSpaceNorm X -> strict non empty RLTopStruct means
:Def4:
the
carrier of it = the carrier of X & 0.it = 0.X & the addF of it = the addF of X
& the Mult of it = the Mult of X & the topology of it = the topology of
TopSpaceNorm X;
existence
proof
reconsider TP = the topology of TopSpaceNorm X as Subset-Family of X;
take RLTopStruct(# the carrier of X,0.X, the addF of X,the Mult of X,TP #);
thus thesis;
end;
uniqueness;
end;
registration
let X be RealNormSpace;
cluster LinearTopSpaceNorm X -> add-continuous Mult-continuous TopSpace-like
Abelian add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital;
correctness
proof
thus LinearTopSpaceNorm X is add-continuous
proof
let x1,x2 be Point of LinearTopSpaceNorm X;
reconsider z2=x2 as Element of MetricSpaceNorm X by Def4;
reconsider z1=x1 as Element of MetricSpaceNorm X by Def4;
reconsider z12=x1+x2 as Element of MetricSpaceNorm X by Def4;
let V be Subset of LinearTopSpaceNorm X;
assume that
A1: V is open and
A2: x1+x2 in V;
V in the topology of LinearTopSpaceNorm X by A1;
then V in the topology of TopSpaceNorm X by Def4;
then consider r be Real such that
A3: r>0 and
A4: Ball(z12,r) c= V by A2,PCOMPS_1:def 4;
set r2=r/2;
A5: 0 < r2 by A3,XREAL_1:215;
reconsider V1= Ball(z1,r/2), V2= Ball(z2,r/2) as Subset of
LinearTopSpaceNorm X by Def4;
A6: V1+V2 c= V
proof
let w be object;
assume w in V1+V2;
then consider v,u be VECTOR of LinearTopSpaceNorm X such that
A7: w=v+u and
A8: v in V1 & u in V2;
reconsider v1=v, u1=u as Element of MetricSpaceNorm X by Def4;
reconsider w1=w as Element of MetricSpaceNorm X by A7,Def4;
reconsider zz12=x1+x2, zz1=x1, zz2=x2, vv1=v, uu1=u as Point of X by
Def4;
A9: ||.(zz1-vv1)+(zz2-uu1).|| <= ||.zz1-vv1.|| + ||.zz2-uu1.|| & ||.
zz1-vv1.|| = dist(z1,v1) by Def1,NORMSP_1:def 1;
dist(z1,v1) < r/2 & dist(z2,u1) < r/2 by A8,METRIC_1:11;
then
A10: dist(z1,v1) + dist(z2,u1) < r/2 + r/2 by XREAL_1:8;
reconsider ww1=w as Point of X by A7,Def4;
A11: ||.zz2-uu1.|| = dist(z2,u1) by Def1;
dist(z12,w1) = ||.zz12-ww1.|| by Def1
.= ||.(zz1+zz2)-ww1.|| by Def4
.= ||.(zz1+zz2)-(vv1+uu1).|| by A7,Def4
.= ||.(zz1+zz2)+(-uu1+-vv1).|| by RLVECT_1:31
.= ||.(zz1+zz2+-vv1)+ -uu1.|| by RLVECT_1:def 3
.= ||.(zz1+-vv1+zz2)+ -uu1.|| by RLVECT_1:def 3
.= ||.(zz1+-vv1)+(zz2+ -uu1).|| by RLVECT_1:def 3;
then dist(z12,w1) < r by A9,A11,A10,XXREAL_0:2;
then w1 in Ball(z12,r) by METRIC_1:11;
hence thesis by A4;
end;
dist(z2,z2) = 0 by METRIC_1:1;
then
A12: x2 in V2 by A5,METRIC_1:11;
Ball(z2,r/2) in the topology of TopSpaceNorm X by PCOMPS_1:29;
then Ball(z2,r/2) in the topology of LinearTopSpaceNorm X by Def4;
then
A13: V2 is open;
Ball(z1,r/2) in the topology of TopSpaceNorm X by PCOMPS_1:29;
then Ball(z1,r/2) in the topology of LinearTopSpaceNorm X by Def4;
then
A14: V1 is open;
dist(z1,z1) = 0 by METRIC_1:1;
then x1 in V1 by A5,METRIC_1:11;
hence thesis by A14,A13,A12,A6;
end;
A15: now
let a,b be Real;
let v be VECTOR of LinearTopSpaceNorm X;
reconsider v1=v as VECTOR of X by Def4;
a * v=a*v1 & b * v=b*v1 by Def4;
then
A16: a * v1 + b * v1 = a*v +b*v by Def4;
(a+b) * v =(a+b) * v1 by Def4;
hence (a+b) * v = a*v +b*v by A16,RLVECT_1:def 6;
end;
thus LinearTopSpaceNorm X is Mult-continuous
proof
let a be Real, x be Point of LinearTopSpaceNorm X, V be Subset of
LinearTopSpaceNorm X such that
A17: V is open and
A18: a*x in V;
reconsider z=x, az=a*x as Element of MetricSpaceNorm X by Def4;
V in the topology of LinearTopSpaceNorm X by A17;
then V in the topology of TopSpaceNorm X by Def4;
then consider r0 be Real such that
A19: r0>0 and
A20: Ball(az,r0) c= V by A18,PCOMPS_1:def 4;
set r=r0/2;
r > 0 by A19,XREAL_1:215;
then
A21: 0 < r/2 by XREAL_1:215;
reconsider z1=z as Point of X;
set r2 = min((r/2)/(1+||.z1.||+|.a.|),1);
reconsider W= Ball(z,r2) as Subset of LinearTopSpaceNorm X by Def4;
A22: r0/2 < r0/1 by A19,XREAL_1:76;
A23: for s being Real st |.s-a.| < r2 holds s*W c= V
proof
let s be Real;
assume |.s-a.| < r2;
then
A24: |.a-s.| <= r2 by COMPLEX1:60;
thus s*W c= V
proof
let w be object;
assume w in s*W;
then consider v be VECTOR of LinearTopSpaceNorm X such that
A25: w=s*v and
A26: v in W;
reconsider v1=v as Element of MetricSpaceNorm X by Def4;
A27: dist(z,v1) < r2 by A26,METRIC_1:11;
reconsider w1=w as Element of MetricSpaceNorm X by A25,Def4;
reconsider zza=a*x, zz=x, vv1=v as Point of X by Def4;
A28: ||.zz-vv1.|| = dist(z,v1) by Def1;
r2 <= 1 by XXREAL_0:17;
then ||. zz-vv1 .|| <= 1 by A28,A27,XXREAL_0:2;
then ||.vv1-zz .|| <= 1 by NORMSP_1:7;
then
A29: ||.zz.|| + ||.vv1-zz .|| <= ||.zz.|| + 1 by XREAL_1:6;
zz+(vv1-zz) = vv1-(zz-zz) by RLVECT_1:29
.=vv1-0.X by RLVECT_1:15
.=vv1 by RLVECT_1:13;
then ||. vv1 .|| <= ||.zz.|| + ||.vv1-zz .|| by NORMSP_1:def 1;
then
A30: ||.vv1.|| <= ||.zz.|| +1 by A29,XXREAL_0:2;
A31: 0 <= 1+||.z1.|| by NORMSP_1:4,XREAL_1:39;
then
A32: r2*(||.zz.|| +1) <= (r/2/(1+||.z1.||+|.a.|))*(||.zz.||+1) by
XREAL_1:64,XXREAL_0:17;
0 <= |.a-s.| & 0 <= ||.vv1.|| by COMPLEX1:46,NORMSP_1:4;
then |.a-s.| * ||.vv1.|| <= r2 * (||.zz.|| + 1) by A24,A30,
XREAL_1:66;
then |.a-s.|*||.vv1.|| <= r/2/(1+||.z1.||+|.a.|)*(||.z1.||+1) by A32
,XXREAL_0:2;
then
A33: |.a-s.|*||.vv1.|| <= (||.z1.||+1)/(1+||.z1.||+|.a.|)* (r/2) by
XCMPLX_1:75;
0 <= |.a.| by COMPLEX1:46;
then 0 + (1+||.z1.||) <= |.a.| + (1+||.z1.||) by XREAL_1:6;
then (||.z1.||+1)/(1+||.z1.||+|.a.|) <= 1 by A31,XREAL_1:183;
then (||.z1.||+1)/(1+||.z1.||+|.a.|)*(r/2) <=1*(r/2) by A19,
XREAL_1:64;
then
A34: |.a-s.| * ||.vv1.|| <= r/2 by A33,XXREAL_0:2;
reconsider ww1=w as Point of X by A25,Def4;
a*(zz-vv1)-(s-a)*vv1 = a*zz-a*vv1-(s-a)*vv1 by RLVECT_1:34
.= a*zz-a*vv1-(s*vv1-a*vv1) by RLVECT_1:35
.= a*zz-(s*vv1-a*vv1 + a*vv1) by RLVECT_1:27
.= a*zz-(s*vv1-(a*vv1 - a*vv1)) by RLVECT_1:29
.= a*zz-(s*vv1-0.X) by RLVECT_1:15
.= a*zz-s*vv1 by RLVECT_1:13;
then ||.a*zz-s*vv1.|| <= ||.a*(zz-vv1).|| + ||.(s-a)*vv1.|| by
NORMSP_1:3;
then ||.a*zz-s*vv1.|| <= |.a.| * ||.zz-vv1.|| + ||.(s-a)*vv1.|| by
NORMSP_1:def 1;
then ||.a*zz-s*vv1.|| <= |.a.| * ||.zz-vv1.|| + |.s-a.|*||.vv1.||
by NORMSP_1:def 1;
then
A35: ||.a*zz-s*vv1.|| <= |.a.| * ||.zz-vv1.|| + |.a-s.|* ||.vv1.||
by COMPLEX1:60;
A36: 0 <= |.a.| by COMPLEX1:46;
then
A37: r2*|.a.| <= r/2/(1+||.z1.||+|.a.|)*|.a.| by XREAL_1:64,XXREAL_0:17;
0 <= 1+||.z1.|| by NORMSP_1:4,XREAL_1:39;
then 0 + |.a.| <=1+||.z1.||+|.a.| by XREAL_1:6;
then |.a.|/(1+||.z1.||+|.a.|) <= 1 by A36,XREAL_1:183;
then
A38: |.a.|/(1+||.z1.||+|.a.|)*(r/2) <= 1*(r/2) by A19,XREAL_1:64;
||.zz-vv1.||*|.a.| <= r2*|.a.| by A28,A27,A36,XREAL_1:64;
then |.a.| * ||.zz-vv1.|| <= |.a.|*(r/2/(1+||.z1.||+|.a.|)) by A37,
XXREAL_0:2;
then |.a.|* ||.zz-vv1.|| <= |.a.|/(1+||.z1.||+|.a.|)*(r/2) by
XCMPLX_1:75;
then |.a.| * ||.zz-vv1.|| <= r/2 by A38,XXREAL_0:2;
then
A39: |.a.| * ||.zz-vv1.|| + |.a-s.| * ||.vv1.||<= r/2 + r/2 by A34,
XREAL_1:7;
dist(az,w1) = ||.zza-ww1.|| by Def1
.= ||.(a*zz)-ww1.|| by Def4
.= ||.(a*zz)-(s*vv1).|| by A25,Def4;
then dist(az,w1) <= r by A35,A39,XXREAL_0:2;
then dist(az,w1) < r0 by A22,XXREAL_0:2;
then w1 in Ball(az,r0) by METRIC_1:11;
hence thesis by A20;
end;
end;
0 <= ||.z1.|| & 0 <= |.a.| by COMPLEX1:46,NORMSP_1:4;
then 0/(1+||.z1.||+|.a.|) < (r/2)/(1+||.z1.||+|.a.|) by A21,XREAL_1:74;
then
A40: 0 < r2 by XXREAL_0:15;
Ball(z,r2) in the topology of TopSpaceNorm X by PCOMPS_1:29;
then Ball(z,r2) in the topology of LinearTopSpaceNorm X by Def4;
then
A41: W is open;
dist(z,z) = 0 by METRIC_1:1;
then x in W by A40,METRIC_1:11;
hence thesis by A41,A40,A23;
end;
thus LinearTopSpaceNorm X is TopSpace-like
proof
set LTSN=LinearTopSpaceNorm X;
A42: the topology of LTSN = the topology of TopSpaceNorm X by Def4;
then
A43: for a,b being Subset of LTSN st a in the topology of LTSN & b in
the topology of LTSN holds a /\ b in the topology of LTSN by PRE_TOPC:def 1;
the carrier of LTSN = the carrier of TopSpaceNorm X by Def4;
then the carrier of LTSN in the topology of LTSN & for a being
Subset-Family of LTSN st a c= the topology of LTSN holds union a in the
topology of LTSN by A42,PRE_TOPC:def 1;
hence thesis by A43;
end;
thus LinearTopSpaceNorm X is Abelian
proof
let v,w be VECTOR of LinearTopSpaceNorm X;
reconsider v1=v,w1=w as VECTOR of X by Def4;
thus v+w = v1+w1 by Def4
.=w1+v1
.= w+v by Def4;
end;
thus LinearTopSpaceNorm X is add-associative
proof
let v,w,x be VECTOR of LinearTopSpaceNorm X;
reconsider v1=v,w1=w,x1=x as VECTOR of X by Def4;
A44: w+x = w1+x1 by Def4;
v+w = v1+w1 by Def4;
hence v+w+x = v1+w1+x1 by Def4
.=v1+(w1+x1) by RLVECT_1:def 3
.=v+(w+x) by A44,Def4;
end;
thus LinearTopSpaceNorm X is right_zeroed
proof
let v be VECTOR of LinearTopSpaceNorm X;
reconsider v1=v as VECTOR of X by Def4;
0.LinearTopSpaceNorm X =0.X by Def4;
hence v + 0.LinearTopSpaceNorm X = v1 + 0.X by Def4
.=v by RLVECT_1:def 4;
end;
thus LinearTopSpaceNorm X is right_complementable
proof
let v be VECTOR of LinearTopSpaceNorm X;
reconsider v1=v as VECTOR of X by Def4;
reconsider w=-v1 as VECTOR of LinearTopSpaceNorm X by Def4;
take w;
thus v+w =v1-v1 by Def4
.= 0.X by RLVECT_1:15
.=0.LinearTopSpaceNorm X by Def4;
end;
A45: now
let a,b be Real;
let v be VECTOR of LinearTopSpaceNorm X;
reconsider v1=v as VECTOR of X by Def4;
b * v=b*v1 by Def4;
then a * (b * v1) = a*(b*v) by Def4;
then a*b * v1 = a*(b*v) by RLVECT_1:def 7;
hence a*b * v = a*(b*v) by Def4;
end;
A46: now
let a be Real;
let v,w be VECTOR of LinearTopSpaceNorm X;
reconsider v1=v,w1=w as VECTOR of X by Def4;
a * v=a*v1 & a * w=a*w1 by Def4;
then
A47: a * v1 + a * w1 = a*v +a*w by Def4;
v+w =v1+w1 by Def4;
then a * (v + w) =a * (v1 + w1) by Def4;
hence a * (v + w) = a*v +a*w by A47,RLVECT_1:def 5;
end;
now
let v be VECTOR of LinearTopSpaceNorm X;
reconsider v1=v as VECTOR of X by Def4;
thus 1 * v =1 * v1 by Def4
.= v by RLVECT_1:def 8;
end;
hence LinearTopSpaceNorm X is vector-distributive scalar-distributive
scalar-associative scalar-unital by A46,A15,A45;
end;
end;
theorem Th20:
for X be RealNormSpace, V be Subset of TopSpaceNorm X, Vt be
Subset of LinearTopSpaceNorm X st V=Vt holds V is open iff Vt is open
by Def4;
theorem Th21:
for X be RealNormSpace, V be Subset of TopSpaceNorm X, Vt be
Subset of LinearTopSpaceNorm X st V=Vt holds V is closed iff Vt is closed
proof
let X be RealNormSpace, V be Subset of TopSpaceNorm X, Vt be Subset of
LinearTopSpaceNorm X;
assume V=Vt;
then
A1: Vt` =V` by Def4;
Vt is closed iff V` is open by A1,Th20;
hence thesis;
end;
theorem
for X be RealNormSpace, V be Subset of LinearTopSpaceNorm X holds V is
open iff for x be Point of X st x in V
ex r be Real st r>0 & {y where y
is Point of X:||.x-y.|| < r} c= V
proof
let X be RealNormSpace, V be Subset of LinearTopSpaceNorm X;
reconsider V0 = V as Subset of TopSpaceNorm X by Def4;
V is open iff V0 is open by Th20;
hence thesis by Th7;
end;
theorem
for X be RealNormSpace, x be Point of X, r be Real, V be Subset of
LinearTopSpaceNorm X st V = {y where y is Point of X:||.x-y.|| < r} holds V is
open
proof
let X be RealNormSpace, x be Point of X, r be Real, V be Subset of
LinearTopSpaceNorm X;
reconsider V0 = V as Subset of TopSpaceNorm X by Def4;
assume V = {y where y is Point of X:||.x-y.|| < r};
then V0 is open by Th8;
hence thesis by Th20;
end;
theorem
for X be RealNormSpace, x be Point of X, r be Real, V be Subset of
TopSpaceNorm X st V = {y where y is Point of X:||.x-y.|| <= r} holds V is
closed
proof
let X be RealNormSpace, x be Point of X, r be Real, V be Subset of
TopSpaceNorm X;
assume
A1: V = {y where y is Point of X:||.x-y.|| <= r};
reconsider z=x as Element of MetricSpaceNorm X;
ex t be Point of X st t=x & cl_Ball(z,r) = {y where y is Point of X: ||.
t-y.|| <= r} by Th3;
hence thesis by A1,TOPREAL6:57;
end;
registration
let X be RealNormSpace;
cluster LinearTopSpaceNorm X -> T_2;
coherence
proof
let p,q be Point of LinearTopSpaceNorm X;
A1: the topology of LinearTopSpaceNorm X = the topology of TopSpaceNorm X
by Def4;
reconsider p1=p, q1=q as Point of TopSpaceNorm X by Def4;
assume p <> q;
then consider W1,V1 being Subset of TopSpaceNorm X such that
A2: W1 is open and
A3: V1 is open and
A4: p1 in W1 & q1 in V1 & W1 misses V1 by PRE_TOPC:def 10;
reconsider W=W1, V=V1 as Subset of LinearTopSpaceNorm X by Def4;
V1 in the topology of TopSpaceNorm X by A3;
then
A5: V is open by A1;
W1 in the topology of TopSpaceNorm X by A2;
then W is open by A1;
hence thesis by A4,A5;
end;
cluster LinearTopSpaceNorm X -> sober;
coherence by YELLOW_8:22;
end;
theorem Th25:
for X be RealNormSpace, S be Subset-Family of TopSpaceNorm X, St
be Subset-Family of LinearTopSpaceNorm X, x be Point of TopSpaceNorm X, xt be
Point of LinearTopSpaceNorm X st S=St & x=xt holds St is Basis of xt iff S is
Basis of x
proof
let X be RealNormSpace, S be Subset-Family of TopSpaceNorm X, St be
Subset-Family of LinearTopSpaceNorm X, x be Point of TopSpaceNorm X, xt be
Point of LinearTopSpaceNorm X;
assume that
A1: S=St and
A2: x=xt;
A3: Intersect S = Intersect St by A1,Def4;
hereby
assume
A4: St is Basis of xt;
then St c= the topology of LinearTopSpaceNorm X by TOPS_2:64;
then
A5: S c= the topology of TopSpaceNorm X by A1,Def4;
A6: now
let U be Subset of TopSpaceNorm X such that
A7: U is open and
A8: x in U;
reconsider Ut=U as open Subset of LinearTopSpaceNorm X by A7,Def4,Th20;
consider Vt being Subset of LinearTopSpaceNorm X such that
A9: Vt in St & Vt c= Ut by A2,A4,A8,YELLOW_8:def 1;
reconsider V=Vt as Subset of TopSpaceNorm X by Def4;
take V;
thus V in S & V c= U by A1,A9;
end;
x in Intersect S by A2,A3,A4,YELLOW_8:def 1;
hence S is Basis of x by A5,A6,TOPS_2:64,YELLOW_8:def 1;
end;
assume
A10: S is Basis of x;
then S c= the topology of TopSpaceNorm X by TOPS_2:64;
then
A11: St c= the topology of LinearTopSpaceNorm X by A1,Def4;
A12: now
let Ut be Subset of LinearTopSpaceNorm X such that
A13: Ut is open and
A14: xt in Ut;
reconsider U=Ut as open Subset of TopSpaceNorm X by A13,Def4,Th20;
consider V being Subset of TopSpaceNorm X such that
A15: V in S & V c= U by A2,A10,A14,YELLOW_8:def 1;
reconsider Vt=V as Subset of LinearTopSpaceNorm X by Def4;
take Vt;
thus Vt in St & Vt c= Ut by A1,A15;
end;
xt in Intersect St by A2,A3,A10,YELLOW_8:def 1;
hence thesis by A11,A12,TOPS_2:64,YELLOW_8:def 1;
end;
registration
let X be RealNormSpace;
cluster LinearTopSpaceNorm X -> first-countable;
coherence
proof
now
let xt be Point of LinearTopSpaceNorm X;
reconsider x=xt as Point of TopSpaceNorm X by Def4;
consider B be Basis of x such that
A1: B is countable by FRECHET:def 2;
reconsider Bt=B as Basis of xt by Th25,Def4;
take Bt;
thus Bt is countable by A1;
end;
hence thesis by FRECHET:def 2;
end;
cluster LinearTopSpaceNorm X -> Frechet;
coherence;
cluster LinearTopSpaceNorm X -> sequential;
coherence;
end;
theorem Th26:
for X be RealNormSpace, S be sequence of TopSpaceNorm X, St be
sequence of LinearTopSpaceNorm X, x be Point of TopSpaceNorm X, xt be Point of
LinearTopSpaceNorm X st S=St & x=xt holds St is_convergent_to xt iff S
is_convergent_to x
proof
let X be RealNormSpace, S be sequence of TopSpaceNorm X, St be sequence of
LinearTopSpaceNorm X, x be Point of TopSpaceNorm X, xt be Point of
LinearTopSpaceNorm X;
assume that
A1: S=St and
A2: x=xt;
A3: now
assume
A4: S is_convergent_to x;
now
let U1t be Subset of LinearTopSpaceNorm X such that
A5: U1t is open and
A6: xt in U1t;
reconsider U1=U1t as open Subset of TopSpaceNorm X by A5,Def4,Th20;
consider n being Nat such that
A7: for m being Nat st n <= m holds S.m in U1 by A2,A4,A6,
FRECHET:def 3;
take n;
let m be Nat;
assume n <= m;
hence St.m in U1t by A1,A7;
end;
hence St is_convergent_to xt by FRECHET:def 3;
end;
now
assume
A8: St is_convergent_to xt;
now
let U1 be Subset of TopSpaceNorm X such that
A9: U1 is open and
A10: x in U1;
reconsider U1t=U1 as open Subset of LinearTopSpaceNorm X by A9,Def4,Th20;
consider n being Nat such that
A11: for m being Nat st n <= m holds St.m in U1t by A2,A8,A10,
FRECHET:def 3;
take n;
let m be Nat;
assume n <= m;
hence S.m in U1 by A1,A11;
end;
hence S is_convergent_to x by FRECHET:def 3;
end;
hence thesis by A3;
end;
theorem Th27:
for X be RealNormSpace, S be sequence of TopSpaceNorm X, St be
sequence of LinearTopSpaceNorm X st S=St holds St is convergent iff S is
convergent
proof
let X be RealNormSpace, S be sequence of TopSpaceNorm X, St be sequence of
LinearTopSpaceNorm X;
assume
A1: S=St;
A2: now
assume S is convergent;
then consider x be Point of TopSpaceNorm X such that
A3: S is_convergent_to x by FRECHET:def 4;
reconsider xt=x as Point of LinearTopSpaceNorm X by Def4;
St is_convergent_to xt by A1,A3,Th26;
hence St is convergent by FRECHET:def 4;
end;
now
assume St is convergent;
then consider xt be Point of LinearTopSpaceNorm X such that
A4: St is_convergent_to xt by FRECHET:def 4;
reconsider x=xt as Point of TopSpaceNorm X by Def4;
S is_convergent_to x by A1,A4,Th26;
hence S is convergent by FRECHET:def 4;
end;
hence thesis by A2;
end;
theorem Th28:
for X be RealNormSpace, S be sequence of TopSpaceNorm X, St be
sequence of LinearTopSpaceNorm X st S=St & St is convergent holds Lim S = Lim
St & lim S = lim St
proof
let X be RealNormSpace, S be sequence of TopSpaceNorm X, St be sequence of
LinearTopSpaceNorm X;
assume that
A1: S=St and
A2: St is convergent;
A3: S is convergent by A1,A2,Th27;
then consider x be Point of TopSpaceNorm X such that
A4: S is_convergent_to x by FRECHET:def 4;
reconsider xxt=x as Point of LinearTopSpaceNorm X by Def4;
St is_convergent_to xxt by A1,A4,Th26;
then
A5: lim St = xxt by FRECHET2:25
.=lim S by A4,FRECHET2:25;
reconsider Sn=S as sequence of X;
consider xt be Point of LinearTopSpaceNorm X such that
A6: Lim St = {xt} by A2,FRECHET2:24;
xt in {xt} by TARSKI:def 1;
then St is_convergent_to xt by A6,FRECHET:def 5;
then Lim St = {lim St} by A6,FRECHET2:25
.= {lim Sn} by A3,A5,Th14
.= Lim S by A3,Th14;
hence thesis by A5;
end;
theorem
for X be RealNormSpace, S be sequence of X, St be sequence of
LinearTopSpaceNorm X, x be Point of X, xt be Point of LinearTopSpaceNorm X st S
=St & x=xt holds St is_convergent_to xt iff
for r be Real st 0 < r ex m be
Nat st for n be Nat st m <= n holds ||.(S.n) - x.|| < r
proof
let X be RealNormSpace, S be sequence of X, St be sequence of
LinearTopSpaceNorm X, x be Point of X, xt be Point of LinearTopSpaceNorm X;
reconsider xxt=xt as Point of TopSpaceNorm X by Def4;
assume
A1: S=St & x=xt;
the carrier of LinearTopSpaceNorm X = the carrier of TopSpaceNorm X by Def4;
then reconsider SSt = St as sequence of TopSpaceNorm X;
St is_convergent_to xt iff SSt is_convergent_to xxt by Th26;
hence thesis by A1,Th12;
end;
theorem
for X be RealNormSpace, S be sequence of X, St be sequence of
LinearTopSpaceNorm X st S=St holds St is convergent iff S is convergent
proof
let X be RealNormSpace, S be sequence of X, St be sequence of
LinearTopSpaceNorm X;
assume
A1: S=St;
the carrier of LinearTopSpaceNorm X = the carrier of TopSpaceNorm X by Def4;
then reconsider SSt = St as sequence of TopSpaceNorm X;
St is convergent iff SSt is convergent by Th27;
hence thesis by A1,Th13;
end;
theorem
for X be RealNormSpace, S be sequence of X, St be sequence of
LinearTopSpaceNorm X st S=St & St is convergent holds Lim St = {lim S} & lim St
=lim S
proof
let X be RealNormSpace, S be sequence of X, St be sequence of
LinearTopSpaceNorm X;
assume that
A1: S=St and
A2: St is convergent;
the carrier of LinearTopSpaceNorm X = the carrier of TopSpaceNorm X by Def4;
then reconsider SSt = St as sequence of TopSpaceNorm X;
SSt is convergent by A2,Th27;
then Lim SSt = {lim S} & lim SSt=lim S by A1,Th14;
hence thesis by A2,Th28;
end;
theorem
for X be RealNormSpace, V be Subset of X, Vt be Subset of
LinearTopSpaceNorm X st V=Vt holds V is closed iff Vt is closed
proof
let X be RealNormSpace, V be Subset of X, Vt be Subset of LinearTopSpaceNorm
X;
reconsider VVt = Vt as Subset of TopSpaceNorm X by Def4;
assume
A1: V=Vt;
Vt is closed iff VVt is closed by Th21;
hence thesis by A1,Th15;
end;
theorem
for X be RealNormSpace, V be Subset of X, Vt be Subset of
LinearTopSpaceNorm X st V=Vt holds V is open iff Vt is open
proof
let X be RealNormSpace, V be Subset of X, Vt be Subset of LinearTopSpaceNorm
X;
reconsider VVt = Vt as Subset of TopSpaceNorm X by Def4;
assume
A1: V=Vt;
Vt is open iff VVt is open by Th20;
hence thesis by A1,Th16;
end;
theorem Th34:
for X be RealNormSpace, U be Subset of TopSpaceNorm X, Ut be
Subset of LinearTopSpaceNorm X, x be Point of TopSpaceNorm X, xt be Point of
LinearTopSpaceNorm X st U=Ut & x=xt holds U is a_neighborhood of x iff Ut is
a_neighborhood of xt
proof
let X be RealNormSpace, U be Subset of TopSpaceNorm X, Ut be Subset of
LinearTopSpaceNorm X, x be Point of TopSpaceNorm X, xt be Point of
LinearTopSpaceNorm X;
assume that
A1: U=Ut and
A2: x=xt;
hereby
assume U is a_neighborhood of x;
then consider V be Subset of TopSpaceNorm X such that
A3: V is open and
A4: V c= U and
A5: x in V by CONNSP_2:6;
reconsider Vt=V as open Subset of LinearTopSpaceNorm X by A3,Def4,Th20;
Vt c= Ut by A1,A4;
hence Ut is a_neighborhood of xt by A2,A5,CONNSP_2:6;
end;
assume Ut is a_neighborhood of xt;
then consider Vt be Subset of LinearTopSpaceNorm X such that
A6: Vt is open and
A7: Vt c= Ut and
A8: xt in Vt by CONNSP_2:6;
reconsider V=Vt as open Subset of TopSpaceNorm X by A6,Def4,Th20;
V c= U by A1,A7;
hence thesis by A2,A8,CONNSP_2:6;
end;
theorem Th35:
for X,Y be RealNormSpace, f be Function of TopSpaceNorm X,
TopSpaceNorm Y, ft be Function of LinearTopSpaceNorm X,LinearTopSpaceNorm Y, x
be Point of TopSpaceNorm X, xt be Point of LinearTopSpaceNorm X st f=ft & x=xt
holds f is_continuous_at x iff ft is_continuous_at xt
proof
let X,Y be RealNormSpace, f be Function of TopSpaceNorm X,TopSpaceNorm Y, ft
be Function of LinearTopSpaceNorm X,LinearTopSpaceNorm Y, x be Point of
TopSpaceNorm X, xt be Point of LinearTopSpaceNorm X;
assume that
A1: f=ft and
A2: x=xt;
hereby
assume
A3: f is_continuous_at x;
now
let Gt be a_neighborhood of ft.xt;
Gt is Subset of TopSpaceNorm Y by Def4;
then reconsider G=Gt as a_neighborhood of f.x by A1,A2,Th34;
consider H being a_neighborhood of x such that
A4: f.:H c= G by A3,TMAP_1:def 2;
H is Subset of LinearTopSpaceNorm X by Def4;
then reconsider Ht=H as a_neighborhood of xt by A2,Th34;
take Ht;
thus ft.:Ht c= Gt by A1,A4;
end;
hence ft is_continuous_at xt by TMAP_1:def 2;
end;
assume
A5: ft is_continuous_at xt;
now
let G be a_neighborhood of f.x;
G is Subset of LinearTopSpaceNorm Y by Def4;
then reconsider Gt=G as a_neighborhood of ft.xt by A1,A2,Th34;
consider Ht being a_neighborhood of xt such that
A6: ft.:Ht c= Gt by A5,TMAP_1:def 2;
Ht is Subset of TopSpaceNorm X by Def4;
then reconsider H=Ht as a_neighborhood of x by A2,Th34;
take H;
thus f.:H c= G by A1,A6;
end;
hence thesis by TMAP_1:def 2;
end;
theorem
for X,Y be RealNormSpace, f be Function of TopSpaceNorm X,TopSpaceNorm
Y, ft be Function of LinearTopSpaceNorm X,LinearTopSpaceNorm Y st f=ft holds f
is continuous iff ft is continuous
proof
let X,Y be RealNormSpace, f be Function of TopSpaceNorm X,TopSpaceNorm Y, ft
be Function of LinearTopSpaceNorm X,LinearTopSpaceNorm Y;
assume
A1: f=ft;
hereby
assume
A2: f is continuous;
now
let xt be Point of LinearTopSpaceNorm X;
reconsider x=xt as Point of TopSpaceNorm X by Def4;
f is_continuous_at x by A2,TMAP_1:44;
hence ft is_continuous_at xt by A1,Th35;
end;
hence ft is continuous by TMAP_1:44;
end;
assume
A3: ft is continuous;
now
let x be Point of TopSpaceNorm X;
reconsider xt=x as Point of LinearTopSpaceNorm X by Def4;
ft is_continuous_at xt by A3,TMAP_1:44;
hence f is_continuous_at x by A1,Th35;
end;
hence thesis by TMAP_1:44;
end;