:: First-countable, Sequential, and { F } rechet Spaces
:: by Bart{\l}omiej Skorulski
::
:: Received May 13, 1998
:: Copyright (c) 1998-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, REAL_1, XXREAL_0, CARD_1, SUBSET_1, ARYTM_3, XBOOLE_0,
STRUCT_0, NAT_1, RELAT_1, TARSKI, PRE_TOPC, RLVECT_3, RCOMP_1, SETFAM_1,
FUNCT_1, ZFMISC_1, METRIC_1, XXREAL_1, ARYTM_1, COMPLEX1, TOPMETR,
PCOMPS_1, ORDINAL1, CARD_3, FUNCT_4, FUNCOP_1, SEQ_2, PARTFUN1, FRECHET,
YELLOW_8;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
XREAL_0, COMPLEX1, REAL_1, NAT_1, SETFAM_1, RELAT_1, FUNCT_1, PARTFUN1,
RELSET_1, FUNCT_2, BINOP_1, FUNCOP_1, STRUCT_0, CARD_3, FUNCT_4, RCOMP_1,
PRE_TOPC, TOPS_2, METRIC_1, PCOMPS_1, TOPMETR, YELLOW_8, XXREAL_0;
constructors FUNCT_4, REAL_1, NAT_1, MEMBERED, COMPLEX1, RCOMP_1, PCOMPS_1,
FUNCOP_1, CARD_3, TOPS_2, TOPMETR, YELLOW_8, BINOP_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, NUMBERS,
XXREAL_0, XREAL_0, NAT_1, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1,
PCOMPS_1, TOPMETR, RELSET_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, TOPS_2, XBOOLE_0;
equalities SUBSET_1, STRUCT_0, RELAT_1, XCMPLX_0, TOPMETR, ORDINAL1;
expansions TARSKI, TOPS_2, XBOOLE_0;
theorems TARSKI, ZFMISC_1, SUBSET_1, SETFAM_1, PRE_TOPC, FUNCT_1, FUNCT_2,
FUNCT_4, FUNCOP_1, NORMSP_1, NAT_1, ORDINAL1, RELAT_1, YELLOW_8, TOPS_1,
TOPS_2, TOPMETR, RCOMP_1, METRIC_1, PCOMPS_1, GOBOARD6, RELSET_1,
XREAL_0, XBOOLE_0, XBOOLE_1, SEQ_4, COMPLEX1, XREAL_1, XXREAL_0, CARD_3,
NUMBERS;
schemes DOMAIN_1, CLASSES1, NAT_1, CARD_4, FUNCT_1;
begin
Lm1: 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:3;
take n;
1/(1/r) > 1/n by A1,A2,XREAL_1:88;
hence 1/n < r;
thus thesis by A1,A2;
end;
::
:: Preliminaries
::
theorem
for T being non empty 1-sorted,S being sequence of T holds
rng S is Subset of T;
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;
A1: dom S = NAT by FUNCT_2:def 1;
assume rng S c= the carrier of T2;
hence thesis by A1,FUNCT_2:2;
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: the carrier of T in the topology of T by PRE_TOPC:def 1;
set U1=[#]T;
reconsider T as non empty TopStruct;
U1 is open by A1,PRE_TOPC:def 2;
then ex U2 be Subset of T st U2 in B & U2 c= U1 by YELLOW_8:13;
hence thesis;
end;
registration
let T be non empty TopSpace;
let x be Point of T;
cluster -> non empty for Basis of x;
coherence by Th3;
end;
Lm2: 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:3;
hence thesis by PRE_TOPC:def 3;
end;
assume [#]T \ A is closed;
then [#](T) \ ([#](T) \ A) is open by PRE_TOPC:def 3;
hence thesis by PRE_TOPC:3;
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 that
A1: A is open and
A2: B is closed;
[#](T)\B is open by A2,PRE_TOPC:def 3;
then A /\ ([#](T)\B) is open by A1,TOPS_1:11;
then
A3: A /\ [#](T) \ A /\ B is open by XBOOLE_1:50;
A /\ [#](T) = A by XBOOLE_1:28;
hence thesis by A3,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 and
A2: [#]T is closed and
A3: for A,B being Subset of T st A is closed & B is closed holds A \/ B
is closed and
A4: for F being Subset-Family of T st F is closed holds meet F is closed;
A5: 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
A6: A in the topology of T and
A7: B in the topology of T;
reconsider A, B as Subset of T;
B is open by A7,PRE_TOPC:def 2;
then
A8: [#]T \ B is closed by Lm2;
A is open by A6,PRE_TOPC:def 2;
then [#]T \ A is closed by Lm2;
then ([#]T \ A) \/ ([#]T \ B) is closed by A3,A8;
then [#]T \ (A /\ B) is closed by XBOOLE_1:54;
then (A /\ B) is open by Lm2;
hence thesis by PRE_TOPC:def 2;
end;
A9: 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 G9 = G as Subset-Family of T;
assume
A10: G c= the topology of T;
per cases;
suppose
A11: G = {};
[#]T \ {}T = [#]T;
then {}T is open by A2,Lm2;
hence thesis by A11,PRE_TOPC:def 2,ZFMISC_1:2;
end;
suppose
A12: G<>{};
reconsider CG = COMPLEMENT(G) as Subset-Family of T;
A13: for A being Subset of T holds A in G implies [#]T \ A is closed
by A10,Lm2,PRE_TOPC:def 2;
COMPLEMENT(G) is closed
proof
let A be Subset of T;
assume A in COMPLEMENT(G);
then A` in G9 by SETFAM_1:def 7;
then [#]T \ A` is closed by A13;
hence thesis by PRE_TOPC:3;
end;
then meet CG is closed by A4;
then (union G9)` is closed by A12,TOPS_2:6;
then [#]T \ union G is closed;
then union G is open by Lm2;
hence thesis by PRE_TOPC:def 2;
end;
end;
[#]T \ {}T is open by A1,PRE_TOPC:def 3;
then the carrier of T in the topology of T by PRE_TOPC:def 2;
hence thesis by A9,A5,PRE_TOPC:def 1;
end;
theorem Th6:
for T being TopSpace, S being non empty TopStruct, f being
Function 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 Function of T,S;
assume
A1: for A being Subset of S holds A is closed iff f"A is closed;
A2: 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:9;
then f"(A \/ B) is closed by RELAT_1:140;
hence thesis by A1;
end;
{}T is closed & f"{}={};
then
A3: {}S is closed by A1;
A4: 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
A5: F is closed;
per cases;
suppose
F = {}S;
hence thesis by A3,SETFAM_1:def 1;
end;
suppose
A6: F <> {};
set F1 = {f"A where A is Subset of S : A in F};
ex A being set st A in F
proof
set A = the Element of F;
take A;
thus thesis by A6;
end;
then consider A being Subset of S such that
A7: A in F;
reconsider A as Subset of S;
A8: f"A in F1 by A7;
F1 c= bool the carrier of T
proof
let B be object;
assume B in F1;
then ex A being Subset of S st B=f"A & A in F;
hence thesis;
end;
then reconsider F1 as Subset-Family of T;
A9: meet(F1) c= f"(meet F)
proof
let x be object;
assume
A10: x in meet(F1);
for A be set st A in F holds f.x in A
proof
let A be set;
assume
A11: A in F;
then reconsider A as Subset of S;
f"A in F1 by A11;
then x in f"A by A10,SETFAM_1:def 1;
hence thesis by FUNCT_1:def 7;
end;
then
A12: f.x in meet F by A6,SETFAM_1:def 1;
x in the carrier of T by A10;
then x in dom f by FUNCT_2:def 1;
hence thesis by A12,FUNCT_1:def 7;
end;
F1 is closed
proof
let B be Subset of T;
assume B in F1;
then consider A being Subset of S such that
A13: f"A = B and
A14: A in F;
A is closed by A5,A14;
hence thesis by A1,A13;
end;
then
A15: meet F1 is closed by TOPS_2:22;
f"(meet F) c= meet(F1)
proof
let x be object;
assume
A16: x in f"(meet F);
then
A17: f.x in meet F by FUNCT_1:def 7;
A18: x in dom f by A16,FUNCT_1:def 7;
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
A19: B = f"A and
A20: A in F;
f.x in A by A17,A20,SETFAM_1:def 1;
hence thesis by A18,A19,FUNCT_1:def 7;
end;
hence thesis by A8,SETFAM_1:def 1;
end;
then meet(F1) = f"(meet F) by A9;
hence thesis by A1,A15;
end;
end;
f"([#]S) = [#]T by TOPS_2:41;
then [#]S is closed by A1;
hence thesis by A3,A2,A4,Th5;
end;
theorem Th7:
for x being Point of RealSpace, r being Real holds
Ball(x,r) = ].x-r, x+r.[
proof
let x be Point of RealSpace, r be Real;
reconsider x2=x as Element of REAL by METRIC_1:def 13;
thus Ball(x,r) c= ].x-r, x+r.[
proof
let y be object;
assume
A1: y in Ball(x,r);
then reconsider y1=y as Element of RealSpace;
reconsider y2=y1 as Element of REAL by METRIC_1:def 13;
A2: dist(x,y1)=real_dist.(x2,y2) by METRIC_1:def 1,def 13
.=|.x2 - y2 .| by METRIC_1:def 12
.=|.-(y2 - x2) .|
.=|.y2 - x2 .| by COMPLEX1:52;
dist(x,y1)<r by A1,METRIC_1:11;
hence thesis by A2,RCOMP_1:1;
end;
let y be object;
assume
A3: y in ].x-r, x+r.[;
then reconsider y2=y as Element of REAL;
reconsider x1=x,y1=y2 as Element of RealSpace by METRIC_1:def 13;
|.y2 - x .|=|.-(y2 - x).| by COMPLEX1:52
.=|.x - y2 .|
.=real_dist.(x2,y2) by METRIC_1:def 12;
then
A4: real_dist.(x2,y2) < r by A3,RCOMP_1:1;
dist(x1,y1)=real_dist.(x2,y2) by METRIC_1:def 1,def 13;
hence thesis by A4,METRIC_1:11;
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;
reconsider A1=A as Subset of RealSpace by TOPMETR:12;
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
reconsider A1=A as Subset of R^1;
A1: the topology of R^1 = Family_open_set(RealSpace) by TOPMETR:12;
assume A is open;
then
A2: A1 in the topology of R^1 by PRE_TOPC:def 2;
let x be Real;
reconsider x1=x as Element of REAL by XREAL_0:def 1;
reconsider x1 as Element of RealSpace by METRIC_1:def 13;
assume x in A;
then consider r being Real such that
A3: r>0 and
A4: Ball(x1,r) c= A1 by A2,A1,PCOMPS_1:def 4;
].x-r, x+r.[ c=A1 by A4,Th7;
hence thesis by A3;
end;
assume
A5: for x being Real st x in A
ex r being Real st r >0 & ].x-r, x+r.[ c= A;
for x being Element of RealSpace st x in A1
ex r being Real st r>0 & Ball(x,r) c= A1
proof
let x be Element of RealSpace;
reconsider x1=x as Real;
assume x in A1;
then consider r being Real such that
A6: r >0 and
A7: ].x1-r, x1+r.[ c= A1 by A5;
Ball(x,r) c= A1 by A7,Th7;
hence thesis by A6;
end;
then
A8: A1 in Family_open_set(RealSpace) by PCOMPS_1:def 4;
the topology of R^1 = Family_open_set(RealSpace) by TOPMETR:12;
hence thesis by A8,PRE_TOPC:def 2;
end;
theorem Th9:
for S being sequence of R^1 st (for n being Element of NAT holds
S.n in ]. n - 1/4 , n + 1/4 .[) holds rng S is closed
proof
let S be sequence of R^1;
reconsider B=rng S as Subset of R^1;
assume
A1: for n being Element of NAT holds S.n in ]. n - 1/4 , n + 1/4 .[;
for x being Point of RealSpace st x in B` ex r being Real 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;
per cases;
suppose
A3: ]. x1 - 1/4 , x1 + 1/4 .[ /\ B = {};
reconsider C=Ball(x,1/4) as Subset of R^1 by TOPMETR:12;
Ball(x,1/4) /\ B`` = {} by A3,Th7;
then C misses B``;
then Ball(x,1/4) c= B` by SUBSET_1:24;
hence thesis;
end;
suppose
A4: ]. x1 - 1/4 , x1 + 1/4 .[ /\ B <> {};
set y = the Element of ]. x1 - 1/4 , x1 + 1/4 .[ /\ B;
A5: y in ]. x1 - 1/4 , x1 + 1/4 .[ by A4,XBOOLE_0:def 4;
A6: y in B by A4,XBOOLE_0:def 4;
reconsider y as Real;
consider n1 being object such that
A7: n1 in dom S and
A8: y = S.n1 by A6,FUNCT_1:def 3;
reconsider n1 as Element of NAT by A7;
set r= |.x1 - y.|;
reconsider C=Ball(x,r) as Subset of R^1 by TOPMETR:12;
|.y-x1.| < 1/4 by A5,RCOMP_1:1;
then |.-(x1-y).| < 1/4;
then
A9: r<=1/4 by COMPLEX1:52;
Ball(x,r) misses rng S
proof
assume Ball(x,r) meets rng S;
then consider z being object such that
A10: z in Ball(x,r) and
A11: z in rng S by XBOOLE_0:3;
consider n2 being object such that
A12: n2 in dom S and
A13: z = S.n2 by A11,FUNCT_1:def 3;
reconsider n2 as Element of NAT by A12;
reconsider z as Real by A10;
per cases by XXREAL_0:1;
suppose
A14: n1=n2;
A15: r = |. 0 + -(y - x1) .| .= |. y - x1 .| by COMPLEX1:52;
y in ].x1-r,x1+r.[ by A8,A10,A13,A14,Th7;
hence contradiction by A15,RCOMP_1:1;
end;
suppose
A16: n1>n2;
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 ex a1 being Real st
S.n1=a1 & n1 - 1/4 < a1 & a1 < n1 + 1/4;
then
A17: n1 < y + 1/4 by A8,XREAL_1:19;
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 ex a2 being Real
st S.n2=a2 & n2-1/4<a2 & a2<n2+1/4;
then z - 1/4 < n2 by A13,XREAL_1:19;
then
A18: n2 + 1 > z - 1/4 + 1 by XREAL_1:6;
n2 + 1 <= n1 by A16,NAT_1:13;
then n2 +1 < y + 1/4 by A17,XXREAL_0:2;
then z + (-1/4 + 1) < y + 1/4 by A18,XXREAL_0:2;
then
A19: z < y + 1/4 - (-1/4 + 1) by XREAL_1:20;
Ball(x,r) c= Ball(x,1/4) by A9,PCOMPS_1:1;
then z in Ball(x,1/4) by A10;
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 ex a1 being Real st a1=z & x1-1/4<a1 & a1<x1 +1/4;
then
A20: z + 1/4 > x1 by XREAL_1:19;
y in {a where a is Real: x1 - 1/4 < a & a < x1 + 1/4 }
by A5,RCOMP_1:def 2;
then ex a1 being Real
st y=a1 & x1 - 1/4 < a1 & a1 < x1 + 1/4;
then y -1/4 < x1 + 1/4 - 1/4 by XREAL_1:9;
then z + 1/4 > y - 1/4 by A20,XXREAL_0:2;
then z + 1/4 + -1/4 > y - 1/4 + -1/4 by XREAL_1:6;
hence contradiction by A19;
end;
suppose
A21: n1<n2;
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 ex a2 being Real st S.n2=a2 & n2-1/4<a2 & a2<n2+1/4;
then
A22: z + 1/4 > n2 + -1/4 + 1/4 by A13,XREAL_1:6;
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 ex a1 being Real st S.n1=a1 & n1-1/4<a1 & a1<n1+1/4;
then n1 + 1/4 - 1/4 > y - 1/4 by A8,XREAL_1:9;
then
A23: n1 + 1 > y - 1/4 + 1 by XREAL_1:6;
n1 + 1 <= n2 by A21,NAT_1:13;
then z + 1/4 > n1 + 1 by A22,XXREAL_0:2;
then y + -1/4 + 1 < z + 1/4 by A23,XXREAL_0:2;
then
A24: y + (-1/4 + 1) - (-1/4 + 1) < z + 1/4 - (-1/4 + 1) by XREAL_1:9;
Ball(x,r) c= Ball(x,1/4) by A9,PCOMPS_1:1;
then z in Ball(x,1/4) by A10;
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 ex a1 being Real st a1=z & x1-1/4<a1 & a1<x1 +1/4;
then
A25: z - 1/4 < x1 by XREAL_1:19;
y in {a where a is Real: x1 - 1/4 < a & a < x1 + 1/4 } by A5,
RCOMP_1:def 2;
then ex a1 being Real st y=a1 & x1 - 1/4 < a1 & a1 < x1 + 1/4;
then x1 + -1/4 + 1/4 < y + 1/4 by XREAL_1:6;
then z - 1/4 < y + 1/4 by A25,XXREAL_0:2;
then z - 1/4 + 1/4< y + 1/4 + 1/4 by XREAL_1:6;
then z - 1/2 < y + 1/2 - 1/2 by XREAL_1:9;
hence contradiction by A24;
end;
end;
then C misses B``;
then
A26: C c= B` by SUBSET_1:24;
x1 <> y
proof
assume x1 = y;
then y in B /\ (B`) by A2,A6,XBOOLE_0:def 4;
then B meets (B`);
hence contradiction by SUBSET_1:24;
end;
then x1 + (-y) <> y + (-y);
then |.x1-y.| > 0 by COMPLEX1:47;
hence thesis by A26;
end;
end;
then [#](R^1)\(rng S) is open by TOPMETR:15;
hence thesis by PRE_TOPC:def 3;
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;
A1: dom (id NAT) = NAT;
A2: rng (id NAT) = NAT;
then reconsider S=(id NAT) as sequence of R^1
by A1,FUNCT_2:2,TOPMETR:17,NUMBERS:19;
for n being Element of NAT holds S.n in ].n-1/4,n + 1/4.[
proof
let n be Element of NAT;
reconsider x=S.n as Real;
A3: - 1/4 + n < 0 + n by XREAL_1:8;
x=n & n < n + 1/4 by XREAL_1:29;
then x in {r where r is Real: n - 1/4 < r & r < n + 1/4} by A3;
hence thesis by RCOMP_1:def 2;
end;
hence thesis by A2,Th9;
end;
definition
let M be non empty MetrStruct, x be Point of TopSpaceMetr(M);
func Balls(x) -> Subset-Family of TopSpaceMetr(M) means
:Def1:
ex y being Point of M st y = x &
it = { Ball(y,1/n) where n is Nat: n <> 0 };
existence
proof
A1: the carrier of M = the carrier of TopSpaceMetr M by TOPMETR:12;
then reconsider y = x as Point of M;
set B = { Ball(y,1/n) where n is Nat: n <> 0 };
B c= bool(the carrier of TopSpaceMetr(M))
proof
let A be object;
assume A in B;
then ex n being Nat st A = Ball(y,1/n) & n <> 0;
hence thesis by A1;
end;
hence thesis;
end;
uniqueness;
end;
registration
let M be non empty MetrSpace, x be Point of TopSpaceMetr(M);
cluster Balls(x) -> open x -quasi_basis;
coherence
proof
set B = Balls(x);
consider x9 being Point of M such that
A1: x9 = x & B = { Ball(x9,1/n) where n is Nat: n <> 0 } by Def1;
A2: B c= the topology of TopSpaceMetr(M)
proof
let A be object;
assume A in B;
then consider n being Nat such that
A3: A = Ball(x9,1/n) and
n<>0 by A1;
Ball(x9,1/n) in Family_open_set M by PCOMPS_1:29;
hence thesis by A3,TOPMETR:12;
end;
A4: for O being set st O in B holds x in O
proof
let O be set;
assume O in B;
then ex n being Nat st O = Ball(x9,1/n) & n<>0 by A1;
hence thesis by A1,GOBOARD6:1;
end;
A5: 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 such that
A6: r>0 and
A7: Ball(x9,r) c= O by A1,TOPMETR:15;
reconsider r as Real;
consider n being Nat such that
A8: 1/n < r and
A9: n > 0 by A6,Lm1;
reconsider Ba=Ball(x9,1/n) as Subset of TopSpaceMetr(M) by TOPMETR:12;
reconsider Ba as Subset of TopSpaceMetr(M);
take Ba;
thus Ba in B by A1,A9;
Ball(x9,1/n) c= Ball(x9,r) by A8,PCOMPS_1:1;
hence thesis by A7;
end;
A10: Ball(x9,1/1) in B by A1;
then Intersect B = meet B by SETFAM_1:def 9;
then x in Intersect B by A10,A4,SETFAM_1:def 1;
hence thesis by A2,A5,TOPS_2:64,YELLOW_8:def 1;
end;
end;
registration
let M be non empty MetrSpace, x be Point of TopSpaceMetr(M);
cluster Balls(x) -> countable;
coherence
proof
set B = Balls(x);
consider x9 being Point of M such that
A1: x9 = x & B = { Ball(x9,1/n) where n is Nat: n <> 0 } by Def1;
deffunc F(Nat) = Ball(x9,1/$1);
defpred P[Nat] means $1 <> 0;
{ F(n) where n is Nat : P[n] } is countable from CARD_4:sch 1;
hence thesis by A1;
end;
end;
theorem Th11:
for M being non empty MetrSpace, x being Point of TopSpaceMetr(M),
x9 being Point of M st x = x9
ex f being sequence of Balls(x) st
for n being Element of NAT holds f.n = Ball(x9,1/(n+1))
proof
let M be non empty MetrSpace, x be Point of TopSpaceMetr(M),
x9 be Point of M;
assume
A1: x = x9;
set B = Balls(x);
consider x9 being Point of M such that
A2: x9 = x & B = { Ball(x9,1/n) where n is Nat: n <> 0 } by Def1;
defpred P[object,object] means
ex n9 being Element of NAT st $1=n9 &
$2 = Ball(x9,1/(n9+1));
A3: for n being object st n in NAT ex O being object st O in B & P[n,O]
proof
let n be object;
assume n in NAT;
then reconsider n as Element of NAT;
take Ball(x9,1/(n+1));
thus thesis by A2;
end;
consider f being Function such that
A4: dom f = NAT & rng f c= B and
A5: for n being object st n in NAT holds P[n,f.n] from FUNCT_1:sch 6(A3);
reconsider f as sequence of B by A4,FUNCT_2:2;
take f;
let n be Element of NAT;
P[n,f.n] by A5;
hence thesis by A2,A1;
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 object;
assume y in rng(f+*g);
then consider x being object such that
A1: x in dom(f+*g) and
A2: (f+*g).x = y by FUNCT_1:def 3;
per cases;
suppose
A3: x in dom g;
then y = g.x by A2,FUNCT_4:13;
then y in rng g by A3,FUNCT_1:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A4: not x in dom g;
x in dom f \/ dom g by A1,FUNCT_4:def 1;
then x in dom f by A4,XBOOLE_0:def 3;
then
A5: x in dom f \ dom g by A4,XBOOLE_0:def 5;
y = f.x by A2,A4,FUNCT_4:11;
then y in f.:(dom f \ dom g) by A5,FUNCT_1:def 6;
hence thesis by XBOOLE_0:def 3;
end;
end;
let y be object;
assume
A6: y in f.:(dom f\dom g) \/ rng g;
per cases by A6,XBOOLE_0:def 3;
suppose
y in f.:(dom f\dom g);
then consider x being object such that
A7: x in dom f and
A8: x in dom f \ dom g and
A9: f.x = y by FUNCT_1:def 6;
not x in dom g by A8,XBOOLE_0:def 5;
then
A10: (f+*g).x = f.x by FUNCT_4:11;
x in dom f \/ dom g by A7,XBOOLE_0:def 3;
then x in dom(f+*g) by FUNCT_4:def 1;
hence thesis by A9,A10,FUNCT_1:def 3;
end;
suppose
A11: y in rng g;
rng g c= rng(f +* g) by FUNCT_4:18;
hence thesis by A11;
end;
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;
thus (id A).:(B) c= B
proof
let y be object;
assume y in (id A).:(B);
then ex x being object st x in dom(id A) & x in B & (id A).x = y by
FUNCT_1:def 6;
hence thesis by FUNCT_1:17;
end;
let y be object;
assume
A2: y in B;
then dom(id A) = A & (id A).y = y by A1,FUNCT_1:17;
hence thesis by A1,A2,FUNCT_1:def 6;
end;
theorem Th14:
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);
hence thesis by FUNCOP_1:13;
end;
theorem Th15:
for A,B,x being set st B <> {} holds rng((id A)+*(B --> x)) = (A \ B) \/ {x}
proof
let A,B,x be set;
set f = ((id A)+*(B --> x));
assume B <> {};
then
A1: rng (B --> x)={x} by FUNCOP_1:8;
thus rng((id A)+*(B --> x)) c= (A \ B) \/ {x}
proof
let y be object;
assume y in rng f;
then consider x1 being object such that
A2: x1 in dom f and
A3: y = f.x1 by FUNCT_1:def 3;
A4: x1 in dom (id A) \/ dom (B --> x) by A2,FUNCT_4:def 1;
per cases;
suppose
x1 in dom (B --> x);
then f.x1 = (B --> x).x1 & (B --> x).x1 = x by A4,FUNCOP_1:7
,FUNCT_4:def 1;
then y in {x} by A3,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A5: not x1 in dom (B --> x);
then
A6: f.x1 = (id A).x1 by A4,FUNCT_4:def 1;
A7: x1 in dom (id A) by A4,A5,XBOOLE_0:def 3;
not x1 in B by A5,FUNCOP_1:13;
then x1 in A \ B by A7,XBOOLE_0:def 5;
then x1 in (A \ B) \/ {x} by XBOOLE_0:def 3;
hence thesis by A3,A6,A7,FUNCT_1:18;
end;
end;
let y be object;
(id A).:(A \ B)=A \ B by Th13;
then (id A).:(dom(id A) \ B)=A \ B;
then
A8: (id A).:(dom(id A) \ dom( B --> x))=A \ B by FUNCOP_1:13;
assume y in (A \ B) \/ {x};
hence thesis by A1,A8,Th12;
end;
theorem Th16:
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 object;
assume
A2: x1 in f"(C \ {x});
then
A3: f.x1 in (C \ {x}) by FUNCT_1:def 7;
A4: not x1 in B
proof
assume
A5: x1 in B;
then
A6: x1 in dom(B --> x) by FUNCOP_1:13;
then x1 in dom(id A) \/ dom(B --> x) by XBOOLE_0:def 3;
then f.x1=(B --> x).x1 by A6,FUNCT_4:def 1;
then
A7: f.x1=x by A5,FUNCOP_1:7;
not f.x1 in {x} by A3,XBOOLE_0:def 5;
hence contradiction by A7,TARSKI:def 1;
end;
then
A8: not x1 in dom(B --> x);
x1 in dom f by A2,FUNCT_1:def 7;
then x1 in A \/ B by Th14;
then
A9: x1 in A or x1 in B by XBOOLE_0:def 3;
then x1 in dom(id A) by A4;
then x1 in dom(id A) \/ dom(B --> x) by XBOOLE_0:def 3;
then f.x1 = (id A).x1 by A8,FUNCT_4:def 1;
then
A10: f.x1 = x1 by A4,A9,FUNCT_1:17;
then
A11: not x1 in {x} by A3,XBOOLE_0:def 5;
x1 in C \ B by A3,A4,A10,XBOOLE_0:def 5;
hence thesis by A11,XBOOLE_0:def 5;
end;
let x1 be object;
assume
A12: x1 in C \ B \ {x};
then not x1 in {x} by XBOOLE_0:def 5;
then
A13: x1 in C \ {x} by A12,XBOOLE_0:def 5;
A14: x1 in C by A12;
then x1 in A by A1;
then x1 in dom(id A);
then
A15: x1 in dom(id A) \/ dom(B --> x) by XBOOLE_0:def 3;
x1 in C \ B by A12,XBOOLE_0:def 5;
then not x1 in dom(B --> x) by XBOOLE_0:def 5;
then f.x1 = (id A).x1 by A15,FUNCT_4:def 1;
then
A16: f.x1 = x1 by A1,A14,FUNCT_1:17;
x1 in dom f by A15,FUNCT_4:def 1;
hence thesis by A13,A16,FUNCT_1:def 7;
end;
theorem Th17:
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;
set f = (id A)+*(B --> x);
assume
A1: not x in A;
thus f"({x}) c= B
proof
let y be object;
assume
A2: y in f"({x});
then
A3: y in dom f by FUNCT_1:def 7;
A4: f.y in {x} by A2,FUNCT_1:def 7;
per cases;
suppose
y in dom (B --> x);
hence thesis;
end;
suppose
A5: not y in dom (B --> x);
then
A6: f.y = (id A).y by FUNCT_4:11;
A7: y in dom (B --> x) or y in dom (id A) by A3,FUNCT_4:12;
then (id A).y = y by A5,FUNCT_1:18;
then y = x by A4,A6,TARSKI:def 1;
hence thesis by A1,A7;
end;
end;
let y be object;
assume
A8: y in B;
then
A9: y in dom (B-->x) by FUNCOP_1:13;
then f.y = (B-->x).y by FUNCT_4:13;
then f.y = x by A8,FUNCOP_1:7;
then
A10: f.y in {x} by TARSKI:def 1;
y in dom f by A9,FUNCT_4:12;
hence thesis by A10,FUNCT_1:def 7;
end;
theorem Th18:
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 that
A1: C c= A and
A2: not x in A;
A3: C \ {x} = C
proof
thus C \ {x} c= C;
let y be object;
assume
A4: y in C;
not y in {x}
proof
assume y in {x};
then y = x by TARSKI:def 1;
hence contradiction by A1,A2,A4;
end;
hence thesis by A4,XBOOLE_0:def 5;
end;
A5: C \ B \ {x} \/ B = C \/ B
proof
thus C \ B \ {x} \/ B c= C \/ B
proof
let y be object;
assume y in C \ B \ {x} \/ B;
then y in C \ B \ {x} or y in B by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
let y be object;
assume y in C \/ B;
then
A6: y in (C \ B) \/ B by XBOOLE_1:39;
per cases by A6,XBOOLE_0:def 3;
suppose
A7: y in C \ B;
then
A8: y in C;
not y in {x}
proof
assume y in {x};
then x in C by A8,TARSKI:def 1;
hence contradiction by A1,A2;
end;
then y in C \ B \ {x} by A7,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
suppose
y in B;
hence thesis by XBOOLE_0:def 3;
end;
end;
set f = ((id A)+*(B --> x));
f"({x})=B by A2,Th17;
then f"(C \/ {x}) = f"(C) \/ B by RELAT_1:140;
hence thesis by A1,A3,A5,Th16;
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 that
A1: C c= A and
A2: not x in A;
not x in C \ B
by A1,A2;
then (C \ B) misses {x} by ZFMISC_1:50;
then C \ B \ {x} = C \ B by XBOOLE_1:83;
hence thesis by A1,Th16;
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
for x be Point of T ex B be Basis of x st B is countable;
end;
theorem Th20:
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);
take Balls(x);
thus thesis;
end;
theorem
R^1 is first-countable by Th20;
registration
cluster R^1 -> first-countable;
coherence by Th20;
end;
definition
let T be TopStruct, S be sequence of T, x be Point of T;
pred S is_convergent_to x means
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 Th22:
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);
let U1 be Subset of T;
assume that
U1 is open and
A2: x in U1;
take 0;
let m be Nat;
m in NAT by ORDINAL1:def 12;
hence thesis by A1,A2,FUNCOP_1:7;
end;
definition
let T be TopStruct, S be sequence of T;
attr S is convergent means
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
:Def5:
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 DOMAIN_1:sch 7;
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 by A1,A2;
hence thesis by SUBSET_1:3;
end;
end;
definition
let T be non empty TopStruct;
attr T is Frechet means
:Def6:
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 Th23:
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;
consider f being sequence of B such that
A4: rng f = B by A3,CARD_3:96;
defpred P[object,object] means
ex D1 being set st D1 = $1 & $2 in A /\ meet (f.:succ D1);
A5: for n being object st n in NAT
ex y being object st y in the carrier of T & P[n,y]
proof
defpred P[Nat] means
ex H being Subset of T st H = meet (f.:
succ $1) & H is open;
let n be object;
A6: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
given G being Subset of T such that
A7: G = meet (f.:succ n) and
A8: G is open;
n+1 in NAT;
then
A9: n+1 in dom f by FUNCT_2:def 1;
A10: n in NAT by ORDINAL1:def 12;
n in succ n & dom f = NAT by FUNCT_2:def 1,ORDINAL1:6;
then
A11: f.n in f.:succ n by FUNCT_1:def 6,A10;
f.(n+1) in B;
then consider H1 being Subset of T such that
A12: H1 = f.(n+1);
A13: H1 is open by A12,YELLOW_8:12;
consider H being Subset of T such that
A14: H = H1 /\ G;
take H;
meet (f.:succ (n+1)) = meet (f.:({n+1} \/ Segm(n+1)))
.= meet ((f.:({n+1} \/ (succ Segm n)))) by NAT_1:38
.= meet (Im(f,n+1) \/ (f.:succ n)) by RELAT_1:120
.= meet ({f.(n+1)} \/ (f.:succ n)) by A9,FUNCT_1:59
.= meet {f.(n+1)} /\ meet (f.:succ n) by A11,SETFAM_1:9
.= H by A7,A12,A14,SETFAM_1:10;
hence thesis by A8,A13,A14,TOPS_1:11;
end;
assume n in NAT;
then reconsider n as Element of NAT;
A15: P[0]
proof
f.0 in B;
then reconsider H = f.0 as Subset of T;
take H;
0 in NAT;
then 0 in dom f by FUNCT_2:def 1;
then meet Im(f,0) = meet {f.0} by FUNCT_1:59
.= H by SETFAM_1:10;
hence thesis by YELLOW_8:12;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A15, A6);
then
A16: ex H being Subset of T st H = meet (f.:succ n) & H is open;
A17: 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 object such that
A18: k in dom f and
k in succ n and
A19: G = f.k by FUNCT_1:def 6;
f.k in B by A18,FUNCT_2:5;
hence thesis by A19,YELLOW_8:12;
end;
n in succ n & dom f = NAT by FUNCT_2:def 1,ORDINAL1:6;
then f.n in f.:succ n by FUNCT_1:def 6;
then x in meet (f.:succ n) by A17,SETFAM_1:def 1;
then A meets meet (f.:succ n) by A2,A16,PRE_TOPC:def 7;
then consider y being object such that
A20: y in A /\ meet (f.:succ n) by XBOOLE_0:4;
take y;
thus thesis by A20;
end;
consider S being Function such that
A21: dom S = NAT & rng S c= the carrier of T & for n being object st n in
NAT holds P[n,S.n] from FUNCT_1:sch 6(A5);
A22: rng S c= A
proof
let y be object;
assume y in rng S;
then consider a be object such that
A23: a in dom S & y = S.a by FUNCT_1:def 3;
reconsider a as set by TARSKI:1;
P[a,S.a] by A21,A23;
then y in A /\ meet (f.:succ a) by A23;
hence thesis by XBOOLE_0:def 4;
end;
reconsider S as sequence of T by A21,FUNCT_2:def 1,RELSET_1:4;
A24: 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 n <= m;
then n + 1 <= m + 1 by XREAL_1:6;
then Segm(n + 1) c= Segm(m + 1) by NAT_1:39;
then succ Segm n c= Segm(m +1) by NAT_1:38;
then succ Segm n c= succ Segm m by NAT_1:38;
then
A25: f.:(succ n) c= f.:(succ m) by RELAT_1:123;
A26: n in NAT by ORDINAL1:def 12;
n in succ n & dom f = NAT by FUNCT_2:def 1,ORDINAL1:6;
then f.n in f.:succ n by FUNCT_1:def 6,A26;
then meet (f.:succ m) c= meet (f.:succ n) by A25,SETFAM_1:6;
hence thesis by XBOOLE_1:26;
end;
S is_convergent_to x
proof
let U1 be Subset of T;
assume
A27: U1 is open & x in U1;
reconsider U1 as Subset of T;
consider U2 being Subset of T such that
A28: U2 in B and
A29: U2 c= U1 by A27,YELLOW_8:13;
consider n be object such that
A30: n in dom f and
A31: U2 = f.n by A4,A28,FUNCT_1:def 3;
reconsider n as Element of NAT by A30;
for m being Nat st n <= m holds S.m in U1
proof
let m be Nat;
A32: m in NAT by ORDINAL1:def 12;
n in succ n & dom f = NAT by FUNCT_2:def 1,ORDINAL1:6;
then
A33: f.n in f.:succ n by FUNCT_1:def 6;
assume n <= m;
then
A34: ( A /\ meet (f.:succ m) ) c= A /\ meet (f.:succ n) by A24;
P[m,S.m] by A21,A32;
then S.m in A /\ meet (f.:succ m);
then S.m in meet (f.:succ n) by A34,XBOOLE_0:def 4;
then S.m in f.n by A33,SETFAM_1:def 1;
hence thesis by A29,A31;
end;
hence thesis;
end;
then x in Lim S by Def5;
hence thesis by A22;
end;
registration
cluster first-countable -> Frechet for non empty TopSpace;
coherence by Th23;
end;
theorem Th24:
for T being non empty TopSpace,A being Subset of T holds A is
closed implies for S being sequence of T st 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: rng S c= A;
thus Lim S c= A
proof
reconsider A as Subset of T;
reconsider L = Lim S as Subset of T;
L c= A
proof
let y be object;
assume
A3: y in L;
then reconsider p=y as Point of T;
A4: S is_convergent_to p by A3,Def5;
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;
reconsider U2 = U1 as Subset of T;
assume p in U1;
then consider n being Nat such that
A6: for m being Nat st n <= m holds S.m in U2 by A4,A5;
A7: n in NAT by ORDINAL1:def 12;
dom S = NAT by FUNCT_2:def 1;
then
A8: S.n in rng S by FUNCT_1:def 3,A7;
S.n in U1 by A6;
then S.n in A /\ U1 by A2,A8,XBOOLE_0:def 4;
hence thesis;
end;
then p in Cl A by PRE_TOPC:def 7;
hence thesis by A1,PRE_TOPC:22;
end;
hence thesis;
end;
end;
theorem Th25:
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
by Th24;
theorem Th26:
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: Cl(A) c= A
proof
let x be object;
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;
S is_convergent_to p by A6,Def5;
then S is convergent;
then Lim S c= A by A2,A5;
hence thesis by A6;
end;
A c= Cl(A) by PRE_TOPC:18;
then A = Cl(A) by A3;
hence thesis by PRE_TOPC:22;
end;
hence thesis by Th25;
end;
registration
cluster Frechet -> sequential for non empty TopSpace;
coherence by Th26;
end;
begin
::
:: Not (for T holds T is Frechet implies T is first-countable)
::
definition
func REAL? -> strict non empty TopSpace means
:Def8:
the carrier of it = (
REAL \ NAT) \/ {REAL} & ex f being Function 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
set f = (id REAL)+*(NAT --> REAL);
reconsider X = (REAL \ NAT) \/ {REAL} as non empty set;
A1: rng f c= (REAL \ NAT) \/ {REAL} by Th15;
REAL \/ NAT = REAL by XBOOLE_1:12,NUMBERS:19;
then dom f = the carrier of R^1 by Th14,TOPMETR:17;
then reconsider f as Function of the carrier of R^1,X by A1,FUNCT_2:2;
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 object;
assume B in O;
then
ex A being Subset of X st B = X\A & ex fA being Subset of R^1 st fA =
f"A & fA is closed;
hence thesis;
end;
then reconsider O as Subset-Family of X;
set T = TopStruct(#X,O#);
reconsider f as Function of R^1,T;
A2: 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 3;
then [#]T \ A in the topology of T by PRE_TOPC:def 2;
then consider B being Subset of X such that
A3: X \ B = [#]T \ A and
A4: ex fA being Subset of R^1 st fA = f"B & fA is closed;
B = [#]T \ ([#]T \ A) by A3,PRE_TOPC:3;
hence thesis by A4,PRE_TOPC:3;
end;
assume f"A is closed;
then X \ A in O;
then [#]T \ A is open by PRE_TOPC:def 2;
hence thesis by PRE_TOPC:def 3;
end;
then reconsider T as strict non empty TopSpace by Th6;
take T;
thus the carrier of T = (REAL \ NAT) \/ {REAL};
reconsider f as Function of R^1,T;
take f;
thus thesis by A2;
end;
uniqueness
proof
let X,Y be strict non empty TopSpace such that
A5: the carrier of X = (REAL \ NAT) \/ {REAL} and
A6: ex f being Function 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
A7: the carrier of Y = (REAL \ NAT) \/ {REAL} and
A8: ex f being Function 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;
consider g being Function of R^1, Y such that
A9: g = (id REAL)+*(NAT --> REAL) and
A10: for A being Subset of Y holds A is closed iff g"A is closed by A8;
consider f being Function of R^1, X such that
A11: f = (id REAL)+*(NAT --> REAL) and
A12: for A being Subset of X holds A is closed iff f"A is closed by A6;
A13: the topology of Y c= the topology of X
proof
let V be object;
assume
A14: V in the topology of Y;
then reconsider V1=V as Subset of Y;
reconsider V2=V as Subset of X by A5,A7,A14;
reconsider V1 as Subset of Y;
reconsider V2 as Subset of X;
V1 is open by A14,PRE_TOPC:def 2;
then [#](Y)\V1 is closed by Lm2;
then f"([#]Y\V1) is closed by A11,A9,A10;
then [#]X\V2 is closed by A5,A7,A12;
then V2 is open by Lm2;
hence thesis by PRE_TOPC:def 2;
end;
the topology of X c= the topology of Y
proof
let V be object;
assume
A15: V in the topology of X;
then reconsider V1=V as Subset of X;
reconsider V2=V as Subset of Y by A5,A7,A15;
reconsider V1 as Subset of X;
reconsider V2 as Subset of Y;
V1 is open by A15,PRE_TOPC:def 2;
then [#](X)\V1 is closed by Lm2;
then g"([#]X\V1) is closed by A11,A12,A9;
then [#]Y\V2 is closed by A5,A7,A10;
then V2 is open by Lm2;
hence thesis by PRE_TOPC:def 2;
end;
hence thesis by A5,A7,A13,XBOOLE_0:def 10;
end;
end;
Lm3: {REAL} c= the carrier of REAL?
proof
let x be object;
assume x in {REAL};
then x in (REAL\NAT) \/ {REAL} by XBOOLE_0:def 3;
hence thesis by Def8;
end;
theorem Th27:
REAL is Point of REAL?
proof
REAL in {REAL} by TARSKI:def 1;
hence thesis by Lm3;
end;
theorem Th28:
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 Function 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 Def8;
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:4;
then f"(A`) is closed by A2;
then
A6: (f"(A`))` is open by TOPS_1:3;
A7: not REAL in [#](REAL?) \ A by A4,XBOOLE_0:def 5;
A8: A` c= A` \ {REAL}
proof
let x be object;
assume
A9: x in A`;
then not x in {REAL} by A7,TARSKI:def 1;
hence thesis by A9,XBOOLE_0:def 5;
end;
A` c= the carrier of REAL?;
then
A10: A` c= (REAL \ NAT) \/ {REAL} by Def8;
A11: A` c= REAL \ NAT
proof
let x be object;
assume
A12: x in A`;
then x in (REAL \ NAT) or x in {REAL} by A10,XBOOLE_0:def 3;
hence thesis by A7,A12,TARSKI:def 1;
end;
A` \ {REAL} c= A` by XBOOLE_1:36;
then
A13: A` = A` \ {REAL} by A8;
not REAL in REAL;
then ((id REAL)+*(NAT --> REAL))"(A` \ {REAL}) = A` \ NAT by A11,Th19,
XBOOLE_1:1;
then O = ([#](R^1) \ A`) \/ (NAT /\ [#](R^1)) by A1,A5,A13,XBOOLE_1:52;
then
A14: O = ([#](R^1) \ A`) \/ NAT by TOPMETR:17,XBOOLE_1:28,NUMBERS:19;
A = A`` .= (the carrier of REAL?) \ A`;
then
A15: A = ((REAL \ NAT) \/ {REAL}) \ A` by Def8;
A16: A = (REAL \ A`) \ NAT \/ {REAL}
proof
thus A c= (REAL \ A`) \ NAT \/ {REAL}
proof
let x be object;
assume
A17: x in A;
then
A18: not x in A` by XBOOLE_0:def 5;
x in (REAL \ NAT) or x in {REAL} by A15,A17,XBOOLE_0:def 3;
then x in (REAL\ A`) & not x in NAT or x in {REAL} by A18,
XBOOLE_0:def 5;
then x in (REAL\ A`) \ NAT or x in {REAL} by XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume x in (REAL \ A`) \ NAT \/ {REAL};
then x in (REAL \ A`) \ NAT or x in {REAL} by XBOOLE_0:def 3;
then
A19: x in (REAL \ A`) & not x in NAT or x in {REAL} & not x in A` by A7,
TARSKI:def 1,XBOOLE_0:def 5;
then x in REAL\ NAT or x in {REAL} by XBOOLE_0:def 5;
then
A20: x in (REAL \ NAT) \/ {REAL} by XBOOLE_0:def 3;
not x in A` by A19,XBOOLE_0:def 5;
hence thesis by A15,A20,XBOOLE_0:def 5;
end;
NAT c= REAL \ A`
proof
let x be object;
assume
A21: x in NAT;
then not x in A` by A11,XBOOLE_0:def 5;
hence thesis by A21,XBOOLE_0:def 5,NUMBERS:19;
end;
then O = REAL \ A` by A14,TOPMETR:17,XBOOLE_1:12;
hence thesis by A5,A6,A14,A16,XBOOLE_1:7;
end;
given O being Subset of R^1 such that
A22: O is open and
A23: NAT c= O and
A24: A=(O\NAT) \/ {REAL};
consider B being Subset of R^1 such that
A25: B = [#](R^1) \ O;
not REAL in REAL;
then ((id REAL)+*(NAT --> REAL))"((REAL \ O) \ {REAL})= REAL \ O \ NAT by
Th19;
then
A26: f"((REAL \ O) \ {REAL}) = REAL \ (O \/ NAT) by A1,XBOOLE_1:41;
A27: B is closed by A22,A25,Lm2;
A` = ((REAL \ NAT) \/ {REAL}) \ ((O\NAT) \/ {REAL}) by A24,Def8
.= ((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 A23,XBOOLE_1:12;
then f"(A`)=B by A23,A25,A26,TOPMETR:17,XBOOLE_1:12;
then [#](REAL?) \ A is closed by A2,A27;
hence A is open by Lm2;
REAL in {REAL} by TARSKI:def 1;
hence thesis by A24,XBOOLE_0:def 3;
end;
theorem Th29:
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 that
A1: A is Subset of REAL? and
A2: not REAL in A;
A c= the carrier of REAL? by A1;
then
A3: A c= (REAL \ NAT) \/ {REAL} by Def8;
A c= REAL
proof
let x be object;
assume
A4: x in A;
then x in REAL \ NAT or x in {REAL} by A3,XBOOLE_0:def 3;
hence thesis by A2,A4,TARSKI:def 1;
end;
hence A is Subset of R^1 by TOPMETR:17;
thus NAT /\ A = {}
proof
set x = the Element of NAT /\ A;
assume
A5: NAT /\ A <> {};
then
A6: x in NAT by XBOOLE_0:def 4;
A7: x in A by A5,XBOOLE_0:def 4;
per cases by A3,A7,XBOOLE_0:def 3;
suppose
x in REAL \ NAT;
hence contradiction by A6,XBOOLE_0:def 5;
end;
suppose
x in {REAL};
then x = REAL by TARSKI:def 1;
then REAL in REAL by A6,NUMBERS:19;
hence contradiction;
end;
end;
end;
assume that
A8: A is Subset of R^1 and
A9: NAT /\ A = {};
A10: A c= REAL \ NAT
proof
let x be object;
assume
A11: x in A;
then not x in NAT by A9,XBOOLE_0:def 4;
hence thesis by A8,A11,TOPMETR:17,XBOOLE_0:def 5;
end;
REAL \ NAT c= (REAL \ NAT) \/ {REAL} by XBOOLE_1:7;
then A c= (REAL \ NAT) \/ {REAL} by A10;
hence A is Subset of REAL? by Def8;
thus not REAL in A
proof
assume REAL in A;
then REAL in REAL by A8,TOPMETR:17;
hence contradiction;
end;
end;
theorem Th30:
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?;
consider f being Function 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 Def8;
assume
A3: A = B;
A4: NAT /\ A = {} & not REAL in B implies f"(B`) = A`
proof
assume that
A5: NAT /\ A = {} and
A6: not REAL in B;
A7: REAL \ A = ((((REAL\NAT)\/{REAL})\A)\{REAL}) \/ NAT
proof
thus REAL \ A c= ((((REAL\NAT)\/{REAL})\A)\{REAL}) \/ NAT
proof
let x be object;
assume
A8: x in REAL\A;
then
A9: not x in A by XBOOLE_0:def 5;
A10: x in REAL by A8;
A11: not x in {REAL}
proof
assume x in {REAL};
then A: x = REAL by TARSKI:def 1;
reconsider xx = x as set by TARSKI:1;
not xx in xx;
hence contradiction by A,A10;
end;
per cases;
suppose
x in NAT;
hence thesis by XBOOLE_0:def 3;
end;
suppose
not x in NAT;
then x in REAL \ NAT by A8,XBOOLE_0:def 5;
then x in (REAL\NAT) \/ {REAL} by XBOOLE_0:def 3;
then x in ((REAL\NAT)\/{REAL})\A by A9,XBOOLE_0:def 5;
then x in (((REAL\NAT)\/{REAL})\A)\{REAL} by A11,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
end;
let x be object;
assume
A12: x in ((((REAL\NAT)\/{REAL})\A)\{REAL}) \/ NAT;
per cases by A12,XBOOLE_0:def 3;
suppose
A13: x in NAT;
then not x in A by A5,XBOOLE_0:def 4;
hence thesis by A13,XBOOLE_0:def 5,NUMBERS:19;
end;
suppose
A14: x in (((REAL\NAT)\/{REAL})\A)\{REAL};
then x in ((REAL\NAT)\/{REAL})\A by XBOOLE_0:def 5;
then
A15: not x in A by XBOOLE_0:def 5;
x in REAL\NAT or x in {REAL} by A14,XBOOLE_0:def 3;
hence thesis by A14,A15,XBOOLE_0:def 5;
end;
end;
B` c= the carrier of REAL?;
then
A16: B` c= (REAL \ NAT) \/ {REAL} by Def8;
A17: B` \ {REAL} c= REAL
proof
let x be object;
assume
A18: x in B` \ {REAL};
then x in B` by XBOOLE_0:def 5;
then x in (REAL \ NAT) or x in {REAL} by A16,XBOOLE_0:def 3;
hence thesis by A18,XBOOLE_0:def 5;
end;
A19: REAL in [#](REAL?) \ B by A6,Th27,XBOOLE_0:def 5;
{REAL} c= B`
by A19,TARSKI:def 1;
then ( not REAL in REAL)& B` = (B`\{REAL}) \/ {REAL} by XBOOLE_1:45;
then ((id REAL)+*(NAT --> REAL))"(B`) = (([#](REAL?) \ B)\{REAL}) \/ NAT
by A17,Th18
.= ((((REAL\NAT)\/{REAL})\A)\{REAL}) \/ NAT by A3,Def8;
hence thesis by A1,A7,TOPMETR:17;
end;
thus NAT /\ A = {} & A is open implies not REAL in B & B is open
proof
assume that
A20: NAT /\ A = {} and
A21: A is open;
thus not REAL in B by A3,A20,Th29;
A` is closed by A21,TOPS_1:4;
then B` is closed by A3,A2,A4,A20,Th29;
hence thesis by TOPS_1:4;
end;
assume that
A22: not REAL in B and
A23: B is open;
thus NAT /\ A = {} by A3,A22,Th29;
B` is closed by A23,TOPS_1:4;
then A` is closed by A3,A2,A4,A22,Th29;
hence thesis by TOPS_1:4;
end;
theorem Th31:
for A being Subset of REAL? st A = {REAL} holds A is closed
proof
reconsider B = REAL \ NAT as Subset of R^1 by TOPMETR:17;
let A be Subset of REAL?;
reconsider B as Subset of R^1;
A1: (REAL\NAT) = ((REAL\NAT) \/ {REAL})\{REAL}
proof
thus (REAL\NAT) c= ((REAL\NAT) \/ {REAL})\{REAL}
proof
let x be object;
assume
A2: x in REAL \ NAT;
then
A3: x in REAL;
A4: not x in {REAL}
proof
assume x in {REAL};
then A: x = REAL by TARSKI:def 1;
reconsider xx = x as set by TARSKI:1;
not xx in xx;
hence contradiction by A,A3;
end;
x in (REAL \ NAT) \/ {REAL} by A2,XBOOLE_0:def 3;
hence thesis by A4,XBOOLE_0:def 5;
end;
let x be object;
assume
A5: x in ((REAL\NAT) \/ {REAL})\{REAL};
then not x in {REAL} by XBOOLE_0:def 5;
hence thesis by A5,XBOOLE_0:def 3;
end;
B misses NAT by XBOOLE_1:79;
then
A6: B /\ NAT = {};
then reconsider C=B as Subset of REAL? by Th29;
assume A = {REAL};
then
A7: C = A` by A1,Def8;
B is open
proof
reconsider N=NAT as Subset of R^1 by TOPMETR:17,NUMBERS:19;
reconsider N as Subset of R^1;
N is closed & N` = B by Th10,TOPMETR:17;
hence thesis by TOPS_1:3;
end;
then C is open by A6,Th30;
hence thesis by A7,TOPS_1:3;
end;
theorem Th32:
REAL? is not first-countable
proof
reconsider y = REAL as Point of REAL? by Th27;
assume REAL? is first-countable;
then consider B being Basis of y such that
A1: B is countable;
consider h being sequence of B such that
A2: rng h = B by A1,CARD_3:96;
defpred P[object,object] means
ex m being Element of NAT st m=$1 & $2 in h.$1 /\
]. m - 1/4 , m + 1/4 .[;
A3: for n being object st n in NAT
ex x being object st x in REAL \ NAT & P[n,x]
proof
let n be object;
assume
A4: n in NAT;
then reconsider m = n as Element of NAT;
n in dom h by A4,FUNCT_2:def 1;
then
A5: h.n in rng h by FUNCT_1:def 3;
then reconsider Bn=h.n as Subset of REAL? by A2;
m in REAL by XREAL_0:def 1;
then reconsider m9=m as Point of RealSpace by METRIC_1:def 13;
reconsider Kn = Ball(m9,1/4) as Subset of R^1 by TOPMETR:12;
reconsider Bn as Subset of REAL?;
Bn is open & y in Bn by A5,YELLOW_8:12;
then consider An being Subset of R^1 such that
A6: An is open and
A7: NAT c= An and
A8: Bn = (An \ NAT) \/ {REAL} by Th28;
reconsider An9=An as Subset of R^1;
Kn is open by TOPMETR:14;
then
A9: An9 /\ Kn is open by A6,TOPS_1:11;
dist(m9,m9)=0 by METRIC_1:1;
then m9 in Ball(m9,1/4) by METRIC_1:11;
then n in An /\ Ball(m9,1/4) by A4,A7,XBOOLE_0:def 4;
then consider r being Real such that
A10: r>0 and
A11: Ball(m9,r) c= An /\ Kn by A9,TOPMETR:15;
reconsider r as Real;
m < m + r by A10,XREAL_1:29;
then m - r < m by XREAL_1:19;
then consider x being Real such that
A12: m - r < x and
A13: x < m by XREAL_1:5;
reconsider x as Element of REAL by XREAL_0:def 1;
take x;
A14: r < 1
proof
assume r>=1;
then 1/2 < r by XXREAL_0:2;
then -r < -(1/2) by XREAL_1:24;
then
A15: -r + m < -(1/2) + m by XREAL_1:6;
-(1/2) + m < r + m by A10,XREAL_1:6;
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(m9,r) by Th7;
then m - 1/2 in Kn by A11,XBOOLE_0:def 4;
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 ex a being Real st a= m - 1/2 & m - 1/4 < a & a < m + 1 /4;
hence contradiction by XREAL_1:6;
end;
A16: not x in NAT
proof
assume x in NAT;
then reconsider x as Element of NAT;
per cases by XXREAL_0:1;
suppose
x = m;
hence contradiction by A13;
end;
suppose
x > m;
hence contradiction by A13;
end;
suppose
A17: x < m;
m < x + r by A12,XREAL_1:19;
then m - x < r by XREAL_1:19;
then
A18: m - x < 1 by A14,XXREAL_0:2;
m >= x + 1 by A17,NAT_1:13;
hence contradiction by A18,XREAL_1:19;
end;
end;
hence x in REAL \ NAT by XBOOLE_0:def 5;
x + 0 < m + r by A10,A13,XREAL_1:8;
then x in {a where a is Real: m - r < a & a < m + r} by A12;
then x in ].m - r,m + r.[ by RCOMP_1:def 2;
then
A19: x in Ball(m9,r) by Th7;
then x in An by A11,XBOOLE_0:def 4;
then x in An \ NAT by A16,XBOOLE_0:def 5;
then
A20: x in Bn by A8,XBOOLE_0:def 3;
take m;
Ball(m9,1/4) = ]. m - 1/4 , m + 1/4 .[ by Th7;
then x in ]. m - 1/4 , m + 1/4 .[ by A11,A19,XBOOLE_0:def 4;
hence thesis by A20,XBOOLE_0:def 4;
end;
consider S being Function such that
A21: dom S = NAT and
A22: rng S c= REAL \ NAT and
A23: for n being object st n in NAT holds P[n,S.n] from FUNCT_1:sch 6(A3);
reconsider S as sequence of R^1 by A21,A22,FUNCT_2:2,TOPMETR:17,XBOOLE_1:1;
reconsider O=rng S as Subset of R^1;
for n being Element of NAT holds S.n in ]. n - 1/4 , n + 1/4 .[
proof
let n be Element of NAT;
ex m being Element of NAT st m=n & S.n in h.n /\ ]. m - 1/4 , m + 1/4
.[ by A23;
hence thesis by XBOOLE_0:def 4;
end;
then O is closed by Th9;
then
A24: [#](R^1)\O is open by PRE_TOPC:def 3;
set A = (O` \ NAT) \/ {REAL};
A c= (REAL \ NAT) \/ {REAL}
proof
let x be object;
assume x in A;
then x in (O` \ NAT) or x in {REAL} by XBOOLE_0:def 3;
then x in O` & not x in NAT or x in {REAL} by XBOOLE_0:def 5;
then x in REAL \ NAT or x in {REAL} by TOPMETR:17,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
then reconsider A as Subset of REAL? by Def8;
reconsider A as Subset of REAL?;
NAT c= O`
proof
let x be object;
assume
A25: x in NAT;
then not x in rng S by A22,XBOOLE_0:def 5;
hence thesis by A25,TOPMETR:17,XBOOLE_0:def 5,NUMBERS:19;
end;
then A is open & REAL in A by A24,Th28;
then consider V being Subset of REAL? such that
A26: V in B and
A27: V c= A by YELLOW_8:13;
consider n1 being object such that
A28: n1 in dom h and
A29: V = h.n1 by A2,A26,FUNCT_1:def 3;
reconsider n=n1 as Element of NAT by A28;
for n being Element of NAT ex x being set st x in h.n & not x in A
proof
let n be Element of NAT;
consider xn being set such that
A30: xn=S.n;
take xn;
A31: S.n in rng S by A21,FUNCT_1:def 3;
then not xn in [#](R^1) \ O by A30,XBOOLE_0:def 5;
then
A32: not xn in (O` \ NAT) by XBOOLE_0:def 5;
not xn = REAL
proof
assume xn = REAL;
then REAL in REAL by A22,A30,A31,XBOOLE_0:def 5;
hence contradiction;
end;
then
A33: not xn in {REAL} by TARSKI:def 1;
ex m being Element of NAT st m=n & S.n in h.n /\ ]. m - 1/4 , m + 1/4
.[ by A23;
hence thesis by A30,A32,A33,XBOOLE_0:def 3,def 4;
end;
then ex x being set st x in h.n & not x in A;
hence contradiction by A27,A29;
end;
theorem Th33:
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 Def8;
then
A2: x in (REAL \ NAT) or x in {REAL} by XBOOLE_0:def 3;
per cases by A2,TARSKI:def 1;
suppose
A3: x in (REAL \ NAT);
then
A4: x in REAL;
A c= the carrier of REAL?;
then
A5: A c= REAL \ NAT \/ {REAL} by Def8;
A\{REAL} c= REAL
proof
let a be object;
assume
A6: a in A\{REAL};
then a in A by XBOOLE_0:def 5;
then a in REAL\NAT or a in {REAL} by A5,XBOOLE_0:def 3;
hence thesis by A6,XBOOLE_0:def 5;
end;
then reconsider A9 = A\{REAL} as Subset of R^1 by TOPMETR:17;
reconsider x9=x as Point of R^1 by A3,TOPMETR:17;
reconsider A9 as Subset of R^1;
for B9 being Subset of R^1 st B9 is open holds x9 in B9 implies A9 meets B9
proof
reconsider C=NAT as Subset of R^1 by TOPMETR:17,NUMBERS:19;
let B9 be Subset of R^1;
reconsider B1=B9 as Subset of R^1;
reconsider C as Subset of R^1;
A7: not x9 in NAT by A3,XBOOLE_0:def 5;
(B9 \ NAT) misses NAT by XBOOLE_1:79;
then
A8: (B9 \ NAT) /\ NAT = {};
then reconsider D=B1 \ C as Subset of REAL? by Th29;
assume B9 is open;
then B1 \ C is open by Th4,Th10;
then
A9: D is open by A8,Th30;
reconsider D as Subset of REAL?;
assume x9 in B9;
then x9 in B9 \ NAT by A7,XBOOLE_0:def 5;
then A meets D by A1,A9,PRE_TOPC:def 7;
then
A10: A /\ D <> {};
A9 /\ B9 <> {}
proof
set a = the Element of A /\ D;
A11: a in D by A10,XBOOLE_0:def 4;
then
A12: a in B9 by XBOOLE_0:def 5;
A13: a in REAL by A11,TOPMETR:17;
A14: not a in {REAL}
proof
assume a in {REAL};
then a = REAL by TARSKI:def 1;
hence contradiction by A13;
end;
a in A by A10,XBOOLE_0:def 4;
then a in A \ {REAL} by A14,XBOOLE_0:def 5;
hence thesis by A12,XBOOLE_0:def 4;
end;
hence thesis;
end;
then x9 in Cl(A9) by PRE_TOPC:def 7;
then consider S9 being sequence of R^1 such that
A15: rng S9 c= A9 and
A16: x9 in Lim S9 by Def6;
A17: rng S9 c= A
by A15,XBOOLE_0:def 5;
then reconsider S=S9 as sequence of REAL? by Th2,XBOOLE_1:1;
take S;
thus rng S c= A by A17;
A18: S9 is_convergent_to x9 by A16,Def5;
S is_convergent_to x
proof
reconsider C={REAL} as Subset of REAL? by Lm3;
let V be Subset of REAL?;
assume that
A19: V is open and
A20: x in V;
reconsider C as Subset of REAL?;
REAL in {REAL} by TARSKI:def 1;
then
A21: not REAL in V \ {REAL} by XBOOLE_0:def 5;
then reconsider V9 = V \ C as Subset of R^1 by Th29;
V \ C is open by A19,Th4,Th31;
then
A22: V9 is open by A21,Th30;
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 A20,XBOOLE_0:def 5;
then consider n being Nat such that
A23: for m being Nat st n <= m holds S9.m in V9 by A18,A22;
take n;
let m be Nat;
assume n <= m;
then S9.m in V9 by A23;
hence thesis by XBOOLE_0:def 5;
end;
hence thesis by Def5;
end;
suppose
A24: x = REAL & x in A;
reconsider S=(NAT --> x) as sequence of REAL?;
take S;
{x} c= A by A24,ZFMISC_1:31;
hence rng S c= A by FUNCOP_1:8;
S is_convergent_to x by Th22;
hence thesis by Def5;
end;
suppose
A25: x = REAL & not x in A;
then reconsider A9=A as Subset of R^1 by Th29;
ex k being Point of R^1 st k in NAT & ex S9 being sequence of R^1 st
rng S9 c= A9 & S9 is_convergent_to k
proof
defpred P[object,object] means
ex D2 being set st D2 = $2 &
$1 in D2 & $2 in the topology of R^1 & D2 /\ A9 = {};
assume
A26: not (ex k being Point of R^1 st k in NAT & ex S9 being sequence
of R^1 st rng S9 c= A9 & S9 is_convergent_to k);
A27: for k being object st k in NAT ex U1 being object st P[k,U1]
proof
given k being object such that
A28: k in NAT and
A29: for U1 being object holds not P[k,U1];
:: for D1 being set, U1 being element
:: holds D1 = U1 & k in D1 & U1 in the topology of R^1
:: implies not D1 /\ A9 = {};
reconsider k as Point of R^1 by A28,TOPMETR:17,NUMBERS:19;
reconsider k99=k as Point of TopSpaceMetr(RealSpace);
reconsider k9=k99 as Point of RealSpace by TOPMETR:12;
set Bs = Balls(k99);
consider h being sequence of Bs such that
A30: for n being Element of NAT holds h.n = Ball(k9,1/(n+1)) by Th11;
defpred P[object,object] means $2 in h.$1 /\ A9;
A31: for n being object st n in NAT
ex z being object st z in the carrier of R^1 & P[n,z]
proof
let n be object;
assume n in NAT;
then reconsider n as Element of NAT;
A32: h.n in Bs;
then reconsider H=h.n as Subset of R^1;
take z = the Element of H /\ A9;
Bs c= the topology of R^1 by TOPS_2:64;
then
A33: H /\ A9 <> {} by A29,A32,YELLOW_8:12;
then z in H by XBOOLE_0:def 4;
hence thesis by A33;
end;
consider S9 being Function such that
A34: dom S9 = NAT & rng S9 c= the carrier of R^1 and
A35: for n being object st n in NAT holds P[n,S9.n]
from FUNCT_1:sch 6(A31);
reconsider S9 as sequence of the carrier of R^1 by A34,FUNCT_2:2;
A36: S9 is_convergent_to k
proof
let U1 be Subset of R^1;
assume U1 is open & k in U1;
then consider r being Real such that
A37: r > 0 and
A38: Ball(k9,r) c= U1 by TOPMETR:15;
reconsider r as Real;
consider n being Nat such that
A39: 1/n < r and
A40: n > 0 by A37,Lm1;
reconsider n as Element of NAT by ORDINAL1:def 12;
take n;
let m be Nat;
A41: m in NAT by ORDINAL1:def 12;
S9.m in h.m /\ A9 by A35,A41;
then
A42: S9.m in h.m by XBOOLE_0:def 4;
assume n <= m;
then n < m + 1 by NAT_1:13;
then 1/(m+1) < 1/n by A40,XREAL_1:88;
then Ball(k9,1/(m+1)) c= Ball(k9,r) by A39,PCOMPS_1:1,XXREAL_0:2;
then
A43: Ball(k9,1/(m+1)) c= U1 by A38;
h.m = Ball(k9,1/(m+1)) by A30,A41;
hence thesis by A43,A42;
end;
rng S9 c= A9
proof
let z be object;
assume z in rng S9;
then consider z9 being object such that
A44: z9 in dom S9 and
A45: z = S9.z9 by FUNCT_1:def 3;
S9.z9 in h.z9 /\ A9 by A35,A44;
hence thesis by A45,XBOOLE_0:def 4;
end;
hence contradiction by A26,A28,A36;
end;
consider g being Function such that
A46: dom g =NAT & for k being object st k in NAT holds P[k,g.k] from
CLASSES1:sch 1(A27);
rng g c= bool the carrier of R^1
proof
let z be object;
assume z in rng g;
then consider k being object such that
A47: k in dom g and
A48: z=g.k by FUNCT_1:def 3;
P[k,g.k] by A46,A47;
then g.k in the topology of R^1;
hence thesis by A48;
end;
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 object such that
A49: k in dom g and
A50: O=g.k by FUNCT_1:def 3;
P[k,g.k] by A46,A49;
then g.k in the topology of R^1;
hence thesis by A50,PRE_TOPC:def 2;
end;
then
A51: union F is open by TOPS_2:19;
(union F)\NAT c= REAL \ NAT by TOPMETR:17,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 Def8;
reconsider B as Subset of REAL?;
A52: B /\ A = {}
proof
set z = the Element of B /\ A;
assume
A53: B /\ A <> {};
then
A54: z in B by XBOOLE_0:def 4;
A55: z in A by A53,XBOOLE_0:def 4;
per cases by A54,XBOOLE_0:def 3;
suppose
z in (union F)\NAT;
then z in union F by XBOOLE_0:def 5;
then consider C being set such that
A56: z in C and
A57: C in F by TARSKI:def 4;
consider l being object such that
A58: l in dom g and
A59: C = g.l by A57,FUNCT_1:def 3;
P[l,g.l] by A46,A58;
then g.l /\ A = {};
hence contradiction by A55,A56,A59,XBOOLE_0:def 4;
end;
suppose
z in {REAL};
then z = REAL by TARSKI:def 1;
hence contradiction by A25,A53,XBOOLE_0:def 4;
end;
end;
NAT c= union F
proof
let k be object;
assume
A60: k in NAT;
then P[k,g.k] by A46;
then k in g.k & g.k in rng g by A46,FUNCT_1:def 3,A60;
hence thesis by TARSKI:def 4;
end;
then B is open & REAL in B by A51,Th28;
then A meets B by A1,A25,PRE_TOPC:def 7;
hence contradiction by A52;
end;
then consider k being Point of R^1 such that
A61: k in NAT and
A62: ex S9 being sequence of R^1 st rng S9 c= A9 & S9 is_convergent_to k;
consider S9 being sequence of R^1 such that
A63: rng S9 c= A9 and
A64: S9 is_convergent_to k by A62;
reconsider S = S9 as sequence of REAL? by A63,Th2,XBOOLE_1:1;
take S;
thus rng S c= A by A63;
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
A65: O is open & NAT c= O and
A66: U1=(O\NAT) \/ {REAL} by A25,Th28;
consider n being Nat such that
A67: for m being Nat st n <= m holds S9.m in O by A61,A64,A65;
take n;
let m be Nat;
assume n <= m;
then
A68: S9.m in O by A67;
A69: m in NAT by ORDINAL1:def 12;
then m in dom S9 by NORMSP_1:12;
then S9.m in rng S9 by FUNCT_1:def 3;
then S9.m in A9 by A63;
then S9.m in the carrier of REAL?;
then S9.m in (REAL \ NAT) \/ {REAL} by Def8;
then
A70: S9.m in (REAL \ NAT) or S9.m in {REAL} by XBOOLE_0:def 3;
reconsider m as Element of NAT by A69;
S9.m <> REAL
proof
A71: S9.m in REAL by TOPMETR:17;
assume S9.m = REAL;
hence contradiction by A71;
end;
then not S9.m in NAT by A70,TARSKI:def 1,XBOOLE_0:def 5;
then S9.m in O \ NAT by A68,XBOOLE_0:def 5;
hence thesis by A66,XBOOLE_0:def 3;
end;
hence thesis by Def5;
end;
end;
theorem
not (for T being non empty TopSpace holds T is Frechet implies T is
first-countable) by Th32,Th33;
begin
::
:: Auxiliary theorems
::
::Moved from CIRCCMB2:5, AK, 20.02.2006
theorem
for f,g being Function st f tolerates g holds rng (f+*g) = (rng f)\/( rng g)
proof
let f,g be Function such that
A1: f tolerates g;
thus rng (f+*g) c= (rng f)\/(rng g) by FUNCT_4:17;
let x be object;
assume
A2: x in (rng f)\/(rng g);
A3: rng(f+*g) = f.:(dom f\dom g)\/rng g by Th12;
A4: rng g c= rng(f+*g) by FUNCT_4:18;
per cases;
suppose
x in rng g;
hence thesis by A4;
end;
suppose
A5: not x in rng g;
then x in rng f by A2,XBOOLE_0:def 3;
then consider a being object such that
A6: a in dom f and
A7: x = f.a by FUNCT_1:def 3;
now
assume
A8: a in dom g;
x = (f+*g).a by A1,A6,A7,FUNCT_4:15
.= g.a by A8,FUNCT_4:13;
hence contradiction by A5,A8,FUNCT_1:def 3;
end;
then a in dom f\dom g by A6,XBOOLE_0:def 5;
then x in f.:(dom f\dom g) by A7,FUNCT_1:def 6;
hence thesis by A3,XBOOLE_0:def 3;
end;
end;
theorem
for r being Real st r>0
ex n being Nat st 1/n < r & n>0 by Lm1;