Copyright (c) 1998 Association of Mizar Users
environ
vocabulary ARYTM_3, ARYTM_1, NORMSP_1, RELAT_1, FUNCT_1, PRE_TOPC, CANTOR_1,
BOOLE, SUBSET_1, SETFAM_1, TARSKI, METRIC_1, RCOMP_1, ABSVALUE, TOPMETR,
PCOMPS_1, CARD_4, FUNCT_4, FUNCOP_1, SEQ_2, ORDINAL2, ORDINAL1, FRECHET,
RLVECT_3, ARYTM;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, REAL_1, NAT_1,
SETFAM_1, STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, ORDINAL1,
CARD_4, FUNCT_4, ABSVALUE, RCOMP_1, PRE_TOPC, TOPS_2, METRIC_1, PCOMPS_1,
TOPMETR, NORMSP_1, CANTOR_1, YELLOW_8;
constructors REAL_1, NAT_1, RAT_1, NORMSP_1, YELLOW_8, CARD_4, TOPS_2,
TOPMETR, CANTOR_1, FUNCT_4, RCOMP_1, MEMBERED;
clusters SUBSET_1, XREAL_0, PRE_TOPC, STRUCT_0, COMPLSP1, NORMSP_1, METRIC_1,
PCOMPS_1, TOPMETR, FUNCOP_1, RELSET_1, XBOOLE_0, NAT_1, MEMBERED,
ZFMISC_1, FUNCT_1, FUNCT_2, PARTFUN1, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, TOPS_2, XBOOLE_0;
theorems REAL_1, REAL_2, TARSKI, ZFMISC_1, SUBSET_1, SETFAM_1, PRE_TOPC,
FUNCT_1, FUNCT_2, FUNCT_4, ABSVALUE, FUNCOP_1, NORMSP_1, NAT_1, ORDINAL1,
RELAT_1, CARD_1, CARD_5, WAYBEL12, YELLOW_8, AXIOMS, TOPS_1, TOPS_2,
TOPMETR, RCOMP_1, CANTOR_1, METRIC_1, PCOMPS_1, GOBOARD6, RELSET_1,
XREAL_0, XBOOLE_0, XBOOLE_1, SEQ_4, XCMPLX_0, XCMPLX_1;
schemes DOMAIN_1, ZFREFLE1, NAT_1, CARD_4, COMPTS_1;
begin
Lm1:
for n being Nat st n<>0 holds 1/n > 0
proof
let n be Nat;
assume
A1: n<>0;
n >= 0 by NAT_1:18;
hence 1/n>0 by A1,REAL_2:127;
end;
Lm2:
for r being Real st r>0
ex n being Nat st 1/n < r & n<>0
proof
let r be Real;
assume
A1: r>0;
consider n being Nat such that
A2: 1/r < n by SEQ_4:10;
take n;
1/r > 0 by A1,REAL_2:127;
then 1/(1/r) > 1/n by A2,REAL_2:151;
hence 1/n < r by XCMPLX_1:56;
thus n <> 0 by A1,A2,REAL_2:127;
end;
::
:: Preliminaries
::
theorem Th1:
for T being non empty 1-sorted,S being sequence of T holds
rng S is Subset of T
proof
let T be non empty 1-sorted,S be sequence of T;
rng S c= the carrier of T
proof
let y be set;
assume y in rng S;
then consider x being set such that
A1: x in dom S & S.x = y by FUNCT_1:def 5;
x in NAT by A1,NORMSP_1:17;
then S.x is Element of T by NORMSP_1:17;
hence y in the carrier of T by A1;
end;
hence rng S is Subset of T;
end;
definition
let T be non empty 1-sorted;
let S be sequence of T;
redefine func rng S -> Subset of T;
coherence by Th1;
end;
theorem Th2:
for T1 being non empty 1-sorted, T2 being 1-sorted, S being sequence of T1 st
rng S c= the carrier of T2 holds
S is sequence of T2
proof
let T1 be non empty 1-sorted, T2 be 1-sorted, S be sequence of T1;
assume
A1: rng S c= the carrier of T2;
dom S = NAT by FUNCT_2:def 1;
then S is Function of NAT,the carrier of T2 by A1,FUNCT_2:4;
hence S is sequence of T2 by NORMSP_1:def 3;
end;
theorem Th3:
for T being non empty TopSpace, x being Point of T, B being Basis of x
holds B <> {}
proof
let T be non empty TopSpace, x be Point of T, B be Basis of x;
A1: x in the carrier of T;
the carrier of T in the topology of T by PRE_TOPC:def 1;
then A2: [#]T in the topology of T & x in [#]T by A1,PRE_TOPC:12;
set U1=[#]T;
reconsider T as non empty TopStruct;
x in U1 & U1 is open by A2,PRE_TOPC:def 5;
then ex U2 be Subset of T st U2 in B & U2 c= U1 by YELLOW_8:22;
hence B <> {};
end;
definition
let T be non empty TopSpace;
let x be Point of T;
cluster -> non empty Basis of x;
coherence by Th3;
end;
Lm3:
for T being TopStruct,A being Subset of T holds
A is open iff [#]T \ A is closed
proof
let T be TopStruct,A be Subset of T;
thus A is open implies [#]T \ A is closed
proof
assume A is open;
then [#](T) \ ([#](T) \ A) is open by PRE_TOPC:22;
hence thesis by PRE_TOPC:def 6;
end;
assume [#]T \ A is closed;
then [#](T) \ ([#](T) \ A) is open by PRE_TOPC:def 6;
hence thesis by PRE_TOPC:22;
end;
theorem Th4:
for T being TopSpace, A,B being Subset of T st
A is open & B is closed holds
A \ B is open
proof
let T be TopSpace, A,B be Subset of T;
assume
A1: A is open & B is closed;
then [#](T)\B is open by PRE_TOPC:def 6;
then A /\ ([#](T)\B) is open by A1,TOPS_1:38;
then A2: A /\ [#](T) \ A /\ B is open by XBOOLE_1:50;
A c= the carrier of T;
then A c= [#](T) by PRE_TOPC:12;
then A /\ [#](T) = A by XBOOLE_1:28;
hence A\B is open by A2,XBOOLE_1:47;
end;
theorem Th5:
for T being TopStruct st
{}T is closed & [#]T is closed &
(for A,B being Subset of T st A is closed & B is closed
holds A \/ B is closed) &
for F being Subset-Family of T st F is closed holds meet F is closed
holds T is TopSpace
proof
let T be TopStruct;
assume that
A1: {}T is closed & [#]T is closed and
A2: (for A,B being Subset of T st A is closed & B is closed
holds A \/ B is closed) and
A3: for F being Subset-Family of T st F is closed holds
meet F is closed;
A4: the carrier of T in the topology of T
proof
[#]T \ {}T is open by A1,PRE_TOPC:def 6;
then [#]T in the topology of T by PRE_TOPC:def 5;
hence thesis by PRE_TOPC:12;
end;
A5: for G being Subset-Family of T
st G c= the topology of T
holds union G in the topology of T
proof
let G be Subset-Family of T;
reconsider G' = G as Subset-Family of T;
assume
A6: G c= the topology of T;
per cases;
suppose A7: G = {};
[#]T \ {}T = [#]T;
then {}T is open by A1,Lm3;
hence thesis by A7,PRE_TOPC:def 5,ZFMISC_1:2;
suppose
A8: G<>{};
A9: for A being Subset of T holds
A in G implies [#]T \ A is closed
proof
let A be Subset of T;
assume A in G;
then A is open by A6,PRE_TOPC:def 5;
hence [#]T \ A is closed by Lm3;
end;
reconsider CG = COMPLEMENT(G) as Subset-Family of T;
COMPLEMENT(G) is closed
proof
let A be Subset of T;
assume A in COMPLEMENT(G);
then A` in G' by YELLOW_8:13;
then [#]T \ A` is closed by A9;
then [#]T \([#]T \ A) is closed by PRE_TOPC:17;
hence A is closed by PRE_TOPC:22;
end;
then meet CG is closed by A3;
then (union G')` is closed by A8,TOPS_2:11;
then [#]T \ union G is closed by PRE_TOPC:17;
then union G is open by Lm3;
hence thesis by PRE_TOPC:def 5;
end;
for A,B being Subset of T st
A in the topology of T & B in the topology of T
holds A /\ B in the topology of T
proof
let A,B be Subset of T;
assume that
A10: A in the topology of T and
A11: B in the topology of T;
reconsider A, B as Subset of T;
A is open by A10,PRE_TOPC:def 5;
then A12: [#]T \ A is closed by Lm3;
B is open by A11,PRE_TOPC:def 5;
then [#]T \ B is closed by Lm3;
then ([#]T \ A) \/ ([#]T \ B) is closed by A2,A12;
then [#]T \ (A /\ B) is closed by XBOOLE_1:54;
then (A /\ B) is open by Lm3;
hence thesis by PRE_TOPC:def 5;
end;
hence thesis by A4,A5,PRE_TOPC:def 1;
end;
theorem Th6:
for T being TopSpace, S being non empty TopStruct, f being map of T,S
st for A being Subset of S holds A is closed iff f"A is closed
holds S is TopSpace
proof
let T be TopSpace, S be non empty TopStruct, f be map of T,S;
assume
A1: for A being Subset of S holds A is closed iff f"A is closed;
A2: {}S is closed
proof
A3: {}T is closed by TOPS_1:22;
f"{}={} by RELAT_1:171;
hence thesis by A1,A3;
end;
A4: [#]S is closed
proof
f"([#]S) = [#]T by TOPS_2:52;
hence thesis by A1;
end;
A5: for A,B being Subset of S st A is closed & B is closed
holds A \/ B is closed
proof
let A,B be Subset of S;
assume
A is closed & B is closed;
then f"A is closed & f"B is closed by A1;
then f"A \/ f"B is closed by TOPS_1:36;
then f"(A \/ B) is closed by RELAT_1:175;
hence thesis by A1;
end;
for F being Subset-Family of S st F is closed holds meet F is closed
proof
let F be Subset-Family of S;
assume
A6: F is closed;
per cases;
suppose F = {}S;
hence meet F is closed by A2,SETFAM_1:def 1;
suppose
A7: F <> {};
set F1 = {f"A where A is Subset of S : A in F};
ex A being set st A in F
proof
consider A being Element of F;
take A;
thus A in F by A7;
end;
then consider A being Subset of S such that
A8: A in F;
reconsider A as Subset of S;
A9: f"A in F1 by A8;
F1 c= bool the carrier of T
proof
let B be set;
assume B in F1;
then consider A being Subset of S such that
A10: B=f"A & A in F;
thus B in bool the carrier of T by A10;
end;
then F1 is Subset-Family of T by SETFAM_1:def 7;
then reconsider F1 as Subset-Family of T;
A11: meet(F1) = f"(meet F)
proof
thus meet(F1) c= f"(meet F)
proof
let x be set;
assume A12: x in meet(F1);
then x in the carrier of T;
then A13: x in dom f by FUNCT_2:def 1;
for A be set st A in F holds f.x in A
proof
let A be set;
assume
A14: A in F;
then reconsider A as Subset of S;
f"A in F1 by A14;
then x in f"A by A12,SETFAM_1:def 1;
hence thesis by FUNCT_1:def 13;
end;
then f.x in meet F by A7,SETFAM_1:def 1;
hence x in f"(meet F) by A13,FUNCT_1:def 13;
end;
thus f"(meet F) c= meet(F1)
proof
let x be set;
assume x in f"(meet F);
then A15: x in dom f & f.x in meet F by FUNCT_1:def 13;
for B be set st B in F1 holds x in B
proof
let B be set;
assume B in F1;
then consider A being Subset of S such that
A16: B = f"A & A in F;
f.x in A by A15,A16,SETFAM_1:def 1;
hence thesis by A15,A16,FUNCT_1:def 13;
end;
hence x in meet(F1) by A9,SETFAM_1:def 1;
end;
end;
F1 is closed
proof
let B be Subset of T;
assume B in F1;
then consider A being Subset of S such that
A17: f"A = B & A in F;
A is closed by A6,A17,TOPS_2:def 2;
hence B is closed by A1,A17;
end;
then meet F1 is closed by TOPS_2:29;
hence thesis by A1,A11;
end;
hence thesis by A2,A4,A5,Th5;
end;
theorem Th7:
for x being Point of RealSpace, x',r being Real st x' = x & r > 0 holds
Ball(x,r) = ].x'-r, x'+r.[
proof
let x be Point of RealSpace, x',r be Real;
assume
A1:
x' = x & r > 0;
thus Ball(x,r) c= ].x'-r, x'+r.[
proof
let y be set;
assume
A2: y in Ball(x,r);
then reconsider y1=y as Element of RealSpace;
A3: dist(x,y1)<r by A2,METRIC_1:12;
reconsider x2=x,y2=y1 as Element of REAL by METRIC_1:def 14;
dist(x,y1)=real_dist.(x2,y2) by METRIC_1:def 1,def 14
.=abs(x2 - y2 ) by METRIC_1:def 13
.=abs(-(y2 - x2) ) by XCMPLX_1:143
.=abs(y2 - x2 ) by ABSVALUE:17;
hence y in ].x'-r, x'+r.[ by A1,A3,RCOMP_1:8;
end;
let y be set;
assume
A4: y in ].x'-r, x'+r.[;
then reconsider y2=y as Real;
abs(y2 - x' )=abs(-(y2 - x') ) by ABSVALUE:17
.=abs(x' - y2 ) by XCMPLX_1:143
.=real_dist.(x',y2) by METRIC_1:def 13;
then A5: real_dist.(x',y2) < r by A4,RCOMP_1:8;
reconsider x1=x',y1=y2 as Element of RealSpace
by METRIC_1:def 14;
dist(x1,y1)=real_dist.(x',y2) by METRIC_1:def 1,def 14;
hence y in Ball(x,r) by A1,A5,METRIC_1:12;
end;
theorem
for A being Subset of R^1 holds A is open iff
for x being Real st x in A ex r being Real st r >0 & ].x-r, x+r.[ c= A
proof
let A be Subset of R^1;
thus A is open implies
for x being Real st x in A ex r being Real st r >0 & ].x-r, x+r.[ c= A
proof
assume
A1: A is open;
let x be Real;
assume
A2: x in A;
reconsider x1=x as Element of REAL;
reconsider x1 as Element of RealSpace by METRIC_1:def 14;
reconsider A1=A as Subset of R^1;
A3: A1 in the topology of R^1 by A1,PRE_TOPC:def 5;
the topology of R^1 = Family_open_set(RealSpace) by TOPMETR:16,def 7;
then consider r being Real such that
A4: r>0 & Ball(x1,r) c= A1 by A2,A3,PCOMPS_1:def 5;
].x-r, x+r.[ c=A1 by A4,Th7;
hence ex r being Real st r >0 & ].x-r, x+r.[ c= A by A4;
end;
assume
A5: for x being Real st x in A ex r being Real st r >0 & ].x-r, x+r.[ c= A;
reconsider A1=A as Subset of RealSpace by TOPMETR:16,def 7;
for x being Element of RealSpace
st x in A1 holds ex r being Real st r>0 & Ball(x,r) c= A1
proof
let x be Element of RealSpace;
assume
A6: x in A1;
reconsider x1=x as Real by METRIC_1:def 14;
consider r being Real such that
A7: r >0 & ].x1-r, x1+r.[ c= A1 by A5,A6;
Ball(x,r) c= A1 by A7,Th7;
hence ex r being Real st r>0 & Ball(x,r) c= A1 by A7;
end;
then A8: A1 in Family_open_set(RealSpace) by PCOMPS_1:def 5;
the topology of R^1 = Family_open_set(RealSpace) by TOPMETR:16,def 7;
hence A is open by A8,PRE_TOPC:def 5;
end;
theorem Th9:
for S being sequence of R^1
st (for n being Nat holds S.n in ]. n - 1/4 , n + 1/4 .[)
holds rng S is closed
proof
let S be sequence of R^1;
assume
A1: for n being Nat holds S.n in ]. n - 1/4 , n + 1/4 .[;
reconsider B=rng S as Subset of TopSpaceMetr(RealSpace) by TOPMETR:def 7;
for x being Point of RealSpace
st x in B` ex r being real number st r>0 & Ball(x,r) c= B`
proof
let x be Point of RealSpace;
assume
A2: x in B`;
reconsider x1=x as Real by METRIC_1:def 14;
per cases;
suppose ]. x1 - 1/4 , x1 + 1/4 .[ /\ B = {};
then ]. x1 - 1/4 , x1 + 1/4 .[ /\ B`` = {};
then A3: Ball(x,1/4) /\ B`` = {} by Th7;
reconsider C=Ball(x,1/4)
as Subset of TopSpaceMetr(RealSpace) by TOPMETR:16;
C misses B`` by A3,XBOOLE_0:def 7;
then Ball(x,1/4) c= B` by TOPS_1:20;
hence thesis;
suppose
A4: ]. x1 - 1/4 , x1 + 1/4 .[ /\ B <> {};
consider y being Element of ]. x1 - 1/4 , x1 + 1/4 .[ /\ B;
A5: y in ]. x1 - 1/4 , x1 + 1/4 .[ & y in B by A4,XBOOLE_0:def 3;
then reconsider y as Real;
consider n1 being set such that
A6: n1 in dom S and
A7: y = S.n1 by A5,FUNCT_1:def 5;
reconsider n1 as Nat by A6,NORMSP_1:17;
consider r being Real such that
A8: r=abs( x1 - y );
x1 <> y
proof
assume x1 = y;
then y in B /\ (B`) by A2,A5,XBOOLE_0:def 3;
then B meets (B`) by XBOOLE_0:4;
hence contradiction by TOPS_1:20;
end;
then x1 + (-y) <> y + (-y) by XCMPLX_1:2;
then x1 + -y <> 0 by XCMPLX_0:def 6;
then A9: x1 - y <> 0 by XCMPLX_0:def 8;
then A10: abs(x1-y) > 0 by ABSVALUE:6;
A11: r>0 by A8,A9,ABSVALUE:6;
abs(y-x1) < 1/4 by A5,RCOMP_1:8;
then abs(-(x1-y)) < 1/4 by XCMPLX_1:143;
then A12: r<=1/4 by A8,ABSVALUE:17;
Ball(x,r) misses rng S
proof
assume Ball(x,r) meets rng S;
then consider z being set such that
A13: z in Ball(x,r) & z in rng S by XBOOLE_0:3;
consider n2 being set such that
A14: n2 in dom S and
A15: z = S.n2 by A13,FUNCT_1:def 5;
reconsider z as Real by A13,METRIC_1:def 14;
reconsider n2 as Nat by A14,NORMSP_1:17;
per cases by REAL_1:def 5;
suppose n1=n2;
then A16: y in ].x1-r,x1+r.[ by A7,A11,A13,A15,Th7;
r = abs( 0 + -y + x1 ) by A8,XCMPLX_0:def 8
.= abs( 0 - y + x1 ) by XCMPLX_0:def 8
.= abs( 0 - (y - x1) ) by XCMPLX_1:37
.= abs( 0 + -(y - x1) ) by XCMPLX_0:def 8
.= abs( y - x1 ) by ABSVALUE:17;
hence contradiction by A16,RCOMP_1:8;
suppose n1>n2;
then A17: n2 + 1 <= n1 by NAT_1:38;
S.n2 in ].n2-1/4,n2+1/4.[ by A1;
then S.n2 in {a where a is Real : n2-1/4<a & a<n2+1/4} by RCOMP_1:def 2;
then consider a2 being Real such that
A18: S.n2=a2 & n2-1/4<a2 & a2<n2+1/4;
z - 1/4 < n2 by A15,A18,REAL_1:84;
then A19: n2 + 1 > z - 1/4 + 1 by REAL_1:53;
S.n1 in ]. n1 - 1/4 , n1 + 1/4 .[ by A1;
then S.n1 in {a where a is Real : n1-1/4<a & a<n1+1/4} by RCOMP_1:def 2;
then consider a1 being Real such that
A20: S.n1=a1 & n1 - 1/4 < a1 & a1 < n1 + 1/4;
n1 < y + 1/4 by A7,A20,REAL_1:84;
then n2 +1 < y + 1/4 by A17,AXIOMS:22;
then z - 1/4 + 1 < y + 1/4 by A19,AXIOMS:22;
then z + -1/4 + 1 < y + 1/4 by XCMPLX_0:def 8;
then z + (-1/4 + 1) < y + 1/4 by XCMPLX_1:1;
then z < y + 1/4 - (-1/4 + 1) by REAL_1:86;
then z < y + 1/4 + -(-1/4 + 1) by XCMPLX_0:def 8;
then A21: z < y + (1/4 + -(-1/4 + 1)) by XCMPLX_1:1;
Ball(x,r) c= Ball(x,1/4) by A12,PCOMPS_1:1;
then z in Ball(x,1/4) by A13;
then z in ].x1-1/4 ,x1 +1/4.[ by Th7;
then z in {a where a is Real : x1-1/4<a & a<x1 +1/4} by RCOMP_1:def 2;
then consider a1 being Real such that
A22: a1=z & x1-1/4<a1 & a1<x1 +1/4;
A23: z + 1/4 > x1 by A22,REAL_1:84;
y in {a where a is Real : x1 - 1/4 < a & a < x1 + 1/4 }
by A5,RCOMP_1:def 2;
then consider a1 being Real such that
A24: y=a1 & x1 - 1/4 < a1 & a1 < x1 + 1/4;
y -1/4 < x1 + 1/4 - 1/4 by A24,REAL_1:54;
then y -1/4 < x1 + 1/4 + -1/4 by XCMPLX_0:def 8;
then y - 1/4 < x1 + (1/4 + -1/4) by XCMPLX_1:1;
then z + 1/4 > y - 1/4 by A23,AXIOMS:22;
then z + 1/4 + -1/4 > y - 1/4 + -1/4 by REAL_1:53;
then z + (1/4 + -1/4) > y - 1/4 + -1/4 by XCMPLX_1:1;
then z > y + -1/4 + -1/4 by XCMPLX_0:def 8;
then z > y + (-1/4 + -1/4) by XCMPLX_1:1;
hence contradiction by A21;
suppose n1<n2;
then A25: n1 + 1 <= n2 by NAT_1:38;
S.n2 in ].n2-1/4,n2+1/4.[ by A1;
then S.n2 in {a where a is Real : n2-1/4<a & a<n2+1/4} by RCOMP_1:def 2;
then consider a2 being Real such that
A26: S.n2=a2 & n2-1/4<a2 & a2<n2+1/4;
z + 1/4 > n2 - 1/4 + 1/4 by A15,A26,REAL_1:53;
then z + 1/4 > n2 + -1/4 + 1/4 by XCMPLX_0:def 8;
then z + 1/4 > n2 + (-1/4 + 1/4) by XCMPLX_1:1;
then A27: z + 1/4 > n1 + 1 by A25,AXIOMS:22;
S.n1 in ]. n1 - 1/4 , n1 + 1/4 .[ by A1;
then S.n1 in {a where a is Real : n1-1/4<a & a<n1+1/4} by RCOMP_1:def 2;
then consider a1 being Real such that
A28: S.n1=a1 & n1-1/4<a1 & a1<n1+1/4;
n1 + 1/4 - 1/4 > y - 1/4 by A7,A28,REAL_1:54;
then n1 + 1/4 + -1/4 > y - 1/4 by XCMPLX_0:def 8;
then n1 + (1/4 + -1/4) > y - 1/4 by XCMPLX_1:1;
then n1 + 1 > y - 1/4 + 1 by REAL_1:53;
then z + 1/4 > y - 1/4 + 1 by A27,AXIOMS:22;
then y + -1/4 + 1 < z + 1/4 by XCMPLX_0:def 8;
then y + (-1/4 + 1) < z + 1/4 by XCMPLX_1:1;
then y + (-1/4 + 1) - (-1/4 + 1) < z + 1/4 - (-1/4 + 1) by REAL_1:54;
then y + (-1/4 + 1) + -(-1/4 + 1) < z + 1/4 - (-1/4 + 1) by XCMPLX_0:def 8
;
then y + ((-1/4 + 1) + -(-1/4 + 1)) < z + 1/4 - (-1/4 + 1) by XCMPLX_1:1;
then y < z + 1/4 + -(-1/4 + 1) by XCMPLX_0:def 8;
then A29: y < z + (1/4 + -(-1/4 + 1)) by XCMPLX_1:1;
Ball(x,r) c= Ball(x,1/4) by A12,PCOMPS_1:1;
then z in Ball(x,1/4) by A13;
then z in ].x1-1/4 ,x1 +1/4.[ by Th7;
then z in {a where a is Real : x1-1/4<a & a<x1 +1/4} by RCOMP_1:def 2;
then consider a1 being Real such that
A30: a1=z & x1-1/4<a1 & a1<x1 +1/4;
A31: z - 1/4 < x1 by A30,REAL_1:84;
y in {a where a is Real : x1 - 1/4 < a & a < x1 + 1/4 }
by A5,RCOMP_1:def 2;
then consider a1 being Real such that
A32: y=a1 & x1 - 1/4 < a1 & a1 < x1 + 1/4;
x1 - 1/4 + 1/4 < y + 1/4 by A32,REAL_1:53;
then x1 + -1/4 + 1/4 < y + 1/4 by XCMPLX_0:def 8;
then x1 + (-1/4 + 1/4) < y + 1/4 by XCMPLX_1:1;
then z - 1/4 < y + 1/4 by A31,AXIOMS:22;
then z - 1/4 + 1/4< y + 1/4 + 1/4 by REAL_1:53;
then z + -1/4 + 1/4< y + 1/4 + 1/4 by XCMPLX_0:def 8;
then z + (-1/4 + 1/4)< y + 1/4 + 1/4 by XCMPLX_1:1;
then z < y + (1/4 + 1/4) by XCMPLX_1:1;
then z - 1/2 < y + 1/2 - 1/2 by REAL_1:54;
then z - 1/2 < y + 1/2 + -1/2 by XCMPLX_0:def 8;
then z - 1/2 < y + (1/2 + -1/2) by XCMPLX_1:1;
hence contradiction by A29,XCMPLX_0:def 8;
end;
then A33: Ball(x,r) /\ B = {} by XBOOLE_0:def 7;
reconsider C=Ball(x,r)
as Subset of TopSpaceMetr(RealSpace) by TOPMETR:16;
C /\ B`` = {} by A33;
then C misses B`` by XBOOLE_0:def 7;
then C c= B` by TOPS_1:20;
hence ex r being real number st r>0 & Ball(x,r) c= B` by A8,A10;
end;
then (rng S)` is open by TOPMETR:22,def 7;
then [#](R^1)\(rng S) is open by PRE_TOPC:17;
hence rng S is closed by PRE_TOPC:def 6;
end;
theorem Th10:
for B being Subset of R^1 holds B = NAT implies B is closed
proof
let B be Subset of R^1;
assume
A1: B = NAT;
A2:
dom (id NAT) = NAT by FUNCT_1:34;
A3:
rng (id NAT) = NAT
proof
thus rng (id NAT) c= NAT
proof
let y be set;
assume y in rng (id NAT);
then consider x being set such that
A4: x in dom (id NAT) & y = (id NAT).x by FUNCT_1:def 5;
thus y in NAT by A2,A4,FUNCT_1:34;
end;
let y be set;
assume
A5: y in NAT;
then (id NAT).y = y by FUNCT_1:34;
hence y in rng (id NAT) by A2,A5,FUNCT_1:def 5;
end;
then id NAT is Function of NAT,the carrier of R^1 by A2,FUNCT_2:4,TOPMETR:24
;
then reconsider S=(id NAT) as sequence of R^1 by NORMSP_1:def 3;
for n being Nat holds S.n in ].n-1/4,n + 1/4.[
proof
let n be Nat;
reconsider x=S.n as Real by FUNCT_1:34;
A6: x=n by FUNCT_1:34;
A7: n < n + 1/4 by REAL_1:69;
- 1/4 + n < 0 + n by REAL_1:67;
then n - 1/4 < 0 + n by XCMPLX_0:def 8;
then x in {r where r is Real : n - 1/4 < r & r < n + 1/4} by A6,A7;
hence S.n in ].n - 1/4 , n + 1/4.[ by RCOMP_1:def 2;
end;
hence B is closed by A1,A3,Th9;
end;
theorem Th11:
for M being non empty MetrSpace,x being Point of TopSpaceMetr(M),
x' being Point of M st x=x'
ex B being Basis of x st
B={Ball(x',1/n) where n is Nat:n<>0} &
B is countable &
ex f being Function of NAT,B st for n being set st n in NAT holds
ex n' being Nat st n=n' & f.n = Ball(x',1/(n'+1))
proof
let M be non empty MetrSpace,x be Point of TopSpaceMetr(M),x' be Point of M;
assume
A1: x=x';
set B = { Ball(x',1/n) where n is Nat:n<>0};
B c= bool(the carrier of TopSpaceMetr(M))
proof
let A be set;
assume A in B;
then consider n being Nat such that
A2: A = Ball(x',1/n) and
n<>0;
Ball(x',1/n) c= the carrier of M;
then Ball(x',1/n) c= the carrier of TopSpaceMetr(M) by TOPMETR:16;
hence A in bool(the carrier of TopSpaceMetr(M)) by A2;
end;
then B is Subset-Family of TopSpaceMetr(M)
by SETFAM_1:def 7;
then reconsider B as Subset-Family of TopSpaceMetr(M);
A3:
B c= the topology of TopSpaceMetr(M)
proof
let A be set;
assume A in B;
then consider n being Nat such that
A4: A = Ball(x',1/n) and
n<>0;
Ball(x',1/n) in Family_open_set M by PCOMPS_1:33;
hence A in the topology of TopSpaceMetr(M) by A4,TOPMETR:16;
end;
A5:
x in Intersect B
proof
A6: Ball(x',1/1) in B;
then A7: Intersect B = meet B by CANTOR_1:def 3;
for O being set st O in B holds x in O
proof
let O be set;
assume O in B;
then consider n being Nat such that
A8: O = Ball(x',1/n) and
A9: n<>0;
1/n > 0 by A9,Lm1;
hence x in O by A1,A8,GOBOARD6:4;
end;
hence x in Intersect B by A6,A7,SETFAM_1:def 1;
end;
for O being Subset of TopSpaceMetr(M) st O is open & x in O
ex V being Subset of TopSpaceMetr(M) st V in B & V c= O
proof
let O be Subset of TopSpaceMetr(M);
assume
O is open & x in O;
then consider r being real number such that
A10: r>0 and
A11: Ball(x',r) c= O by A1,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
consider n being Nat such that
A12: 1/n < r and
A13: n <> 0 by A10,Lm2;
A14: Ball(x',1/n) c= Ball(x',r) by A12,PCOMPS_1:1;
reconsider Ba=Ball(x',1/n) as Subset of
TopSpaceMetr(M) by TOPMETR:16;
reconsider Ba as Subset of TopSpaceMetr(M);
take Ba;
thus Ba in B by A13;
thus Ba c= O by A11,A14,XBOOLE_1:1;
end;
then reconsider B as Basis of x by A3,A5,YELLOW_8:def 2;
take B;
deffunc F(Nat) = Ball(x',1/$1);
defpred P[Nat] means $1 <> 0;
thus B={Ball(x',1/n) where n is Nat:n<>0};
{ F(n) where n is Nat : P[n] } is countable from FraenCoun1;
hence B is countable;
defpred P[set,set] means
ex n' being Nat st $1=n' & $2 = Ball(x',1/(n'+1));
A15: for n being set st n in NAT ex O being set st O in B & P[n,O]
proof
let n be set;
assume n in NAT;
then reconsider n'=n as Nat;
reconsider O=Ball(x',1/(n'+1)) as set;
take O;
thus O in B;
take n';
thus n=n';
thus O = Ball(x',1/(n'+1));
end;
consider f being Function such that
A16: dom f = NAT and
A17: rng f c= B and
A18: for n being set st n in NAT holds P[n,f.n]
from NonUniqBoundFuncEx(A15);
reconsider f as Function of NAT,B by A16,A17,FUNCT_2:4;
take f;
thus for n being set st n in NAT holds
ex n' being Nat st n=n' & f.n = Ball(x',1/(n'+1)) by A18;
end;
theorem Th12:
for f,g being Function holds
rng(f+*g)=f.:(dom f\dom g) \/ rng g
proof
let f,g be Function;
thus rng(f+*g)c=f.:(dom f\dom g) \/ rng g
proof
let y be set;
assume y in rng(f+*g);
then consider x being set such that
A1: x in dom(f+*g) and
A2: (f+*g).x = y by FUNCT_1:def 5;
per cases;
suppose
A3: x in dom g;
then y = g.x by A2,FUNCT_4:14;
then y in rng g by A3,FUNCT_1:def 5;
hence y in f.:(dom f\dom g) \/ rng g by XBOOLE_0:def 2;
suppose
A4: not x in dom g;
then A5: y = f.x by A2,FUNCT_4:12;
x in dom f \/ dom g by A1,FUNCT_4:def 1;
then A6: x in dom f by A4,XBOOLE_0:def 2;
then x in dom f \ dom g by A4,XBOOLE_0:def 4;
then y in f.:(dom f \ dom g) by A5,A6,FUNCT_1:def 12;
hence y in f.:(dom f\dom g) \/ rng g by XBOOLE_0:def 2;
end;
let y be set;
assume
A7: y in f.:(dom f\dom g) \/ rng g;
per cases by A7,XBOOLE_0:def 2;
suppose y in f.:(dom f\dom g);
then consider x being set such that
A8: x in dom f and
A9: x in dom f \ dom g and
A10: f.x = y by FUNCT_1:def 12;
x in dom f \/ dom g by A8,XBOOLE_0:def 2;
then A11: x in dom(f+*g) by FUNCT_4:def 1;
not x in dom g by A9,XBOOLE_0:def 4;
then (f+*g).x = f.x by FUNCT_4:12;
hence y in rng(f+*g) by A10,A11,FUNCT_1:def 5;
suppose
A12: y in rng g;
rng g c= rng(f +* g) by FUNCT_4:19;
hence y in rng(f +* g) by A12;
end;
theorem Th13:
for A,B being set holds
B c= A implies (id A).:(B) = B
proof
let A,B be set;
assume
A1: B c= A;
A2: dom(id A) = A by FUNCT_1:34;
thus (id A).:(B) c= B
proof
let y be set;
assume y in (id A).:(B);
then consider x being set such that
A3: x in dom(id A) and
A4: x in B and
A5: (id A).x = y by FUNCT_1:def 12;
thus y in B by A2,A3,A4,A5,FUNCT_1:34;
end;
let y be set;
assume
A6: y in B;
then (id A).y = y by A1,FUNCT_1:34;
hence y in (id A).:(B) by A1,A2,A6,FUNCT_1:def 12;
end;
canceled;
theorem Th15:
for A,B,x being set holds
dom((id A)+*(B --> x)) = A \/ B
proof
let A,B,x be set;
dom((id A)+*(B --> x)) = dom (id A) \/ dom (B --> x) by FUNCT_4:def 1;
then dom((id A)+*(B --> x)) = A \/ dom (B --> x) by FUNCT_1:34;
hence dom((id A)+*(B --> x)) = A \/ B by FUNCOP_1:19;
end;
theorem Th16:
for A,B,x being set st B <> {} holds
rng((id A)+*(B --> x)) = (A \ B) \/ {x}
proof
let A,B,x be set;
assume
A1: B <> {};
set f = ((id A)+*(B --> x));
thus rng((id A)+*(B --> x)) c= (A \ B) \/ {x}
proof
let y be set;
assume
y in rng f;
then consider x1 being set such that
A2: x1 in dom f & y = f.x1 by FUNCT_1:def 5;
A3: x1 in dom (id A) \/ dom (B --> x) by A2,FUNCT_4:def 1;
per cases;
suppose
A4: x1 in dom (B --> x);
then A5: f.x1 = (B --> x).x1 by A3,FUNCT_4:def 1;
x1 in B by A4,FUNCOP_1:19;
then (B --> x).x1 = x by FUNCOP_1:13;
then y in {x} by A2,A5,TARSKI:def 1;
hence y in (A \ B) \/ {x} by XBOOLE_0:def 2;
suppose
A6: not x1 in dom (B --> x);
then A7: f.x1 = (id A).x1 by A3,FUNCT_4:def 1;
A8: not x1 in B by A6,FUNCOP_1:19;
x1 in dom (id A) by A3,A6,XBOOLE_0:def 2;
then A9: x1 in A by FUNCT_1:34;
then x1 in A \ B by A8,XBOOLE_0:def 4;
then x1 in (A \ B) \/ {x} by XBOOLE_0:def 2;
hence thesis by A2,A7,A9,FUNCT_1:35;
end;
let y be set;
assume
A10: y in (A \ B) \/ {x};
A11:
rng (B --> x)={x} by A1,FUNCOP_1:14;
A \ B c= A by XBOOLE_1:36;
then (id A).:(A \ B)=A \ B by Th13;
then (id A).:(dom(id A) \ B)=A \ B by FUNCT_1:34;
then (id A).:(dom(id A) \ dom( B --> x))=A \ B by FUNCOP_1:19;
hence y in rng((id A)+*(B --> x)) by A10,A11,Th12;
end;
theorem Th17:
for A,B,C,x being set holds
C c= A implies ((id A)+*(B --> x))"(C \ {x}) = C \ B \ {x}
proof
let A,B,C,x be set;
assume
A1: C c= A;
set f=((id A)+*(B --> x));
thus f"(C \ {x}) c= C \ B \ {x}
proof
let x1 be set;
assume x1 in f"(C \ {x});
then A2: x1 in dom f & f.x1 in (C \ {x}) by FUNCT_1:def 13;
A3: not x1 in B
proof
assume
A4: x1 in B;
A5: not f.x1 in {x} by A2,XBOOLE_0:def 4;
A6: x1 in dom(B --> x) by A4,FUNCOP_1:19;
then x1 in dom(id A) \/ dom(B --> x) by XBOOLE_0:def 2;
then f.x1=(B --> x).x1 by A6,FUNCT_4:def 1;
then f.x1=x by A4,FUNCOP_1:13;
hence contradiction by A5,TARSKI:def 1;
end;
then A7: not x1 in dom(B --> x) by FUNCOP_1:19;
x1 in A \/ B by A2,Th15;
then A8: x1 in A or x1 in B by XBOOLE_0:def 2;
then x1 in dom(id A) by A3,FUNCT_1:34;
then x1 in dom(id A) \/ dom(B --> x) by XBOOLE_0:def 2;
then f.x1 = (id A).x1 by A7,FUNCT_4:def 1;
then f.x1 = x1 by A3,A8,FUNCT_1:34;
then A9: x1 in C & not x1 in {x} by A2,XBOOLE_0:def 4;
then x1 in C \ B by A3,XBOOLE_0:def 4;
hence x1 in C \ B \ {x} by A9,XBOOLE_0:def 4;
end;
let x1 be set;
assume x1 in C \ B \ {x};
then x1 in C \ B & not x1 in {x} by XBOOLE_0:def 4;
then A10: x1 in C & not x1 in B & not x1 in {x} by XBOOLE_0:def 4;
then A11: x1 in A by A1;
A12:
not x1 in dom(B --> x) by A10,FUNCOP_1:19;
A13: x1 in C \ {x} by A10,XBOOLE_0:def 4;
x1 in dom(id A) by A11,FUNCT_1:34;
then A14: x1 in dom(id A) \/ dom(B --> x) by XBOOLE_0:def 2;
then A15: x1 in dom f by FUNCT_4:def 1;
f.x1 = (id A).x1 by A12,A14,FUNCT_4:def 1;
then f.x1 = x1 by A1,A10,FUNCT_1:34;
hence x1 in f"(C \ {x}) by A13,A15,FUNCT_1:def 13;
end;
theorem Th18:
for A,B,x being set holds
not x in A implies ((id A)+*(B --> x))"({x}) = B
proof
let A,B,x be set;
assume
A1: not x in A;
set f = (id A)+*(B --> x);
thus f"({x}) c= B
proof
let y be set;
assume y in f"({x});
then A2: y in dom f & f.y in {x} by FUNCT_1:def 13;
per cases;
suppose y in dom (B --> x);
hence y in B by FUNCOP_1:19;
suppose
A3: not y in dom (B --> x);
then A4: f.y = (id A).y by FUNCT_4:12;
A5: y in dom (B --> x) or y in dom (id A) by A2,FUNCT_4:13;
then y in A by A3,FUNCT_1:34;
then (id A).y = y by FUNCT_1:35;
then y = x by A2,A4,TARSKI:def 1;
hence y in B by A1,A3,A5,FUNCT_1:34;
end;
let y be set;
assume
A6: y in B;
then A7: y in dom (B-->x) by FUNCOP_1:19;
then f.y = (B-->x).y by FUNCT_4:14;
then f.y = x by A6,FUNCOP_1:13;
then A8: f.y in {x} by TARSKI:def 1;
y in dom f by A7,FUNCT_4:13;
hence y in f"({x}) by A8,FUNCT_1:def 13;
end;
theorem Th19:
for A,B,C,x being set holds
(C c= A & not x in A) implies ((id A)+*(B --> x))"(C \/ {x}) = C \/ B
proof
let A,B,C,x be set;
assume
A1: C c= A & not x in A;
set f = ((id A)+*(B --> x));
A2:
C \ {x} = C
proof
thus C \ {x} c= C by XBOOLE_1:36;
let y be set;
assume
A3: y in C;
not y in {x}
proof
assume y in {x};
then y = x by TARSKI:def 1;
hence contradiction by A1,A3;
end;
hence y in C\ {x} by A3,XBOOLE_0:def 4;
end;
f"({x})=B by A1,Th18;
then A4: f"(C \/ {x}) = f"(C) \/ B by RELAT_1:175;
C \ B \ {x} \/ B = C \/ B
proof
thus C \ B \ {x} \/ B c= C \/ B
proof
let y be set;
assume y in C \ B \ {x} \/ B;
then y in C \ B \ {x} or y in B by XBOOLE_0:def 2;
then y in C \ B or y in B by XBOOLE_0:def 4;
then y in C or y in B by XBOOLE_0:def 4;
hence y in C \/ B by XBOOLE_0:def 2;
end;
let y be set;
assume y in C \/ B;
then A5: y in (C \ B) \/ B by XBOOLE_1:39;
per cases by A5,XBOOLE_0:def 2;
suppose
A6: y in C \ B;
then A7: y in C by XBOOLE_0:def 4;
not y in {x}
proof
assume y in {x};
then x in C by A7,TARSKI:def 1;
hence contradiction by A1;
end;
then y in C \ B \ {x} by A6,XBOOLE_0:def 4;
hence y in (C \ B \ {x}) \/ B by XBOOLE_0:def 2;
suppose y in B;
hence y in (C \ B \ {x}) \/ B by XBOOLE_0:def 2;
end;
hence ((id A)+*(B --> x))"(C \/ {x}) = C \/ B by A1,A2,A4,Th17;
end;
theorem Th20:
for A,B,C,x being set holds
C c= A & not x in A implies ((id A)+*(B --> x))"(C \ {x}) = C \ B
proof
let A,B,C,x be set;
assume
A1: C c= A & not x in A;
not x in C \ B
proof
assume x in C \ B;
then x in C by XBOOLE_0:def 4;
hence contradiction by A1;
end;
then (C \ B) misses {x} by ZFMISC_1:56;
then C \ B \ {x} = C \ B by XBOOLE_1:83;
hence ((id A)+*(B --> x))"(C \ {x}) = C \ B by A1,Th17;
end;
Lm4:
for A,B,C,x being set holds
not x in A implies ((id A)+*(B --> x))"((A \ C) \ {x}) = A \ C \ B
proof
let A,B,C,x be set;
assume
A1: not x in A;
A \ C c= A by XBOOLE_1:36;
hence thesis by A1,Th20;
end;
begin
::
:: Convergent Sequences in Topological Spaces,
:: FIRST-COUNTABLE, SEQUENTIAL, FRECHET SPACES
::
definition
let T be non empty TopStruct;
attr T is first-countable means :Def1:
for x be Point of T ex B be Basis of x st B is countable;
end;
theorem Th21:
for M being non empty MetrSpace holds TopSpaceMetr(M) is first-countable
proof
let M be non empty MetrSpace;
let x be Point of TopSpaceMetr(M);
reconsider x' = x as Element of TopSpaceMetr(M);
reconsider x' as Element of M by TOPMETR:16;
reconsider x' as Point of M;
consider B being Basis of x such that
B={Ball(x',1/n) where n is Nat:n<>0} and
A1: B is countable and
ex f being Function of NAT,B st for n being set st n in NAT holds
ex n' being Nat st n=n' & f.n = Ball(x',1/(n'+1)) by Th11;
take B;
thus B is countable by A1;
end;
theorem
R^1 is first-countable by Th21,TOPMETR:def 7;
definition
cluster R^1 -> first-countable;
coherence by Th21,TOPMETR:def 7;
end;
definition
let T be TopStruct, S be sequence of T, x be Point of T;
pred S is_convergent_to x means :Def2:
for U1 being Subset of T st (U1 is open & x in U1)
ex n being Nat st for m being Nat st n <= m holds S.m in U1;
end;
theorem Th23:
for T being non empty TopStruct, x being Point of T, S being sequence of T
holds S = (NAT --> x) implies S is_convergent_to x
proof
let T be non empty TopStruct, x be Point of T, S be sequence of T;
assume
A1: S = (NAT --> x);
thus S is_convergent_to x
proof
let U1 be Subset of T;
assume
A2: U1 is open & x in U1;
take 0;
thus for m being Nat st 0 <= m holds S.m in U1 by A1,A2,FUNCOP_1:13;
end;
end;
definition
let T be TopStruct, S be sequence of T;
attr S is convergent means :Def3:
ex x being Point of T st S is_convergent_to x;
end;
definition
let T be non empty TopStruct, S be sequence of T;
func Lim S -> Subset of T means :Def4:
for x being Point of T holds
x in it iff S is_convergent_to x;
existence
proof
defpred P[Element of T] means S is_convergent_to $1;
{x where x is Element of T : P[x]}
is Subset of T from SubsetD; then
reconsider X={x where x is Point of T : P[x]}
as Subset of T;
take X;
let y be Point of T;
y in X iff ex x being Point of T st x=y & S is_convergent_to x;
hence thesis;
end;
uniqueness
proof
let A,B be Subset of T such that
A1: for x being Point of T holds x in A iff S is_convergent_to x and
A2: for x being Point of T holds x in B iff S is_convergent_to x;
for x being Point of T holds x in A iff x in B
proof
let x be Point of T;
x in A iff S is_convergent_to x by A1;
hence thesis by A2;
end;
hence A=B by SUBSET_1:8;
end;
end;
definition
let T be non empty TopStruct;
attr T is Frechet means :Def5:
for A being Subset of T,x being Point of T st x in Cl(A)
ex S being sequence of T st (rng S c= A & x in Lim S );
end;
definition
let T be non empty TopStruct;
attr T is sequential means
for A being Subset of T holds A is closed iff
for S being sequence of T st ( S is convergent & rng S c= A ) holds
Lim S c= A;
end;
theorem Th24:
for T being non empty TopSpace holds
T is first-countable implies T is Frechet
proof
let T be non empty TopSpace;
assume
A1: T is first-countable;
let A be Subset of T;
let x be Point of T such that
A2: x in Cl(A);
consider B being Basis of x such that
A3: B is countable by A1,Def1;
consider f being Function of NAT,B such that
A4: rng f = B by A3,WAYBEL12:4;
defpred P[set,set] means $2 in A /\ meet (f.:succ $1);
A5: for n being set st n in NAT ex y being set st y in the carrier of T &
P[n,y]
proof
let n be set;
assume n in NAT;
then reconsider n as Nat;
defpred P[Nat] means ex H being Subset of T st
H = meet (f.:succ $1) & H is open;
for n being Nat holds P[n]
proof
A6: P[0]
proof
0 in NAT;
then A7: 0 in dom f by FUNCT_2:def 1;
f.0 in B;
then consider H being Subset of T such that
A8: H = f.0;
reconsider H as Subset of T;
take H;
meet (f.:succ 0) = meet {f.0} by A7,CARD_5:1,FUNCT_1:117
.= H by A8,SETFAM_1:11;
hence thesis by A8,YELLOW_8:21;
end;
A9: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
given G being Subset of T such that
A10: G = meet (f.:succ n) and
A11: G is open;
n+1 in NAT;
then A12: n+1 in dom f by FUNCT_2:def 1;
f.(n+1) in B;
then consider H1 being Subset of T such that
A13: H1 = f.(n+1);
reconsider H1 as Subset of T;
A14: H1 is open by A13,YELLOW_8:21;
n in succ n & dom f = NAT by FUNCT_2:def 1,ORDINAL1:10;
then A15: f.n in f.:succ n by FUNCT_1:def 12;
consider H being Subset of T such that
A16: H = H1 /\ G;
reconsider H as Subset of T;
take H;
meet (f.:succ (n+1)) = meet (f.:({n+1} \/ (n+1))) by ORDINAL1:def 1
.= meet ((f.:({n+1} \/ (succ n)))) by CARD_1:52
.= meet ((f.:{n+1}) \/ (f.:succ n)) by RELAT_1:153
.= meet ({f.(n+1)} \/ (f.:succ n)) by A12,FUNCT_1:117
.= meet {f.(n+1)} /\ meet (f.:succ n) by A15,SETFAM_1:10
.= H by A10,A13,A16,SETFAM_1:11;
hence thesis by A11,A14,A16,TOPS_1:38;
end;
thus for n being Nat holds P[n] from Ind(A6,A9);
end;
then consider H being Subset of T such that
A17: H = meet (f.:succ n) & H is open;
n in succ n & dom f = NAT by FUNCT_2:def 1,ORDINAL1:10;
then A18: f.n in f.:succ n by FUNCT_1:def 12;
for G being set st G in (f.:succ n) holds x in G
proof
let G be set;
assume G in (f.:succ n);
then consider k be set such that
A19: k in dom f & k in succ n & G = f.k by FUNCT_1:def 12;
k in NAT by A19,FUNCT_2:def 1;
then A20: f.k in B by FUNCT_2:7;
then reconsider G1=G as Subset of T by A19;
reconsider G1 as Subset of T;
x in G1 by A19,A20,YELLOW_8:21;
hence thesis;
end;
then x in meet (f.:succ n) by A18,SETFAM_1:def 1;
then A meets meet (f.:succ n) by A2,A17,PRE_TOPC:def 13;
then consider y being set such that
A21:y in A /\ meet (f.:succ n) by XBOOLE_0:4;
take y;
y in A by A21,XBOOLE_0:def 3;
hence thesis by A21;
end;
consider S being Function such that
A22: dom S = NAT & rng S c= the carrier of T & for n being set st n in NAT
holds P[n,S.n] from NonUniqBoundFuncEx(A5);
A23: for m,n being Nat st n <= m holds
( A /\ meet (f.:succ m) ) c= A /\ meet (f.:succ n)
proof
let m,n be Nat;
assume
A24: n <= m;
n in succ n & dom f = NAT by FUNCT_2:def 1,ORDINAL1:10;
then A25: f.n in f.:succ n by FUNCT_1:def 12;
n + 1 <= m + 1 by A24,AXIOMS:24;
then n + 1 c= m + 1 by CARD_1:56;
then succ n c= m +1 by CARD_1:52;
then succ n c= succ m by CARD_1:52;
then f.:(succ n) c= f.:(succ m) by RELAT_1:156;
then meet (f.:succ m) c= meet (f.:succ n) by A25,SETFAM_1:7;
hence thesis by XBOOLE_1:26;
end;
A26: rng S c= A
proof
let y be set;
assume
y in rng S;
then consider a be set such that
A27: a in dom S & y = S.a by FUNCT_1:def 5;
y in A /\ meet (f.:succ a) by A22,A27;
hence thesis by XBOOLE_0:def 3;
end;
S is Function of NAT, the carrier of T by A22,FUNCT_2:def 1,RELSET_1:11;
then reconsider S as sequence of T by NORMSP_1:def 3;
S is_convergent_to x
proof
let U1 be Subset of T;
assume that
A28: U1 is open and
A29: x in U1;
reconsider U1 as Subset of T;
consider U2 being Subset of T such that
A30: U2 in B & U2 c= U1 by A28,A29,YELLOW_8:22;
consider n be set such that
A31: n in dom f & U2 = f.n by A4,A30,FUNCT_1:def 5;
reconsider n as Nat by A31,FUNCT_2:def 1;
for m being Nat st n <= m holds S.m in U1
proof
let m be Nat;
assume
n <= m;
then A32: ( A /\ meet (f.:succ m) ) c= A /\ meet (f.:succ n) by A23;
S.m in A /\ meet (f.:succ m) by A22;
then A33: S.m in meet (f.:succ n) by A32,XBOOLE_0:def
3;
n in succ n & dom f = NAT by FUNCT_2:def 1,ORDINAL1:10;
then f.n in f.:succ n by FUNCT_1:def 12;
then S.m in f.n by A33,SETFAM_1:def 1;
hence S.m in U1 by A30,A31;
end;
hence thesis;
end;
then x in Lim S by Def4;
hence ex S be sequence of T st (rng S c= A & x in Lim S ) by A26;
end;
definition
cluster first-countable -> Frechet (non empty TopSpace);
coherence by Th24;
end;
canceled;
theorem Th26:
for T being non empty TopSpace,A being Subset of T holds
A is closed implies
for S being sequence of T st S is convergent & rng S c= A holds Lim S c= A
proof
let T be non empty TopSpace,A be Subset of T;
assume
A1: A is closed;
let S be sequence of T such that
A2: S is convergent & rng S c= A;
thus Lim S c= A
proof
reconsider
L = Lim S as Subset of T;
reconsider A as Subset of T;
L c= A
proof
let y be set;
assume
A3: y in L;
then reconsider p=y as Point of T;
A4: S is_convergent_to p by A3,Def4;
for U1 being Subset of T st U1 is open
holds p in U1 implies A meets U1
proof
let U1 be Subset of T;
assume
A5: U1 is open;
assume
A6: p in U1;
reconsider U2 = U1 as Subset of T;
consider n being Nat such that
A7: for m being Nat st n <= m holds S.m in U2 by A4,A5,A6,Def2;
A8: S.n in U1 by A7;
dom S = NAT by FUNCT_2:def 1;
then S.n in rng S by FUNCT_1:def 5;
then S.n in A /\ U1 by A2,A8,XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 7;
end;
then p in Cl A by PRE_TOPC:def 13;
hence y in A by A1,PRE_TOPC:52;
end;
hence thesis;
end;
end;
theorem Th27:
for T being non empty TopSpace holds
(for A being Subset of T holds
(for S being sequence of T st S is convergent & rng S c= A holds Lim S c= A)
implies A is closed) implies
T is sequential
proof
let T be non empty TopSpace;
assume
A1: for A being Subset of T holds
(for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A) implies A is closed;
let A be Subset of T;
thus A is closed implies for S being sequence of T
st ( S is convergent & rng S c= A ) holds Lim S c= A by Th26;
assume for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A;
hence A is closed by A1;
end;
theorem Th28:
for T being non empty TopSpace holds T is Frechet implies T is sequential
proof
let T be non empty TopSpace;
assume
A1: T is Frechet;
for A being Subset of T holds
(for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A) implies A is closed
proof
let A be Subset of T;
assume
A2: for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A;
A3: A c= Cl(A) by PRE_TOPC:48;
Cl(A) c= A
proof
let x be set;
assume
A4: x in Cl(A);
then reconsider p=x as Point of T;
consider S being sequence of T such that
A5: rng S c= A and
A6: p in Lim S by A1,A4,Def5;
S is_convergent_to p by A6,Def4;
then S is convergent by Def3;
then Lim S c= A by A2,A5;
hence x in A by A6;
end;
then A = Cl(A) by A3,XBOOLE_0:def 10;
hence A is closed by PRE_TOPC:52;
end;
hence T is sequential by Th27;
end;
definition
cluster Frechet -> sequential (non empty TopSpace);
coherence by Th28;
end;
begin
::
:: Not (for T holds T is Frechet implies T is first-countable)
::
definition
func REAL? -> strict non empty TopSpace means :Def7:
the carrier of it = (REAL \ NAT) \/ {REAL} &
ex f being map of R^1, it st
f = (id REAL)+*(NAT --> REAL) &
for A being Subset of it holds A is closed iff f"A is closed;
existence
proof
reconsider X = (REAL \ NAT) \/ {REAL} as non empty set;
set f = (id REAL)+*(NAT --> REAL);
REAL \/ NAT = REAL by XBOOLE_1:12;
then A1: dom f = the carrier of R^1 by Th15,TOPMETR:24;
rng f c= (REAL \ NAT) \/ {REAL} by Th16;
then reconsider f as Function of the carrier of R^1,X by A1,FUNCT_2:4;
set O = {X\A where A is Subset of X: ex fA being Subset of R^1 st
fA = f"A & fA is closed};
O c= bool X
proof
let B be set;
assume B in O;
then consider A being Subset of X such that
A2: B = X\A & ex fA being Subset of R^1 st
fA = f"A & fA is closed;
X \ A c= X by XBOOLE_1:36;
hence B in bool X by A2;
end;
then reconsider O as Subset-Family of X by SETFAM_1:def 7;
set T = TopStruct(#X,O#);
reconsider f as map of R^1,T;
A3: for A being Subset of T holds A is closed iff f"A is closed
proof
let A be Subset of T;
thus A is closed implies f"A is closed
proof
assume A is closed;
then [#]T \ A is open by PRE_TOPC:def 6;
then [#]T \ A in the topology of T by PRE_TOPC:def 5;
then consider B being Subset of X such that
A4: X \ B = [#]T \ A & ex fA being Subset of R^1 st
fA = f"B & fA is closed;
[#]T \ B = [#]T \ A by A4,PRE_TOPC:12;
then B = [#]T \ ([#]T \ A) by PRE_TOPC:22;
hence f"A is closed by A4,PRE_TOPC:22;
end;
assume f"A is closed;
then X \ A in O;
then [#]T \ A in O by PRE_TOPC:12;
then [#]T \ A is open by PRE_TOPC:def 5;
hence A is closed by PRE_TOPC:def 6;
end;
then reconsider T as strict non empty TopSpace by Th6;
take T; thus the carrier of T = (REAL \ NAT) \/ {REAL};
reconsider f as map of R^1,T;
take f;
thus thesis by A3;
end;
uniqueness
proof
let X,Y be strict non empty TopSpace such that
A5:
the carrier of X = (REAL \ NAT) \/ {REAL} &
ex f being map of R^1, X st f = (id REAL)+*(NAT --> REAL) &
for A being Subset of X holds A is closed iff f"A is closed and
A6: the carrier of Y = (REAL \ NAT) \/ {REAL} &
ex f being map of R^1, Y st f = (id REAL)+*(NAT --> REAL) &
for A being Subset of Y holds A is closed iff f"A is closed;
the carrier of X = [#]Y by A5,A6,PRE_TOPC:12;
then A7: [#]X = [#]Y by PRE_TOPC:12;
consider f being map of R^1, X such that
A8: f = (id REAL)+*(NAT --> REAL) and
A9: for A being Subset of X holds A is closed iff f"A is closed by A5;
consider g being map of R^1, Y such that
A10: g = (id REAL)+*(NAT --> REAL) and
A11: for A being Subset of Y holds A is closed iff g"A is closed by A6;
the topology of X = the topology of Y
proof
thus
the topology of X c= the topology of Y
proof
let V be set;
assume
A12: V in the topology of X;
then reconsider V1=V as Subset of X;
reconsider V1 as Subset of X;
V1 is open by A12,PRE_TOPC:def 5;
then [#](X)\V1 is closed by Lm3;
then A13: g"([#]X\V1) is closed by A8,A9,A10;
reconsider V2=V as Subset of Y by A5,A6,A12;
reconsider V2 as Subset of Y;
[#]Y\V2 is closed by A7,A11,A13;
then V2 is open by Lm3;
hence V in the topology of Y by PRE_TOPC:def 5;
end;
thus the topology of Y c= the topology of X
proof
let V be set;
assume
A14: V in the topology of Y;
then reconsider V1=V as Subset of Y;
reconsider V1 as Subset of Y;
V1 is open by A14,PRE_TOPC:def 5;
then [#](Y)\V1 is closed by Lm3;
then A15: f"([#]Y\V1) is closed by A8,A10,A11;
reconsider V2=V as Subset of X by A5,A6,A14;
reconsider V2 as Subset of X;
[#]X\V2 is closed by A7,A9,A15;
then V2 is open by Lm3;
hence V in the topology of X by PRE_TOPC:def 5;
end;
end;
hence X=Y by A5,A6;
end;
end;
Lm5:
{REAL} c= the carrier of REAL?
proof
let x be set;
assume x in {REAL};
then x in (REAL\NAT) \/ {REAL} by XBOOLE_0:def 2;
hence x in the carrier of REAL? by Def7;
end;
canceled;
theorem Th30:
REAL is Point of REAL?
proof
REAL in {REAL} by TARSKI:def 1;
hence REAL is Point of REAL? by Lm5;
end;
theorem Th31:
for A being Subset of REAL? holds
A is open & REAL in A iff
ex O being Subset of R^1 st O is open & NAT c= O & A=(O\NAT) \/ {REAL}
proof
let A be Subset of REAL?;
consider f being map of R^1, REAL? such that
A1: f = (id REAL)+*(NAT --> REAL) and
A2: for A being Subset of REAL? holds A is closed iff f"A is closed by Def7;
thus A is open & REAL in A implies
ex O being Subset of R^1 st O is open & NAT c= O & A=(O\NAT) \/ {REAL}
proof
assume that
A3: A is open and
A4: REAL in A;
consider O being Subset of R^1 such that
A5: O=(f"(A`))`;
A` is closed by A3,TOPS_1:30;
then f"(A`) is closed by A2;
then A6: (f"(A`))` is open by TOPS_1:29;
not REAL in [#](REAL?) \ A by A4,XBOOLE_0:def 4;
then A7: not REAL in A` by PRE_TOPC:17;
A8:
A` = A` \ {REAL}
proof
thus A` c= A` \ {REAL}
proof
let x be set;
assume
A9: x in A`;
then not x in {REAL} by A7,TARSKI:def 1;
hence x in A` \ {REAL} by A9,XBOOLE_0:def 4;
end;
thus A` \ {REAL} c= A` by XBOOLE_1:36;
end;
A10:
REAL \ NAT c= REAL by XBOOLE_1:36;
A` c= the carrier of REAL?;
then A11: A` c= (REAL \ NAT) \/ {REAL} by Def7;
A12: A` c= REAL \ NAT
proof
let x be set;
assume
A13: x in A`;
then x in (REAL \ NAT) or x in {REAL} by A11,XBOOLE_0:def 2;
hence x in REAL\NAT by A7,A13,TARSKI:def 1;
end;
then A14: A` c= REAL by A10,XBOOLE_1:1;
not REAL in REAL;
then A15: ((id REAL)+*(NAT --> REAL))"(A` \ {REAL}) = A` \ NAT by A14,Th20;
NAT c= the carrier of R^1 by TOPMETR:24;
then A16: NAT c= [#](R^1) by PRE_TOPC:12;
O = [#](R^1) \ f"(A`) by A5,PRE_TOPC:17
.= ([#](R^1) \ A`) \/ (NAT /\ [#](R^1)) by A1,A8,A15,XBOOLE_1:52;
then A17: O = ([#](R^1) \ A`) \/ NAT by A16,XBOOLE_1:28;
then A18: NAT c= O by XBOOLE_1:7;
A19: NAT c= REAL \ A`
proof
let x be set;
assume
A20: x in NAT;
then not x in A` by A12,XBOOLE_0:def 4;
hence x in REAL \ A` by A20,XBOOLE_0:def 4;
end;
O = NAT \/ (REAL \ A`) by A17,PRE_TOPC:12,TOPMETR:24;
then A21: O = REAL \ A` by A19,XBOOLE_1:12;
A = A``
.= [#](REAL?) \ A` by PRE_TOPC:17
.= (the carrier of REAL?) \ A` by PRE_TOPC:12;
then A22: A = ((REAL \ NAT) \/ {REAL}) \ A` by Def7;
A = (REAL \ A`) \ NAT \/ {REAL}
proof
thus A c= (REAL \ A`) \ NAT \/ {REAL}
proof
let x be set;
assume x in A;
then x in (REAL \ NAT) \/ {REAL} & not x in A` by A22,XBOOLE_0:def 4;
then (x in (REAL \ NAT) or x in {REAL}) & not x in A` by XBOOLE_0:def 2;
then (x in REAL & not x in NAT & not x in A`) or x in {REAL}
by XBOOLE_0:def 4;
then (x in (REAL\ A`) & not x in NAT) or x in {REAL} by XBOOLE_0:def 4;
then (x in (REAL\ A`) \ NAT) or x in {REAL} by XBOOLE_0:def 4;
hence x in (REAL\ A`) \ NAT \/ {REAL} by XBOOLE_0:def 2;
end;
let x be set;
assume x in (REAL \ A`) \ NAT \/ {REAL};
then x in (REAL \ A`) \ NAT or x in {REAL} by XBOOLE_0:def 2;
then (x in (REAL \ A`) & not x in NAT) or (x in {REAL} & not x in A`)
by A7,TARSKI:def 1,
XBOOLE_0:def 4;
then (x in REAL & not x in A` & not x in NAT) or (x in {REAL} & not x in
A`)
by XBOOLE_0:def 4;
then (x in REAL\ NAT or x in {REAL}) & not x in A` by XBOOLE_0:def 4;
then x in (REAL \ NAT) \/ {REAL} & not x in A` by XBOOLE_0:def 2;
hence x in A by A22,XBOOLE_0:def 4;
end;
hence thesis by A5,A6,A18,A21;
end;
given O being Subset of R^1 such that
A23: O is open and
A24: NAT c= O and
A25: A=(O\NAT) \/ {REAL};
consider B being Subset of R^1 such that
A26: B = [#](R^1) \ O;
A27:
B is closed by A23,A26,Lm3;
f"(A`)=B
proof
A28: A` = [#](REAL?) \ A by PRE_TOPC:17
.= (the carrier of REAL?) \ A by PRE_TOPC:12
.= ((REAL \ NAT) \/ {REAL}) \ ((O\NAT) \/ {REAL}) by A25,Def7
.= ((REAL \ NAT) \((O\NAT) \/ {REAL})) \/ ({REAL} \ ({REAL} \/
(O\NAT))) by XBOOLE_1:42
.= ((REAL \ NAT) \((O\NAT) \/ {REAL})) \/ {} by XBOOLE_1:46
.= ((REAL \ NAT) \ (O\NAT)) \ {REAL} by XBOOLE_1:41
.= (REAL \ (NAT \/ (O \ NAT))) \ {REAL} by XBOOLE_1:41
.= (REAL \ (NAT \/ O )) \ {REAL} by XBOOLE_1:39
.= (REAL \ O) \ {REAL} by A24,XBOOLE_1:12;
not REAL in REAL;
then ((id REAL)+*(NAT --> REAL))"((REAL \ O) \ {REAL})= REAL \ O \ NAT
by Lm4;
then A29: f"((REAL \ O) \ {REAL}) = REAL \ (O \/ NAT) by A1,XBOOLE_1:41;
B = REAL \ O by A26,PRE_TOPC:12,TOPMETR:24;
hence thesis by A24,A28,A29,XBOOLE_1:12;
end;
then A` is closed by A2,A27;
then [#](REAL?) \ A is closed by PRE_TOPC:17;
hence A is open by Lm3;
REAL in {REAL} by TARSKI:def 1;
hence REAL in A by A25,XBOOLE_0:def 2;
end;
theorem Th32:
for A being set holds
A is Subset of REAL? & not REAL in A iff
A is Subset of R^1 & NAT /\ A = {}
proof
let A be set;
thus A is Subset of REAL? & not REAL in A implies
A is Subset of R^1 & NAT /\ A = {}
proof
assume
A1: A is Subset of REAL? & not REAL in A;
then A c= the carrier of REAL?;
then A2: A c= (REAL \ NAT) \/ {REAL} by Def7;
A c= REAL
proof
let x be set;
assume
A3: x in A;
then x in REAL \ NAT or x in {REAL} by A2,XBOOLE_0:def 2;
hence x in REAL by A1,A3,TARSKI:def 1,XBOOLE_0:def 4;
end;
hence A is Subset of R^1 by TOPMETR:24;
thus NAT /\ A = {}
proof
assume
A4: NAT /\ A <> {};
consider x being Element of NAT /\ A;
A5: x in NAT & x in A by A4,XBOOLE_0:def 3;
per cases by A2,A5,XBOOLE_0:def 2;
suppose x in REAL \ NAT;
hence contradiction by A5,XBOOLE_0:def 4;
suppose x in {REAL};
then x = REAL by TARSKI:def 1;
then REAL in REAL by A5;
hence contradiction;
end;
end;
assume
A6: A is Subset of R^1 & NAT /\ A = {};
A7:A c= REAL \ NAT
proof
let x be set;
assume
A8: x in A;
then not x in NAT by A6,XBOOLE_0:def 3;
hence x in REAL \ NAT by A6,A8,TOPMETR:24,XBOOLE_0:def 4;
end;
REAL \ NAT c= (REAL \ NAT) \/ {REAL} by XBOOLE_1:7;
then A c= (REAL \ NAT) \/ {REAL} by A7,XBOOLE_1:1;
then A is Subset of REAL? by Def7;
hence A is Subset of REAL?;
thus not REAL in A
proof
assume REAL in A;
then REAL in REAL by A6,TOPMETR:24;
hence contradiction;
end;
end;
theorem Th33:
for A being Subset of R^1,B being Subset of REAL? st A = B holds
NAT /\ A = {} & A is open iff not REAL in B & B is open
proof
let A be Subset of R^1,B be Subset of REAL?;
assume
A1: A = B;
consider f being map of R^1, REAL? such that
A2: f = (id REAL)+*(NAT --> REAL) and
A3: for A being Subset of REAL? holds A is closed iff f"A is closed by Def7;
A4:
(NAT /\ A = {} & not REAL in B) implies f"(B`) = A`
proof
assume
A5: NAT /\ A = {} & not REAL in B;
REAL in the carrier of REAL? by Th30;
then REAL in [#](REAL?) by PRE_TOPC:12;
then REAL in [#](REAL?) \ B by A5,XBOOLE_0:def 4;
then A6: REAL in B` by PRE_TOPC:17;
B` c= the carrier of REAL?;
then A7: B` c= (REAL \ NAT) \/ {REAL} by Def7;
A8: B` \ {REAL} c= REAL
proof
let x be set;
assume A9: x in B` \ {REAL};
then x in B` & not x in {REAL} by XBOOLE_0:def 4;
then x in (REAL \ NAT) or x in {REAL} by A7,XBOOLE_0:def 2;
hence x in REAL by A9,XBOOLE_0:def 4;
end;
A10:not REAL in REAL;
{REAL} c= B`
proof
let x be set;
assume x in {REAL};
hence x in B` by A6,TARSKI:def 1;
end;
then B` = (B`\{REAL}) \/ {REAL} by XBOOLE_1:45;
then A11: ((id REAL)+*(NAT --> REAL))"(B`)
= (B`\{REAL}) \/ NAT by A8,A10,Th19
.= (([#](REAL?) \ B)\{REAL}) \/ NAT by PRE_TOPC:17
.= (((the carrier of REAL?) \ B)\{REAL}) \/ NAT by PRE_TOPC:12
.= ((((REAL\NAT)\/{REAL})\A)\{REAL}) \/ NAT by A1,Def7;
REAL \ A = ((((REAL\NAT)\/{REAL})\A)\{REAL}) \/ NAT
proof
thus REAL \ A c= ((((REAL\NAT)\/{REAL})\A)\{REAL}) \/ NAT
proof
let x be set;
assume x in REAL\A;
then A12: x in REAL & not x in A by XBOOLE_0:def 4;
A13: not x in {REAL}
proof
assume x in {REAL};
then x = REAL by TARSKI:def 1;
hence contradiction by A12;
end;
per cases;
suppose x in NAT;
hence x in ((((REAL\NAT)\/{REAL})\A)\{REAL}) \/ NAT by XBOOLE_0:def 2;
suppose not x in NAT;
then x in REAL \ NAT by A12,XBOOLE_0:def 4;
then x in (REAL\NAT) \/ {REAL} by XBOOLE_0:def 2;
then x in ((REAL\NAT)\/{REAL})\A by A12,XBOOLE_0:def 4;
then x in (((REAL\NAT)\/{REAL})\A)\{REAL} by A13,XBOOLE_0:def 4;
hence x in ((((REAL\NAT)\/{REAL})\A)\{REAL}) \/ NAT by XBOOLE_0:def 2;
end;
let x be set;
assume A14: x in ((((REAL\NAT)\/{REAL})\A)\{REAL}) \/ NAT;
per cases by A14,XBOOLE_0:def 2;
suppose
A15: x in NAT;
then not x in A by A5,XBOOLE_0:def 3;
hence x in REAL \ A by A15,XBOOLE_0:def 4;
suppose A16: x in (((REAL\NAT)\/{REAL})\A)\{REAL};
then x in ((REAL\NAT)\/{REAL})\A & not x in {REAL} by XBOOLE_0:def 4
;
then A17: x in (REAL\NAT)\/{REAL} & not x in A by XBOOLE_0:def 4;
then x in REAL\NAT or x in {REAL} by XBOOLE_0:def 2;
then x in REAL by A16,XBOOLE_0:def 4;
hence x in REAL \ A by A17,XBOOLE_0:def 4;
end;
then [#](R^1) \ A = ((((REAL\NAT)\/ {REAL})\A)\{REAL}) \/
NAT by PRE_TOPC:12,TOPMETR:24;
hence f"(B`) = A` by A2,A11,PRE_TOPC:17;
end;
thus NAT /\ A = {} & A is open implies not REAL in B & B is open
proof
assume
A18: NAT /\ A = {} & A is open;
hence
not REAL in B by A1,Th32;
A` is closed by A18,TOPS_1:30;
then B` is closed by A1,A3,A4,A18,Th32;
hence B is open by TOPS_1:30;
end;
assume
A19: not REAL in B & B is open;
hence
NAT /\ A = {} by A1,Th32;
B` is closed by A19,TOPS_1:30;
then A` is closed by A1,A3,A4,A19,Th32;
hence A is open by TOPS_1:30;
end;
theorem Th34:
for A being Subset of REAL? st A = {REAL} holds A is closed
proof
let A be Subset of REAL?;
assume
A1: A = {REAL};
reconsider B = REAL \ NAT as Subset of R^1 by TOPMETR:24,
XBOOLE_1:36;
reconsider B as Subset of R^1;
A2:B is open
proof
reconsider N=NAT as Subset of R^1 by TOPMETR:24;
reconsider N as Subset of R^1;
A3: N is closed by Th10;
N` = [#](R^1) \ N by PRE_TOPC:17
.= B by PRE_TOPC:12,TOPMETR:24;
hence B is open by A3,TOPS_1:29;
end;
B misses NAT by XBOOLE_1:79;
then A4: B /\ NAT = {} by XBOOLE_0:def 7;
then reconsider C=B as Subset of REAL? by Th32;
A5: C is open by A2,A4,Th33;
(REAL\NAT) = ((REAL\NAT) \/ {REAL})\{REAL}
proof
thus (REAL\NAT) c= ((REAL\NAT) \/ {REAL})\{REAL}
proof
let x be set;
assume
A6: x in REAL \ NAT;
then A7: x in REAL by XBOOLE_0:def 4;
A8: not x in {REAL}
proof
assume x in {REAL};
then x = REAL by TARSKI:def 1;
hence contradiction by A7;
end;
x in (REAL \ NAT) \/ {REAL} by A6,XBOOLE_0:def 2;
hence x in ((REAL\NAT) \/ {REAL})\{REAL} by A8,XBOOLE_0:def 4;
end;
let x be set;
assume x in ((REAL\NAT) \/ {REAL})\{REAL};
then x in (REAL\NAT) \/ {REAL} & not x in {REAL} by XBOOLE_0:def 4;
hence x in REAL \ NAT by XBOOLE_0:def 2;
end;
then C = (the carrier of REAL?) \ A by A1,Def7
.= [#](REAL?) \ A by PRE_TOPC:12
.= A` by PRE_TOPC:17;
hence A is closed by A5,TOPS_1:29;
end;
theorem Th35:
REAL? is not first-countable
proof
assume
A1: REAL? is first-countable;
reconsider y = REAL as Point of REAL? by Th30;
consider B being Basis of y such that
A2: B is countable by A1,Def1;
consider h being Function of NAT,B such that
A3: rng h = B by A2,WAYBEL12:4;
defpred P[set,set] means
ex m being Nat st m=$1 & $2 in h.$1 /\ ]. m - 1/4 , m + 1/4 .[;
A4:for n being set st n in NAT
ex x being set st x in REAL \ NAT & P[n,x]
proof
let n be set;
assume
A5: n in NAT;
then n in dom h by FUNCT_2:def 1;
then A6: h.n in rng h by FUNCT_1:def 5;
then reconsider Bn=h.n as Subset of REAL? by A3;
reconsider Bn as Subset of REAL?;
Bn is open & y in Bn by A3,A6,YELLOW_8:21;
then consider An being Subset of R^1 such that
A7: An is open and
A8: NAT c= An and
A9: Bn = (An \ NAT) \/ {REAL} by Th31;
reconsider An'=An as Subset of TopSpaceMetr(RealSpace) by TOPMETR:def 7;
reconsider m = n as Nat by A5;
reconsider m'=m as Point of RealSpace by METRIC_1:def 14;
A10: Ball(m',1/4) = ]. m - 1/4 , m + 1/4 .[ by Th7;
dist(m',m')=0 by METRIC_1:1;
then m' in Ball(m',1/4) by METRIC_1:12;
then A11: n in An /\ Ball(m',1/4) by A5,A8,XBOOLE_0:def 3;
Ball(m',1/4) c= the carrier of RealSpace;
then Ball(m',1/4) c= the carrier of TopSpaceMetr(RealSpace) by TOPMETR:16;
then reconsider Kn = Ball(m',1/4) as
Subset of TopSpaceMetr(RealSpace);
Kn is open by TOPMETR:21;
then An' /\ Kn is open by A7,TOPMETR:def 7,TOPS_1:38;
then consider r being real number such that
A12: r>0 and
A13: Ball(m',r) c= An /\ Kn by A11,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
A14: r < 1
proof
assume r>=1;
then 1/2 < r by AXIOMS:22;
then -r < -(1/2) by REAL_1:50;
then -r + m < -(1/2) + m by REAL_1:53;
then m - r < m + -(1/2) by XCMPLX_0:def 8;
then A15: m - r < m - 1/2 by XCMPLX_0:def 8;
-(1/2) < r by A12,AXIOMS:22;
then -(1/2) + m < r + m by REAL_1:53;
then m - 1/2 < m + r by XCMPLX_0:def 8;
then m - 1/2 in {a where a is Real:m-r<a & a<m+r} by A15;
then m - 1/2 in ].m-r,m+r.[ by RCOMP_1:def 2;
then m - 1/2 in Ball(m',r) by A12,Th7;
then m - 1/2 in Kn by A13,XBOOLE_0:def 3;
then m - 1/2 in ]. m - 1/4,m+1/4.[ by Th7;
then m - 1/2 in {a where a is Real: m - 1/4 < a & a < m + 1/4 }
by RCOMP_1:def 2;
then consider a being Real such that
A16: a= m - 1/2 & m - 1/4 < a & a < m + 1/4;
m + -(1/4) < m - 1/2 by A16,XCMPLX_0:def 8;
then m + -(1/4) < m + -(1/2) by XCMPLX_0:def 8;
hence contradiction by AXIOMS:24;
end;
m < m + r by A12,REAL_1:69;
then m - r < m by REAL_1:84;
then consider x being real number such that
A17: m - r < x and
A18: x < m by REAL_1:75;
reconsider x as Real by XREAL_0:def 1;
take x;
x + 0 < m + r by A12,A18,REAL_1:67;
then x in {a where a is Real : m - r < a & a < m + r} by A17;
then x in ].m - r,m + r.[ by RCOMP_1:def 2;
then A19: x in Ball(m',r) by A12,Th7;
then A20: x in ]. m - 1/4 , m + 1/4 .[ by A10,A13,XBOOLE_0:def 3;
A21: not x in NAT
proof
assume x in NAT;
then reconsider x as Nat;
per cases by REAL_1:def 5;
suppose x = m;
hence contradiction by A18;
suppose x > m;
hence contradiction by A18;
suppose x < m;
then A22: m >= x + 1 by NAT_1:38;
m < x + r by A17,REAL_1:84;
then m - x < r by REAL_1:84;
then m - x < 1 by A14,AXIOMS:22;
hence contradiction by A22,REAL_1:84;
end;
x in An by A13,A19,XBOOLE_0:def 3;
then x in An \ NAT by A21,XBOOLE_0:def 4;
then A23: x in Bn by A9,XBOOLE_0:def 2;
thus x in REAL \ NAT by A21,XBOOLE_0:def 4;
take m;
m=n & x in h.n /\ ]. m - 1/4 , m + 1/4 .[ by A20,A23,XBOOLE_0:def 3;
hence thesis;
end;
consider S being Function such that
A24: dom S = NAT and
A25: rng S c= REAL \ NAT and
A26: for n being set st n in NAT holds P[n,S.n]
from NonUniqBoundFuncEx(A4);
REAL \ NAT c= REAL by XBOOLE_1:36;
then rng S c= REAL by A25,XBOOLE_1:1;
then S is Function of NAT, the carrier of R^1 by A24,FUNCT_2:4,TOPMETR:24;
then reconsider S as sequence of R^1 by NORMSP_1:def 3;
A27:
for n being Nat holds S.n in ]. n - 1/4 , n + 1/4 .[
proof
let n be Nat;
consider m being Nat such that
A28: m=n and
A29: S.n in h.n /\ ]. m - 1/4 , m + 1/4 .[ by A26;
thus S.n in ]. n - 1/4 , n + 1/4 .[ by A28,A29,XBOOLE_0:def 3;
end;
reconsider O=rng S as Subset of R^1;
O is closed by A27,Th9;
then [#](R^1)\O is open by PRE_TOPC:def 6;
then A30: O` is open by PRE_TOPC:17;
A31:
NAT c= O`
proof
let x be set;
assume
A32: x in NAT;
then x in the carrier of R^1 by TOPMETR:24;
then A33: x in [#](R^1) by PRE_TOPC:12;
not x in rng S by A25,A32,XBOOLE_0:def 4;
then x in [#](R^1) \ O by A33,XBOOLE_0:def 4;
hence x in O` by PRE_TOPC:17;
end;
set A = (O` \ NAT) \/ {REAL};
A c= (REAL \ NAT) \/ {REAL}
proof
let x be set;
assume x in A;
then x in (O` \ NAT) or x in {REAL} by XBOOLE_0:def 2;
then (x in O` & not x in NAT) or x in {REAL} by XBOOLE_0:def 4;
then (x in REAL \ NAT) or x in {REAL} by TOPMETR:24,XBOOLE_0:def 4;
hence x in (REAL \ NAT) \/ {REAL} by XBOOLE_0:def 2;
end;
then reconsider A as Subset of REAL? by Def7;
reconsider A as Subset of REAL?;
A is open & REAL in A by A30,A31,Th31;
then consider V being Subset of REAL? such that
A34: V in B & V c= A by YELLOW_8:22;
A35:
for n being Nat ex x being set st x in h.n & not (x in A)
proof
let n be Nat;
consider xn being set such that
A36: xn=S.n;
take xn;
A37: ex m being Nat st m=n & S.n in h.n /\ ]. m - 1/4 , m + 1/4 .[ by A26;
A38: S.n in rng S by A24,FUNCT_1:def 5;
then not xn in [#](R^1) \ O by A36,XBOOLE_0:def 4;
then A39: not xn in O` by PRE_TOPC:17;
not xn = REAL
proof
assume xn = REAL;
then REAL in REAL by A25,A36,A38,XBOOLE_0:def 4;
hence contradiction;
end;
then not xn in (O` \ NAT) & not xn in {REAL} by A39,TARSKI:def 1,XBOOLE_0:
def 4;
hence xn in h.n & not (xn in A) by A36,A37,XBOOLE_0:def 2,def 3;
end;
consider n1 being set such that
A40: n1 in dom h and
A41: V = h.n1 by A3,A34,FUNCT_1:def 5;
reconsider n=n1 as Nat by A40,FUNCT_2:def 1;
consider x being set such that
A42: x in h.n & not (x in A) by A35;
thus contradiction by A34,A41,A42;
end;
theorem Th36:
REAL? is Frechet
proof
let A be Subset of REAL?,x be Point of REAL?;
assume
A1: x in Cl(A);
x in the carrier of REAL?;
then x in (REAL \ NAT) \/ {REAL} by Def7;
then A2: x in (REAL \ NAT) or x in {REAL} by XBOOLE_0:def 2;
per cases by A2,TARSKI:def 1;
suppose
A3: x in (REAL \ NAT);
then A4: x in REAL by XBOOLE_0:def 4;
reconsider x'=x as Point of R^1 by A3,TOPMETR:24,XBOOLE_0:def 4;
A c= the carrier of REAL?;
then A5: A c= REAL \ NAT \/ {REAL} by Def7;
A\{REAL} c= REAL
proof
let a be set;
assume a in A\{REAL};
then a in A & not a in{REAL} by XBOOLE_0:def 4;
then (a in REAL\NAT or a in {REAL}) & not a in {REAL} by A5,XBOOLE_0:def 2
;
hence a in REAL by XBOOLE_0:def 4;
end;
then reconsider A' = A\{REAL} as Subset of R^1 by TOPMETR:24;
reconsider A' as Subset of R^1;
for B' being Subset of R^1 st B' is open holds
x' in B' implies A' meets B'
proof
let B' be Subset of R^1;
assume
A6: B' is open;
assume
A7: x' in B';
reconsider B1=B' as Subset of R^1;
reconsider C=NAT as Subset of R^1 by TOPMETR:24;
reconsider C as Subset of R^1;
C is closed by Th10;
then A8: B1 \ C is open by A6,Th4;
(B' \ NAT) misses NAT by XBOOLE_1:79;
then A9: (B' \ NAT) /\ NAT = {} by XBOOLE_0:def 7;
then reconsider D=B1 \ C as Subset of REAL? by Th32;
A10:D is open by A8,A9,Th33;
not x' in NAT by A3,XBOOLE_0:def 4;
then A11: x' in B' \ NAT by A7,XBOOLE_0:def 4;
reconsider D as Subset of REAL?;
A meets D by A1,A10,A11,PRE_TOPC:def 13;
then A12: A /\ D <> {} by XBOOLE_0:def 7;
A' /\ B' <> {}
proof
consider a being Element of A /\ D;
A13: a in D by A12,XBOOLE_0:def 3;
then A14: a in B' by XBOOLE_0:def 4;
A15: a in REAL by A13,TOPMETR:24;
A16: not a in {REAL}
proof
assume a in {REAL};
then a = REAL by TARSKI:def 1;
hence contradiction by A15;
end;
a in A by A12,XBOOLE_0:def 3;
then a in A \ {REAL} by A16,XBOOLE_0:def 4;
hence A' /\ B' <> {} by A14,XBOOLE_0:def 3;
end;
hence A' meets B' by XBOOLE_0:def 7;
end;
then x' in Cl(A') by PRE_TOPC:def 13;
then consider S' being sequence of R^1 such that
A17: rng S' c= A' and
A18: x' in Lim S' by Def5;
A19: S' is_convergent_to x' by A18,Def4;
A20:
rng S' c= A
proof
let a be set;
assume a in rng S';
hence a in A by A17,XBOOLE_0:def 4;
end;
then rng S' c= the carrier of REAL? by XBOOLE_1:1;
then reconsider S=S' as sequence of REAL? by Th2;
take S;
thus rng S c= A by A20;
S is_convergent_to x
proof
let V be Subset of REAL?;
assume
A21: V is open & x in V;
reconsider C={REAL} as Subset of REAL? by Lm5;
reconsider C as Subset of REAL?;
C is closed by Th34;
then A22: V \ C is open by A21,Th4;
REAL in {REAL} by TARSKI:def 1;
then A23: not REAL in V \ {REAL} by XBOOLE_0:def 4;
then reconsider V' = V \ C as Subset of R^1 by Th32;
A24: V' is open by A22,A23,Th33;
not x in C
proof
assume x in C;
then x = REAL by TARSKI:def 1;
hence contradiction by A4;
end;
then x in V \ C by A21,XBOOLE_0:def 4;
then consider n being Nat such that
A25: for m being Nat st n <= m holds S'.m in V' by A19,A24,Def2;
take n;
thus for m being Nat st n <= m holds S.m in V
proof
let m be Nat;
assume n <= m;
then S'.m in V' by A25;
hence S.m in V by XBOOLE_0:def 4;
end;
end;
hence x in Lim S by Def4;
suppose
A26: x = REAL & x in A;
A27: rng (NAT --> x) = {x} by FUNCOP_1:14;
dom (NAT --> x) = NAT by FUNCOP_1:19;
then (NAT --> x) is Function of NAT,the carrier of REAL? by A27,FUNCT_2:4;
then reconsider S=(NAT --> x) as sequence of REAL? by NORMSP_1:def 3;
take S;
{x} c= A by A26,ZFMISC_1:37;
hence rng S c= A by FUNCOP_1:14;
S is_convergent_to x by Th23;
hence x in Lim S by Def4;
suppose
A28: x = REAL & not x in A;
then reconsider A'=A as Subset of R^1 by Th32;
ex k being Point of R^1 st k in NAT & ex S' being sequence of R^1 st
rng S' c= A' & S' is_convergent_to k
proof
assume
A29: not (ex k being Point of R^1 st k in NAT & ex S' being sequence of
R^1 st
rng S' c= A' & S' is_convergent_to k);
defpred P[set,set] means
$1 in $2 & $2 in the topology of R^1 & $2 /\ A' = {};
A30: for k being set st k in NAT ex U1 being set st P[k,U1]
proof
given k being set such that
A31: k in NAT and
A32: for U1 being set holds
(k in U1 & U1 in the topology of R^1) implies not U1 /\ A' = {};
reconsider k as Point of R^1 by A31,TOPMETR:24;
reconsider k''=k as Point of TopSpaceMetr(RealSpace) by TOPMETR:def 7;
reconsider k'=k'' as Point of RealSpace by TOPMETR:16;
consider Bs being Basis of k'' such that
A33: Bs={Ball(k',1/n) where n is Nat:n<>0} and
Bs is countable and
A34: ex f being Function of NAT,Bs st for n being set st n in NAT holds
ex n' being Nat st n=n' & f.n = Ball(k',1/(n'+1)) by Th11;
consider h being Function of NAT,Bs such that
A35: for n being set st n in NAT holds
ex n' being Nat st n=n' & h.n = Ball(k',1/(n'+1)) by A34;
defpred P[set,set] means $2 in h.$1 /\ A';
A36: for n being set st n in NAT
ex z being set st z in the carrier of R^1 & P[n,z]
proof
let n be set;
assume
n in NAT;
then consider n' being Nat such that
n=n' and
A37: h.n=Ball(k',1/(n'+1)) by A35;
A38: h.n in Bs by A33,A37;
A39: Bs c= the topology of TopSpaceMetr(RealSpace) by YELLOW_8:def 2;
reconsider H=h.n as
Subset of TopSpaceMetr(RealSpace) by A38;
reconsider H as Subset of TopSpaceMetr(RealSpace);
k in H by A38,YELLOW_8:21;
then A40: H /\ A' <> {} by A32,A38,A39,TOPMETR:def 7;
consider z being Element of H /\ A';
A41: z in H by A40,XBOOLE_0:def 3;
take z;
thus z in the carrier of R^1 & z in h.n /\ A' by A40,A41,TOPMETR:def 7
;
end;
consider S' being Function such that
A42: dom S' = NAT & rng S' c= the carrier of R^1 and
A43: for n being set st n in NAT holds P[n,S'.n]
from NonUniqBoundFuncEx(A36);
reconsider S' as Function of NAT,the carrier of R^1 by A42,FUNCT_2:4;
reconsider S' as sequence of R^1 by NORMSP_1:def 3;
A44: rng S' c= A'
proof
let z be set;
assume z in rng S';
then consider z' being set such that
A45: z' in dom S' and
A46: z = S'.z' by FUNCT_1:def 5;
S'.z' in h.z' /\ A' by A42,A43,A45;
hence z in A' by A46,XBOOLE_0:def 3;
end;
S' is_convergent_to k
proof
let U1 be Subset of R^1;
assume
A47: U1 is open & k in U1;
reconsider U2=U1 as Subset of TopSpaceMetr(RealSpace)
by TOPMETR:def 7;
consider r being real number such that
A48: r > 0 and
A49: Ball(k',r) c= U2 by A47,TOPMETR:22,def 7;
reconsider r as Real by XREAL_0:def 1;
consider n being Nat such that
A50: 1/n < r and
A51: n <> 0 by A48,Lm2;
take n;
thus for m being Nat st n <= m holds S'.m in U1
proof
let m be Nat;
assume
n <= m;
then A52: n < m + 1 by NAT_1:38;
n > 0 by A51,NAT_1:19;
then 1/(m+1) < 1/n by A52,REAL_2:151;
then 1/(m+1) < r by A50,AXIOMS:22;
then Ball(k',1/(m+1)) c= Ball(k',r) by PCOMPS_1:1;
then A53: Ball(k',1/(m+1)) c= U2 by A49,XBOOLE_1:1;
consider m' being Nat such that
A54: m=m' and
A55: h.m = Ball(k',1/(m'+1)) by A35;
S'.m in h.m /\ A' by A43;
then S'.m in h.m by XBOOLE_0:def 3;
hence S'.m in U1 by A53,A54,A55;
end;
end;
hence contradiction by A29,A31,A44;
end;
consider g being Function such that
A56: dom g =NAT and
A57: for k being set st k in NAT holds P[k,g.k]
from NonUniqFuncEx(A30);
rng g c= bool the carrier of R^1
proof
let z be set;
assume z in rng g;
then consider k being set such that
A58: k in dom g and
A59: z=g.k by FUNCT_1:def 5;
g.k in the topology of R^1 by A56,A57,A58;
hence z in bool the carrier of R^1 by A59;
end;
then rng g is Subset-Family of R^1 by SETFAM_1:def 7;
then reconsider F = rng g as Subset-Family of R^1;
F is open
proof
let O be Subset of R^1;
assume O in F;
then consider k being set such that
A60: k in dom g and
A61: O=g.k by FUNCT_1:def 5;
g.k in the topology of R^1 by A56,A57,A60;
hence O is open by A61,PRE_TOPC:def 5;
end;
then A62: union F is open by TOPS_2:26;
A63: NAT c= union F
proof
let k be set;
assume
A64: k in NAT;
then A65: k in g.k by A57;
g.k in rng g by A56,A64,FUNCT_1:def 5;
hence k in union F by A65,TARSKI:def 4;
end;
(union F)\NAT c= REAL \ NAT by TOPMETR:24,XBOOLE_1:33;
then ((union F)\NAT) \/ {REAL} c= (REAL \ NAT) \/ {REAL} by XBOOLE_1:9;
then reconsider B = ((union F)\NAT) \/ {REAL} as
Subset of REAL? by Def7;
reconsider B as Subset of REAL?;
B is open & REAL in B by A62,A63,Th31;
then A66: A meets B by A1,A28,PRE_TOPC:def 13;
B /\ A = {}
proof
assume
A67: B /\ A <> {};
consider z being Element of B /\ A;
A68: z in B & z in A by A67,XBOOLE_0:def 3;
per cases by A68,XBOOLE_0:def 2;
suppose z in (union F)\NAT;
then z in union F by XBOOLE_0:def 4;
then consider C being set such that
A69: z in C and
A70: C in F by TARSKI:def 4;
consider l being set such that
A71: l in dom g and
A72: C = g.l by A70,FUNCT_1:def 5;
g.l /\ A = {} by A56,A57,A71;
hence contradiction by A68,A69,A72,XBOOLE_0:def 3;
suppose z in {REAL};
then z = REAL by TARSKI:def 1;
hence contradiction by A28,A67,XBOOLE_0:def 3;
end;
hence contradiction by A66,XBOOLE_0:def 7;
end;
then consider k being Point of R^1 such that
A73: k in NAT and
A74: ex S' being sequence of R^1 st rng S' c= A' & S' is_convergent_to k;
consider S' being sequence of R^1 such that
A75: rng S' c= A' and
A76: S' is_convergent_to k by A74;
rng S' c= the carrier of REAL? by A75,XBOOLE_1:1;
then reconsider S = S' as sequence of REAL? by Th2;
take S;
thus rng S c= A by A75;
S is_convergent_to x
proof
let U1 be Subset of REAL?;
assume (U1 is open & x in U1);
then consider O being Subset of R^1 such that
A77: O is open and
A78: NAT c= O and
A79: U1=(O\NAT) \/ {REAL} by A28,Th31;
consider n being Nat such that
A80: for m being Nat st n <= m holds S'.m in O by A73,A76,A77,A78,Def2;
take n;
thus for m being Nat st n <= m holds S.m in U1
proof
let m be Nat;
assume n <= m;
then A81: S'.m in O by A80;
m in NAT;
then m in dom S' by NORMSP_1:17;
then S'.m in rng S' by FUNCT_1:def 5;
then S'.m in A' by A75;
then S'.m in the carrier of REAL?;
then S'.m in (REAL \ NAT) \/ {REAL} by Def7;
then A82: S'.m in (REAL \ NAT) or S'.m in {REAL} by XBOOLE_0:def 2;
S'.m <> REAL
proof
assume
A83: S'.m = REAL;
S'.m in REAL by TOPMETR:24;
hence contradiction by A83;
end;
then not S'.m in NAT by A82,TARSKI:def 1,XBOOLE_0:def 4;
then S'.m in O \ NAT by A81,XBOOLE_0:def 4;
hence S.m in U1 by A79,XBOOLE_0:def 2;
end;
end;
hence x in Lim S by Def4;
end;
theorem
not (for T being non empty TopSpace holds
T is Frechet implies T is first-countable) by Th35,Th36;
begin
::
:: Auxiliary theorems
::
canceled 2;
theorem
for r being Real st r>0 ex n being Nat st (1/n < r & n<>0) by Lm2;