:: The Sequential Closure Operator In Sequential and Frechet Spaces
:: by Bart{\l}omiej Skorulski
::
:: Received February 13, 1999
:: Copyright (c) 1999-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 XBOOLE_0, PRE_TOPC, RCOMP_1, TARSKI, NAT_1, NUMBERS, FUNCOP_1,
FRECHET, SUBSET_1, CARD_1, STRUCT_0, ORDINAL2, RELAT_1, SEQ_1, VALUED_0,
XXREAL_0, FUNCT_1, RLVECT_3, CARD_3, SETFAM_1, ORDINAL1, ZFMISC_1,
FINSET_1, ARYTM_3, SEQ_2, METRIC_1, PCOMPS_1, METRIC_6, XREAL_0, REAL_1,
WAYBEL_7, ARYTM_1, FUNCT_2, FRECHET2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, SETFAM_1, FINSET_1, CARD_3, TOPS_2, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, SEQ_1, FUNCT_2, NAT_1, XXREAL_2, VALUED_0, METRIC_1,
PCOMPS_1, TBSP_1, DOMAIN_1, STRUCT_0, PRE_TOPC, FUNCOP_1, METRIC_6,
YELLOW_8, FRECHET, SEQ_4;
constructors SETFAM_1, REALSET1, CARD_3, TOPS_2, TBSP_1, METRIC_6, YELLOW_8,
FRECHET, SEQ_4, RELSET_1, FUNCOP_1, NUMBERS;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0,
MEMBERED, STRUCT_0, METRIC_1, PCOMPS_1, FRECHET, VALUED_0, CARD_1,
XXREAL_2, ORDINAL1, FINSET_1, NAT_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, SEQM_3, PRE_TOPC, METRIC_6, FUNCT_1, FRECHET, XBOOLE_0;
equalities XBOOLE_0, ORDINAL1;
expansions TARSKI, PRE_TOPC, TOPS_2, METRIC_6, FUNCT_1, FRECHET, XBOOLE_0;
theorems FRECHET, URYSOHN1, YELLOW_8, PRE_TOPC, TARSKI, FUNCOP_1, NORMSP_1,
ZFMISC_1, PCOMPS_1, FUNCT_1, AXIOMS, CARD_1, RELAT_1, SETFAM_1, ORDINAL1,
FUNCT_2, TOPS_2, SUBSET_1, SEQM_3, NAT_1, INT_1, SEQ_1, TOPMETR,
METRIC_6, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_0, XREAL_1, XXREAL_0,
VALUED_0, XXREAL_2, CARD_3;
schemes CLASSES1, DOMAIN_1, NAT_1, RECDEF_1, SEQ_1, FUNCT_1, VALUED_1;
begin
Lm1: for T being non empty TopSpace st for p being Point of T holds Cl({p}) =
{p} holds T is T_1
proof
let T be non empty TopSpace;
assume
A1: for p being Point of T holds Cl({p}) = {p};
for p being Point of T holds {p} is closed
proof
let p be Point of T;
Cl({p}) = {p} by A1;
hence thesis by PRE_TOPC:22;
end;
hence thesis by URYSOHN1:19;
end;
Lm2: for T being non empty TopSpace holds not T is T_1 implies ex x1,x2 being
Point of T st x1 <> x2 & x2 in Cl({x1})
proof
let T be non empty TopSpace;
assume not T is T_1;
then consider x1 being Point of T such that
A1: Cl{x1} <> {x1} by Lm1;
not {x1} c= Cl{x1} or not Cl{x1} c= {x1} by A1;
then consider x2 being object such that
A2: x2 in Cl{x1} and
A3: not x2 in {x1} by PRE_TOPC:18;
reconsider x2 as Point of T by A2;
take x1,x2;
thus x1 <> x2 by A3,TARSKI:def 1;
thus thesis by A2;
end;
Lm3: for T being non empty TopSpace holds not T is T_1 implies ex x1,x2 being
Point of T, S being sequence of T st S = (NAT --> x1) & x1 <> x2 & S
is_convergent_to x2
proof
let T be non empty TopSpace;
assume not T is T_1;
then consider x1,x2 being Point of T such that
A1: x1 <> x2 and
A2: x2 in Cl({x1}) by Lm2;
set S = NAT --> x1;
take x1,x2,S;
thus S = (NAT --> x1);
thus x1 <> x2 by A1;
thus S is_convergent_to x2
proof
let U1 be Subset of T;
assume
A3: U1 is open & x2 in U1;
take 0;
let n be Nat;
A4: n in NAT by ORDINAL1:def 12;
assume 0 <= n;
{x1} meets U1 by A2,A3,PRE_TOPC:def 7;
then x1 in U1 by ZFMISC_1:50;
hence thesis by FUNCOP_1:7,A4;
end;
end;
Lm4: for T being non empty TopSpace holds T is T_2 implies T is T_1
proof
let T be non empty TopSpace;
assume T is T_2;
then for p being Point of T holds {p} is closed by PCOMPS_1:7;
hence thesis by URYSOHN1:19;
end;
theorem
for T being non empty 1-sorted, S being sequence of T, NS being
increasing sequence of NAT holds S*NS is sequence of T;
theorem
for RS being Real_Sequence st RS=id NAT holds RS is increasing
sequence of NAT;
theorem Th3:
for T being non empty 1-sorted, S being sequence of T, A being
Subset of T holds (for S1 being subsequence of S holds not rng S1 c= A) implies
ex n being Element of NAT st for m being Element of NAT st n <= m holds not S.m
in A
proof
let T be non empty 1-sorted, S be sequence of T, A be Subset of T;
assume
A1: for S1 being subsequence of S holds not rng S1 c= A;
defpred Q[set] means $1 in A;
assume
for n being Element of NAT ex m being Element of NAT st n <= m & S.m in A;
then
A2: for n being Element of NAT ex m being Element of NAT st n <= m & Q[S.m];
consider S1 being subsequence of S such that
A3: for n being Element of NAT holds Q[S1.n] from VALUED_1:sch 1(A2);
rng S1 c= A
proof
let y be object;
assume y in rng S1;
then consider x1 being object such that
A4: x1 in dom S1 and
A5: S1.x1 = y by FUNCT_1:def 3;
reconsider n=x1 as Element of NAT by A4;
S1.n in A by A3;
hence thesis by A5;
end;
hence contradiction by A1;
end;
theorem Th4:
for T being non empty 1-sorted,S being sequence of T, A,B being
Subset of T st rng S c= A \/ B holds ex S1 being subsequence of S st rng S1 c=
A or rng S1 c= B
proof
let T be non empty 1-sorted,S be sequence of T, A,B be Subset of T;
assume
A1: rng S c= A \/ B;
assume
A2: for S1 being subsequence of S holds not rng S1 c= A & not rng S1 c= B;
then consider n1 being Element of NAT such that
A3: for m being Element of NAT st n1 <= m holds not S.m in A by Th3;
consider n2 being Element of NAT such that
A4: for m being Element of NAT st n2 <= m holds not S.m in B by A2,Th3;
reconsider n=max(n1,n2) as Element of NAT;
A5: not S.n in B by A4,XXREAL_0:25;
n in NAT;
then n in dom S by NORMSP_1:12;
then
A6: S.n in rng S by FUNCT_1:def 3;
not S.n in A by A3,XXREAL_0:25;
hence contradiction by A1,A5,A6,XBOOLE_0:def 3;
end;
Lm5: for T being non empty TopSpace st T is first-countable holds for x being
Point of T holds ex B being Basis of x st ex S being Function st dom S = NAT &
rng S = B & for n,m being Element of NAT st m >= n holds S.m c= S.n
proof
let T be non empty TopSpace;
assume
A1: T is first-countable;
let x be Point of T;
consider B1 being Basis of x such that
A2: B1 is countable by A1;
consider f being sequence of B1 such that
A3: rng f = B1 by A2,CARD_3:96;
defpred P[object,object] means
ex D1 being set st D1 = $1 & $2 = meet (f.:succ D1);
A4: for n being object st n in NAT ex A being object st P[n,A]
proof let n be object;
reconsider D1 = n as set by TARSKI:1;
assume n in NAT;
take A = meet (f.:succ D1);
thus P[n,A];
end;
consider S being Function such that
A5: dom S = NAT and
A6: for n being object st n in NAT holds P[n,S.n] from CLASSES1:sch 1(A4);
A7: rng S c= bool the carrier of T
proof
let A be object;
assume A in rng S;
then consider n being object such that
A8: n in dom S & A = S.n by FUNCT_1:def 3;
reconsider n as set by TARSKI:1;
reconsider fsuccn = f.:succ n as Subset-Family of T by XBOOLE_1:1;
P[n,S.n] by A5,A6,A8;
then consider D1 being set such that
A9: D1 = n & S.n = meet fsuccn;
thus thesis by A8,A9;
end;
then reconsider B = rng S as Subset-Family of T;
reconsider B as Subset-Family of T;
A10: ex A being set st A in B
proof
take A = meet(f.:(succ 0));
P[0,S.0] by A6;
then A = S.0;
hence thesis by A5,FUNCT_1:def 3;
end;
then
A11: Intersect B = meet B by SETFAM_1:def 9;
for A being set st A in B holds x in A
proof
let A be set;
assume A in B;
then consider n being object such that
A12: n in dom S and
A13: A = S.n by FUNCT_1:def 3;
reconsider n as set by TARSKI:1;
dom f = NAT & n in succ n by FUNCT_2:def 1,ORDINAL1:6;
then
A14: f.n in f.:succ n by A5,A12,FUNCT_1:def 6;
A15: for A1 being set st A1 in f.:(succ n) holds x in A1
proof
let A1 be set;
assume A1 in f.:(succ n);
then consider m being object such that
A16: m in dom f and
m in succ n and
A17: A1 = f.m by FUNCT_1:def 6;
f.m in rng f by A16,FUNCT_1:def 3;
then reconsider A2=A1 as Subset of T by A3,A17;
reconsider A2 as Subset of T;
A2 in B1 by A3,A16,A17,FUNCT_1:def 3;
hence thesis by YELLOW_8:12;
end;
P[n,S.n] by A5,A6,A12;
then A = meet (f.:(succ n)) by A13;
hence thesis by A15,A14,SETFAM_1:def 1;
end;
then
A18: x in meet B by A10,SETFAM_1:def 1;
A19: B c= the topology of T
proof
let A be object;
assume A in B;
then consider n being object such that
A20: n in dom S and
A21: A = S.n by FUNCT_1:def 3;
reconsider n9=n as Element of NAT by A5,A20;
reconsider n as set by TARSKI:1;
reconsider C=f.:succ n as Subset-Family of T by XBOOLE_1:1;
A22: C is open
by YELLOW_8:12;
succ(n9) is finite;
then f.:(succ n) is finite;
then
A23: meet C is open by A22,TOPS_2:20;
P[n,S.n] by A5,A6,A20;
then A = meet (f.:succ n) by A21;
hence thesis by A23;
end;
for O being Subset of T st O is open & x in O ex A being Subset of T st
A in B & A c= O
proof
let O be Subset of T;
assume O is open & x in O;
then consider A1 being Subset of T such that
A24: A1 in B1 and
A25: A1 c= O by YELLOW_8:def 1;
consider n being object such that
A26: n in dom f and
A27: A1 = f.n by A3,A24,FUNCT_1:def 3;
reconsider n as set by TARSKI:1;
S.n in rng S by A5,A26,FUNCT_1:def 3;
then reconsider A = S.n as Subset of T by A7;
reconsider A as Subset of T;
take A;
thus A in B by A5,A26,FUNCT_1:def 3;
n in succ n by ORDINAL1:6;
then f.n in f.:(succ n) by A26,FUNCT_1:def 6;
then
A28: meet(f.:(succ n)) c= A1 by A27,SETFAM_1:3;
P[n,S.n] by A26,A6;
then S.n c= A1 by A28;
hence thesis by A25;
end;
then reconsider B as Basis of x by A19,A11,A18,TOPS_2:64,YELLOW_8:def 1;
take B,S;
thus dom S = NAT by A5;
thus rng S = B;
for n,m being Element of NAT st m >= n holds S.m c= S.n
proof
let n,m be Element of NAT;
assume m >= n;
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
A29: f.:(succ n) c= f.:(succ m) by RELAT_1:123;
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
A30: meet (f.:succ m) c= meet (f.:succ n) by A29,SETFAM_1:6;
A31: P[m,S.m] by A6;
P[n,S.n] by A6;
hence thesis by A30,A31;
end;
hence thesis;
end;
theorem
for T being non empty TopSpace holds (for S being sequence of T holds
for x1,x2 being Point of T holds (x1 in Lim S & x2 in Lim S implies x1=x2))
implies T is T_1
proof
let T be non empty TopSpace;
assume
A1: for S being sequence of T holds for x1,x2 being Point of T holds (x1
in Lim S & x2 in Lim S implies x1=x2);
assume not T is T_1;
then consider x1,x2 being Point of T,S being sequence of T such that
A2: S = (NAT --> x1) and
A3: x1 <> x2 and
A4: S is_convergent_to x2 by Lm3;
S is_convergent_to x1 by A2,FRECHET:22;
then
A5: x1 in Lim S by FRECHET:def 5;
x2 in Lim S by A4,FRECHET:def 5;
hence contradiction by A1,A3,A5;
end;
theorem Th6:
for T being non empty TopSpace st T is T_2 holds for S being
sequence of T, x1,x2 being Point of T holds (x1 in Lim S & x2 in Lim S implies
x1=x2)
proof
let T be non empty TopSpace;
assume
A1: T is T_2;
assume not(for S being sequence of T, x1,x2 being Point of T holds (x1 in
Lim S & x2 in Lim S implies x1=x2));
then consider S being sequence of T such that
A2: ex x1,x2 being Point of T st x1 in Lim S & x2 in Lim S & x1<>x2;
consider x1,x2 being Point of T such that
A3: x1 in Lim S and
A4: x2 in Lim S and
A5: x1<>x2 by A2;
consider U1,U2 being Subset of T such that
A6: U1 is open and
A7: U2 is open and
A8: x1 in U1 and
A9: x2 in U2 and
A10: U1 misses U2 by A1,A5;
S is_convergent_to x1 by A3,FRECHET:def 5;
then consider n1 being Nat such that
A11: for m being Nat st n1 <= m holds S.m in U1 by A6,A8;
S is_convergent_to x2 by A4,FRECHET:def 5;
then consider n2 being Nat such that
A12: for m being Nat st n2 <= m holds S.m in U2 by A7,A9;
reconsider n = max(n1,n2) as Element of NAT by ORDINAL1:def 12;
A13: S.n in U1 by A11,XXREAL_0:25;
A14: S.n in U2 by A12,XXREAL_0:25;
U1 /\ U2 = {} by A10;
hence contradiction by A13,A14,XBOOLE_0:def 4;
end;
theorem
for T being non empty TopSpace st T is first-countable holds T is T_2
iff for S being sequence of T holds for x1,x2 being Point of T holds (x1 in Lim
S & x2 in Lim S implies x1=x2)
proof
let T be non empty TopSpace;
assume
A1: T is first-countable;
thus T is T_2 implies for S being sequence of T holds for x1,x2 being Point
of T holds (x1 in Lim S & x2 in Lim S implies x1=x2) by Th6;
assume
A2: for S being sequence of T holds for x1,x2 being Point of T holds (x1
in Lim S & x2 in Lim S implies x1=x2);
assume not T is T_2;
then consider x1,x2 being Point of T such that
A3: x1 <> x2 and
A4: for U1,U2 being Subset of T st U1 is open & U2 is open & x1 in U1 &
x2 in U2 holds U1 meets U2;
consider B1 being Basis of x1 such that
A5: ex S being Function st dom S = NAT & rng S = B1 & for n,m being
Element of NAT st m >= n holds S.m c= S.n by A1,Lm5;
consider B2 being Basis of x2 such that
A6: ex S being Function st dom S = NAT & rng S = B2 & for n,m being
Element of NAT st m >= n holds S.m c= S.n by A1,Lm5;
consider S1 being Function such that
A7: dom S1 = NAT and
A8: rng S1 = B1 and
A9: for n,m being Element of NAT st m >= n holds S1.m c= S1.n by A5;
consider S2 being Function such that
A10: dom S2 = NAT and
A11: rng S2 = B2 and
A12: for n,m being Element of NAT st m >= n holds S2.m c= S2.n by A6;
defpred P[object,object] means $2 in S1.$1 /\ S2.$1;
A13: for n being object st n in NAT
ex x being object st x in the carrier of T & P[n,x]
proof
let n be object;
set x = the Element of S1.n /\ S2.n;
assume
A14: n in NAT;
then
A15: S1.n in B1 by A7,A8,FUNCT_1:def 3;
then reconsider U1=S1.n as Subset of T;
A16: S2.n in B2 by A10,A11,A14,FUNCT_1:def 3;
then reconsider U2=S2.n as Subset of T;
take x;
reconsider U1 as Subset of T;
reconsider U2 as Subset of T;
A17: U2 is open & x2 in U2 by A16,YELLOW_8:12;
U1 is open & x1 in U1 by A15,YELLOW_8:12;
then U1 meets U2 by A4,A17;
then
A18: U1 /\ U2 <> {};
then x in U1 /\ U2;
hence x in the carrier of T;
thus thesis by A18;
end;
consider S being Function such that
A19: dom S = NAT & rng S c= the carrier of T and
A20: for n being object st n in NAT holds P[n,S.n] from FUNCT_1:sch 6(A13);
reconsider S as sequence of the carrier of T by A19,FUNCT_2:def 1
,RELSET_1:4;
S is_convergent_to x2
proof
let U2 be Subset of T;
assume U2 is open & x2 in U2;
then consider V2 being Subset of T such that
A21: V2 in B2 and
A22: V2 c= U2 by YELLOW_8:13;
consider n being object such that
A23: n in dom S2 and
A24: V2 = S2.n by A11,A21,FUNCT_1:def 3;
reconsider n as Element of NAT by A10,A23;
take n;
let m be Nat;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
S.mm in S1.mm /\ S2.mm & S1.mm /\ S2.mm c= S2.mm by A20,XBOOLE_1:17;
then
A25: S.m in S2.m;
assume n <= m;
then S2.mm c= S2.n by A12;
then S.m in S2.n by A25;
hence S.m in U2 by A22,A24;
end;
then
A26: x2 in Lim S by FRECHET:def 5;
S is_convergent_to x1
proof
let U1 be Subset of T;
assume U1 is open & x1 in U1;
then consider V1 being Subset of T such that
A27: V1 in B1 and
A28: V1 c= U1 by YELLOW_8:13;
consider n being object such that
A29: n in dom S1 and
A30: V1 = S1.n by A8,A27,FUNCT_1:def 3;
reconsider n as Element of NAT by A7,A29;
take n;
let m be Nat;
A31: m in NAT by ORDINAL1:def 12;
then S.m in S1.m /\ S2.m & S1.m /\ S2.m c= S1.m by A20,XBOOLE_1:17;
then
A32: S.m in S1.m;
assume n <= m;
then S1.m c= S1.n by A9,A31;
then S.m in S1.n by A32;
hence S.m in U1 by A28,A30;
end;
then x1 in Lim S by FRECHET:def 5;
hence contradiction by A2,A3,A26;
end;
theorem
for T being non empty TopStruct, S being sequence of T st S is
not convergent holds Lim S = {}
proof
let T be non empty TopStruct, S be sequence of T;
assume
A1: S is not convergent;
set x = the Element of Lim S;
assume
A2: Lim S <> {};
then x in Lim S;
then reconsider x as Point of T;
S is_convergent_to x by A2,FRECHET:def 5;
hence contradiction by A1;
end;
theorem Th9:
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
by FRECHET:24;
theorem
for T being non empty TopStruct,S being sequence of T, x being Point
of T st not S is_convergent_to x holds ex S1 being subsequence of S st for S2
being subsequence of S1 holds not S2 is_convergent_to x
proof
let T be non empty TopStruct,S be sequence of T, x be Point of T;
assume not S is_convergent_to x;
then consider A being Subset of T such that
A1: A is open & x in A and
A2: for n being Nat ex m being Nat st n <= m & not
S.m in A;
defpred P[set] means not $1 in A;
A3: for n being Element of NAT ex m being Element of NAT st n <= m & P[S.m]
proof let n be Element of NAT;
consider m being Nat such that
A4: n <= m & not S.m in A by A2;
reconsider m as Element of NAT by ORDINAL1:def 12;
take m;
thus thesis by A4;
end;
consider S1 being subsequence of S such that
A5: for n being Element of NAT holds P[S1.n] from VALUED_1:sch 1(A3);
take S1;
let S2 be subsequence of S1;
ex U1 being Subset of T st U1 is open & x in U1 &
for n being Nat ex m being Nat st n <= m & not S2.m in U1
proof
take A;
consider NS being increasing sequence of NAT such that
A6: S2=S1*NS by VALUED_0:def 17;
thus A is open & x in A by A1;
let n be Nat;
take n;
thus n <= n;
n in NAT by ORDINAL1:def 12;
then n in dom S2 by NORMSP_1:12;
then S2.n=S1.(NS.n) by A6,FUNCT_1:12;
hence thesis by A5;
end;
hence thesis;
end;
begin ::The Continuous Maps
theorem Th11:
for T1,T2 being non empty TopSpace, f being Function of T1,T2
holds f is continuous implies for S1 being sequence of T1, S2 being sequence of
T2 st S2=f*S1 holds f.:(Lim S1) c= Lim S2
proof
let T1,T2 be non empty TopSpace, f be Function of T1,T2;
assume
A1: f is continuous;
let S1 be sequence of T1, S2 be sequence of T2;
assume
A2: S2=f*S1;
let y be object;
assume
A3: y in f.:(Lim S1);
then reconsider y9=y as Point of T2;
S2 is_convergent_to y9
proof
let U2 be Subset of T2;
assume that
A4: U2 is open and
A5: y9 in U2;
consider x being object such that
A6: x in dom f and
A7: x in Lim S1 and
A8: y = f.x by A3,FUNCT_1:def 6;
A9: x in f"U2 by A5,A6,A8,FUNCT_1:def 7;
reconsider U1=f"U2 as Subset of T1;
[#]T2 <> {};
then
A10: U1 is open by A1,A4,TOPS_2:43;
reconsider x as Point of T1 by A6;
S1 is_convergent_to x by A7,FRECHET:def 5;
then consider n being Nat such that
A11: for m being Nat st n <= m holds S1.m in f"U2 by A10,A9;
take n;
let m be Nat;
A12: m in NAT by ORDINAL1:def 12;
assume n <= m;
then S1.m in f"U2 by A11;
then
A13: f.(S1.m) in U2 by FUNCT_1:def 7;
dom S1 = NAT by FUNCT_2:def 1;
hence S2.m in U2 by A2,A13,FUNCT_1:13,A12;
end;
hence thesis by FRECHET:def 5;
end;
theorem
for T1,T2 being non empty TopSpace, f being Function of T1,T2 st T1 is
sequential holds f is continuous iff for S1 being sequence of T1, S2 being
sequence of T2 st S2=f*S1 holds f.:(Lim S1) c= Lim S2
proof
let T1,T2 be non empty TopSpace, f be Function of T1,T2;
assume
A1: T1 is sequential;
thus f is continuous implies for S1 being sequence of T1, S2 being sequence
of T2 st S2=f*S1 holds f.:(Lim S1) c= Lim S2 by Th11;
assume
A2: for S1 being sequence of T1, S2 being sequence of T2 st S2=f*S1
holds f.:(Lim S1) c= Lim S2;
let B be Subset of T2;
reconsider A=f"B as Subset of T1;
assume
A3: B is closed;
for S being sequence of T1 st S is convergent & rng S c= A holds Lim S c= A
proof
reconsider B9=B as Subset of T2;
let S be sequence of T1;
assume that
S is convergent and
A4: rng S c= A;
set S2=f*S;
rng S2 c= B9
proof
let z be object;
assume z in rng S2;
then consider n being object such that
A5: n in dom S2 and
A6: z = S2.n by FUNCT_1:def 3;
dom S = NAT by NORMSP_1:12;
then S.n in rng S by A5,FUNCT_1:def 3;
then f.(S.n) in B by A4,FUNCT_1:def 7;
hence thesis by A5,A6,FUNCT_1:12;
end;
then
A7: Lim S2 c= B9 by A3,Th9;
let x be object;
A8: dom f = the carrier of T1 by FUNCT_2:def 1;
A9: f.:(Lim S) c= Lim S2 by A2;
assume
A10: x in Lim S;
then f.x in f.:(Lim S) by A8,FUNCT_1:def 6;
then f.x in Lim S2 by A9;
hence thesis by A10,A8,A7,FUNCT_1:def 7;
end;
hence thesis by A1;
end;
begin ::The Sequential Closure Operator
definition
let T be non empty TopStruct, A be Subset of T;
func Cl_Seq A -> Subset of T means
:Def1:
for x being Point of T holds x in
it iff ex S being sequence of T st rng S c= A & x in Lim S;
existence
proof
defpred P[Point of T] means ex S being sequence of T st rng S c=A & $1 in
Lim S;
reconsider X= {x where x is Point of T: P[x]} as Subset of T from DOMAIN_1
:sch 7;
reconsider X as Subset of T;
take X;
let x be Point of T;
thus x in X implies ex S being sequence of T st rng S c= A & x in Lim S
proof
assume x in X;
then
ex x9 being Point of T st x=x9 & ex S being sequence of T st rng S c=
A & x9 in Lim S;
hence thesis;
end;
assume ex S being sequence of T st rng S c= A & x in Lim S;
hence thesis;
end;
uniqueness
proof
let A1,A2 be Subset of T;
assume that
A1: for x being Point of T holds x in A1 iff ex S being sequence of T
st rng S c= A & x in Lim S and
A2: for x being Point of T holds x in A2 iff ex S being sequence of T
st rng S c= A & x in Lim S;
for x being Point of T holds x in A1 iff x in A2
proof
let x be Point of T;
x in A1 iff ex S being sequence of T st rng S c= A & x in Lim S by A1;
hence thesis by A2;
end;
hence thesis by SUBSET_1:3;
end;
end;
theorem Th13:
for T being non empty TopStruct, A being Subset of T, S being
sequence of T, x being Point of T st rng S c= A & x in Lim S holds x in Cl(A)
proof
let T be non empty TopStruct, A be Subset of T, S be sequence of T, x be
Point of T;
assume that
A1: rng S c= A and
A2: x in Lim S;
for O being Subset of T st O is open holds x in O implies A meets O
proof
let O be Subset of T;
assume
A3: O is open;
A4: S is_convergent_to x by A2,FRECHET:def 5;
assume x in O;
then consider n being Nat such that
A5: for m being Nat st n <= m holds S.m in O by A3,A4;
n in NAT by ORDINAL1:def 12;
then n in dom S by NORMSP_1:12;
then
A6: S.n in rng S by FUNCT_1:def 3;
S.n in O by A5;
then S.n in A /\ O by A1,A6,XBOOLE_0:def 4;
hence thesis;
end;
hence thesis by PRE_TOPC:def 7;
end;
theorem Th14:
for T being non empty TopStruct, A being Subset of T holds Cl_Seq(A) c= Cl(A)
proof
let T be non empty TopStruct, A be Subset of T;
let x be object;
assume
A1: x in Cl_Seq(A);
then reconsider x9=x as Point of T;
ex S being sequence of T st rng S c= A & x9 in Lim S by A1,Def1;
hence thesis by Th13;
end;
theorem Th15:
for T being non empty TopStruct, S being sequence of T, S1 being
subsequence of S, x being Point of T holds S is_convergent_to x implies S1
is_convergent_to x
proof
let T be non empty TopStruct, S be sequence of T, S1 be subsequence of S, x
be Point of T;
assume
A1: S is_convergent_to x;
let U1 be Subset of T;
assume U1 is open & x in U1;
then consider n being Nat such that
A2: for m being Nat st n <= m holds S.m in U1 by A1;
take n;
let m be Nat;
assume
A3: n <= m;
m in NAT by ORDINAL1:def 12;
then
A4: m in dom S1 by NORMSP_1:12;
consider NS being increasing sequence of NAT such that
A5: S1 = S * NS by VALUED_0:def 17;
m <= NS.m by SEQM_3:14;
then S.(NS.m) in U1 by A2,A3,XXREAL_0:2;
hence S1.m in U1 by A5,A4,FUNCT_1:12;
end;
theorem Th16:
for T being non empty TopStruct, S being sequence of T, S1 being
subsequence of S holds Lim S c= Lim S1
proof
let T be non empty TopStruct, S be sequence of T, S1 be subsequence of S;
let x be object;
assume
A1: x in Lim S;
then reconsider x9=x as Point of T;
S is_convergent_to x9 by A1,FRECHET:def 5;
then S1 is_convergent_to x9 by Th15;
hence thesis by FRECHET:def 5;
end;
theorem Th17:
for T being non empty TopStruct holds Cl_Seq({}T) = {}
proof
let T be non empty TopStruct;
set x = the Element of Cl_Seq({}T);
assume
A1: Cl_Seq({}T) <> {};
then x in Cl_Seq({}T);
then reconsider x as Point of T;
consider S being sequence of T such that
A2: rng S c= {}T and
x in Lim S by A1,Def1;
rng S = {} by A2;
then dom S = {} by RELAT_1:42;
hence contradiction by NORMSP_1:12;
end;
theorem Th18:
for T being non empty TopStruct, A being Subset of T holds A c= Cl_Seq(A)
proof
let T be non empty TopStruct, A be Subset of T;
let x be object;
assume
A1: x in A;
then reconsider x9=x as Point of T;
ex S being sequence of T st rng S c= A & x9 in Lim S
proof
set S = NAT --> x9;
take S;
{x9} c= A
by A1,TARSKI:def 1;
hence rng S c= A by FUNCOP_1:8;
S is_convergent_to x9 by FRECHET:22;
hence thesis by FRECHET:def 5;
end;
hence thesis by Def1;
end;
theorem Th19:
for T being non empty TopStruct, A,B being Subset of T holds
Cl_Seq(A) \/ Cl_Seq(B) = Cl_Seq(A \/ B)
proof
let T be non empty TopStruct, A,B be Subset of T;
thus Cl_Seq(A) \/ Cl_Seq(B) c= Cl_Seq(A \/ B)
proof
let x be object;
assume
A1: x in Cl_Seq(A) \/ Cl_Seq(B);
per cases by A1,XBOOLE_0:def 3;
suppose
A2: x in Cl_Seq(A);
then reconsider x9=x as Point of T;
consider S being sequence of T such that
A3: rng S c= A and
A4: x9 in Lim S by A2,Def1;
A c= A \/ B by XBOOLE_1:7;
then rng S c= A \/ B by A3;
hence thesis by A4,Def1;
end;
suppose
A5: x in Cl_Seq(B);
then reconsider x9=x as Point of T;
consider S being sequence of T such that
A6: rng S c= B and
A7: x9 in Lim S by A5,Def1;
B c= A \/ B by XBOOLE_1:7;
then rng S c= A \/ B by A6;
hence thesis by A7,Def1;
end;
end;
thus Cl_Seq(A \/ B) c= Cl_Seq(A) \/ Cl_Seq(B)
proof
let x be object;
assume
A8: x in Cl_Seq(A \/ B);
then reconsider x9 = x as Point of T;
consider S being sequence of T such that
A9: rng S c= A \/ B and
A10: x9 in Lim S by A8,Def1;
consider S1 being subsequence of S such that
A11: rng S1 c= A or rng S1 c= B by A9,Th4;
A12: Lim S c= Lim S1 by Th16;
per cases by A11;
suppose
rng S1 c= A;
then x9 in Cl_Seq(A) by A10,A12,Def1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
rng S1 c= B;
then x9 in Cl_Seq(B) by A10,A12,Def1;
hence thesis by XBOOLE_0:def 3;
end;
end;
end;
theorem Th20:
for T being non empty TopStruct holds T is Frechet iff for A
being Subset of T holds Cl(A)=Cl_Seq(A)
proof
let T be non empty TopStruct;
thus T is Frechet implies for A being Subset of T holds Cl(A)=Cl_Seq(A)
proof
assume
A1: T is Frechet;
let A be Subset of T;
reconsider A9=A as Subset of T;
thus Cl(A)c=Cl_Seq(A)
proof
let x be object;
assume
A2: x in Cl(A);
then reconsider x9=x as Point of T;
ex S being sequence of T st rng S c= A9 & x9 in Lim S by A1,A2;
hence thesis by Def1;
end;
thus thesis by Th14;
end;
assume
A3: for A being Subset of T holds Cl(A)=Cl_Seq(A);
let A be Subset of T,x be Point of T;
assume x in Cl(A);
then x in Cl_Seq(A) by A3;
hence thesis by Def1;
end;
theorem Th21:
for T being non empty TopSpace st T is Frechet holds for A,B
being Subset of T holds Cl_Seq({}T) = {} & A c= Cl_Seq(A) & Cl_Seq(A \/ B) =
Cl_Seq(A) \/ Cl_Seq(B) & Cl_Seq(Cl_Seq(A)) = Cl_Seq(A)
proof
let T be non empty TopSpace;
assume
A1: T is Frechet;
let A,B be Subset of T;
thus Cl_Seq({}T) = {} & A c= Cl_Seq(A) & Cl_Seq(A \/ B)=Cl_Seq(A) \/ Cl_Seq(
B) by Th17,Th18,Th19;
thus Cl_Seq(Cl_Seq(A)) = Cl_Seq(Cl(A)) by A1,Th20
.= Cl(Cl(A)) by A1,Th20
.= Cl_Seq(A) by A1,Th20;
end;
theorem Th22:
for T being non empty TopSpace st T is sequential holds (for A
being Subset of T holds Cl_Seq(Cl_Seq(A)) = Cl_Seq(A)) implies T is Frechet
proof
let T be non empty TopSpace;
assume
A1: T is sequential;
assume
A2: for A being Subset of T holds Cl_Seq(Cl_Seq(A)) = Cl_Seq(A);
assume not T is Frechet;
then consider A being Subset of T such that
A3: ex x being Point of T st x in Cl(A) & for S being sequence of T
holds (rng S c= A implies not x in Lim S );
for Sq being sequence of T st Sq is convergent & rng Sq c= Cl_Seq(A)
holds Lim Sq c= Cl_Seq(A)
proof
let Sq be sequence of T;
assume that
Sq is convergent and
A4: rng Sq c= Cl_Seq(A);
let y be object;
assume
A5: y in Lim Sq;
then reconsider y9=y as Point of T;
y9 in Cl_Seq(Cl_Seq(A)) by A4,A5,Def1;
hence thesis by A2;
end;
then
A6: Cl_Seq(A) is closed by A1;
consider x being Point of T such that
A7: x in Cl(A) and
A8: for S being sequence of T holds (rng S c= A implies not x in Lim S ) by A3;
A c= Cl_Seq(A) by Th18;
then x in Cl_Seq(A) by A7,A6,PRE_TOPC:15;
hence contradiction by A8,Def1;
end;
theorem
for T being non empty TopSpace st T is sequential holds T is Frechet
iff for A,B being Subset of T holds Cl_Seq({}T) = {} & A c= Cl_Seq(A) & Cl_Seq(
A \/ B) = Cl_Seq(A) \/ Cl_Seq(B) & Cl_Seq(Cl_Seq(A)) = Cl_Seq(A) by Th21,Th22;
begin ::The Limit
definition
let T be non empty TopSpace, S be sequence of T;
assume
A1: ex x being Point of T st Lim S = {x};
func lim S -> Point of T means
:Def2:
S is_convergent_to it;
existence
proof
consider x being Point of T such that
A2: Lim S = {x} by A1;
take x;
x in {x} by TARSKI:def 1;
hence thesis by A2,FRECHET:def 5;
end;
uniqueness
proof
let x1,x2 be Point of T;
assume that
A3: S is_convergent_to x1 and
A4: S is_convergent_to x2;
consider x being Point of T such that
A5: Lim S = {x} by A1;
A6: x2 in {x} by A4,A5,FRECHET:def 5;
x1 in Lim S by A3,FRECHET:def 5;
then x1=x by A5,TARSKI:def 1;
hence thesis by A6,TARSKI:def 1;
end;
end;
theorem Th24:
for T being non empty TopSpace st T is T_2 for S being sequence
of T st S is convergent holds ex x being Point of T st Lim S = {x}
proof
let T be non empty TopSpace;
assume
A1: T is T_2;
let S be sequence of T;
assume S is convergent;
then consider x being Point of T such that
A2: S is_convergent_to x;
take x;
A3: x in Lim S by A2,FRECHET:def 5;
thus Lim S c= {x}
proof
let y be object;
assume
A4: y in Lim S;
then reconsider y9=y as Point of T;
y9=x by A1,A3,A4,Th6;
hence thesis by TARSKI:def 1;
end;
let y be object;
assume y in {x};
hence thesis by A3,TARSKI:def 1;
end;
theorem Th25:
for T being non empty TopSpace st T is T_2 for S being sequence
of T,x being Point of T holds S is_convergent_to x iff S is convergent & x =
lim S
proof
let T be non empty TopSpace;
assume
A1: T is T_2;
let S be sequence of T, x be Point of T;
thus S is_convergent_to x implies S is convergent & x = lim S
proof
assume
A2: S is_convergent_to x;
hence S is convergent;
then ex y being Point of T st Lim S = {y} by A1,Th24;
hence thesis by A2,Def2;
end;
assume that
A3: S is convergent and
A4: x = lim S;
ex x being Point of T st Lim S = {x} by A1,A3,Th24;
hence thesis by A4,Def2;
end;
theorem
for M being MetrStruct,S being sequence of M holds S is sequence of
TopSpaceMetr(M)
proof
let M be MetrStruct,S be sequence of M;
the carrier of M = the carrier of TopSpaceMetr M by TOPMETR:12;
hence thesis;
end;
theorem
for M being non empty MetrStruct,S being sequence of TopSpaceMetr(M)
holds S is sequence of M by TOPMETR:12;
theorem Th28:
for M being non empty MetrSpace,S being sequence of M, x being
Point of M, S9 being sequence of TopSpaceMetr(M), x9 being Point of
TopSpaceMetr(M) st S = S9 & x = x9 holds S is_convergent_in_metrspace_to x iff
S9 is_convergent_to x9
proof
let M be non empty MetrSpace,S be sequence of M, x be Point of M, S9 be
sequence of TopSpaceMetr(M), x9 be Point of TopSpaceMetr(M);
assume that
A1: S = S9 and
A2: x=x9;
thus S is_convergent_in_metrspace_to x implies S9 is_convergent_to x9
proof
assume
A3: S is_convergent_in_metrspace_to x;
let U1 be Subset of TopSpaceMetr(M);
assume U1 is open & x9 in U1;
then consider r being Real such that
A4: r>0 and
A5: Ball(x,r) c= U1 by A2,TOPMETR:15;
reconsider r as Real;
Ball(x,r) contains_almost_all_sequence S by A3,A4,METRIC_6:15;
then consider n being Nat such that
A6: for m being Nat st n <= m holds S.m in Ball(x,r);
reconsider n as Element of NAT by ORDINAL1:def 12;
take n;
let m be Nat;
assume n <= m;
then S.m in Ball(x,r) by A6;
hence S9.m in U1 by A1,A5;
end;
assume
A7: S9 is_convergent_to x9;
for V being Subset of M st x in V & V in Family_open_set M holds V
contains_almost_all_sequence S
proof
let V be Subset of M;
assume that
A8: x in V and
A9: V in Family_open_set M;
reconsider V9=V as Subset of TopSpaceMetr(M) by TOPMETR:12;
reconsider V9 as Subset of TopSpaceMetr(M);
V9 in the topology of TopSpaceMetr(M) by A9,TOPMETR:12;
then V9 is open;
then consider n being Nat such that
A10: for m being Nat st n <= m holds S9.m in V9 by A2,A7,A8;
take n;
let m be Nat;
assume n <= m;
hence thesis by A1,A10;
end;
hence thesis by METRIC_6:17;
end;
theorem
for M being non empty MetrSpace,Sm being sequence of M, St being
sequence of TopSpaceMetr(M) st Sm=St holds Sm is convergent iff St is
convergent
proof
let M be non empty MetrSpace,Sm be sequence of M, St be sequence of
TopSpaceMetr(M);
assume
A1: Sm=St;
thus Sm is convergent implies St is convergent
proof
assume Sm is convergent;
then consider x being Point of M such that
A2: Sm is_convergent_in_metrspace_to x by METRIC_6:10;
reconsider x9=x as Point of TopSpaceMetr(M) by TOPMETR:12;
St is_convergent_to x9 by A1,A2,Th28;
hence thesis;
end;
assume St is convergent;
then consider x9 being Point of TopSpaceMetr(M) such that
A3: St is_convergent_to x9;
reconsider x=x9 as Point of M by TOPMETR:12;
Sm is_convergent_in_metrspace_to x by A1,A3,Th28;
hence thesis by METRIC_6:9;
end;
theorem
for M being non empty MetrSpace,Sm being sequence of M, St being
sequence of TopSpaceMetr(M) st Sm=St & Sm is convergent holds lim Sm = lim St
proof
let M be non empty MetrSpace,Sm be sequence of M, St be sequence of
TopSpaceMetr(M);
assume that
A1: Sm=St and
A2: Sm is convergent;
set x=lim Sm;
reconsider x9=x as Point of TopSpaceMetr(M) by TOPMETR:12;
Sm is_convergent_in_metrspace_to x by A2,METRIC_6:12;
then TopSpaceMetr(M) is T_2 & St is_convergent_to x9 by A1,Th28,PCOMPS_1:34;
hence thesis by Th25;
end;
begin ::The Cluster Points
definition
let T be TopStruct, S be sequence of T, x be Point of T;
pred x is_a_cluster_point_of S means
for O being Subset of T, n being Nat st O is open & x in O
ex m being Element of NAT st n <= m & S.m
in O;
end;
theorem Th31:
for T being non empty TopStruct, S being sequence of T, x being
Point of T st ex S1 being subsequence of S st S1 is_convergent_to x holds x
is_a_cluster_point_of S
proof
let T be non empty TopStruct, S be sequence of T, x be Point of T;
given S1 being subsequence of S such that
A1: S1 is_convergent_to x;
let O be Subset of T, n be Nat;
assume O is open & x in O;
then consider n1 being Nat such that
A2: for m being Nat st n1 <= m holds S1.m in O by A1;
reconsider n2=max(n1,n) as Element of NAT by ORDINAL1:def 12;
A3: S1.n2 in O by A2,XXREAL_0:25;
consider NS being increasing sequence of NAT such that
A4: S1 = S * NS by VALUED_0:def 17;
take NS.n2;
n <= n2 & n2 <= NS.n2 by SEQM_3:14,XXREAL_0:25;
hence n <= NS.n2 by XXREAL_0:2;
n2 in NAT;
then n2 in dom NS by FUNCT_2:def 1;
hence thesis by A4,A3,FUNCT_1:13;
end;
theorem
for T being non empty TopStruct, S being sequence of T, x being Point
of T st S is_convergent_to x holds x is_a_cluster_point_of S
proof
let T be non empty TopStruct, S be sequence of T, x be Point of T;
assume
A1: S is_convergent_to x;
ex S1 being subsequence of S st S1 is_convergent_to x
proof
reconsider S1=S as subsequence of S by VALUED_0:19;
take S1;
thus thesis by A1;
end;
hence thesis by Th31;
end;
theorem Th33:
for T being non empty TopStruct, S being sequence of T, x being
Point of T, Y being Subset of T st Y = {y where y is Point of T : x in Cl({y})
} & rng S c= Y holds S is_convergent_to x
proof
let T be non empty TopStruct, S be sequence of T, x be Point of T, Y be
Subset of T;
assume that
A1: Y = {y where y is Point of T : x in Cl({y}) } and
A2: rng S c= Y;
let U1 be Subset of T;
assume
A3: U1 is open & x in U1;
take 0;
let m be Nat;
m in NAT by ORDINAL1:def 12;
then m in dom S by NORMSP_1:12;
then S.m in rng S by FUNCT_1:def 3;
then S.m in Y by A2;
then consider y being Point of T such that
A4: y=S.m and
A5: x in Cl({y}) by A1;
assume 0 <= m;
{y} meets U1 by A3,A5,PRE_TOPC:def 7;
hence S.m in U1 by A4,ZFMISC_1:50;
end;
theorem Th34:
for T being non empty TopStruct, S being sequence of T, x,y
being Point of T st for n being Element of NAT holds S.n = y & S
is_convergent_to x holds x in Cl({y})
proof
let T be non empty TopStruct, S be sequence of T, x,y be Point of T;
assume
A1: for n being Element of NAT holds S.n = y & S is_convergent_to x;
for G being Subset of T st G is open holds x in G implies {y} meets G
proof
let G be Subset of T;
assume
A2: G is open;
assume x in G;
then consider n being Nat such that
A3: for m being Nat st n <= m holds S.m in G by A1,A2,FRECHET:def 3;
A4: n in NAT by ORDINAL1:def 12;
S.n in G by A3;
then
A5: y in G by A1,A4;
y in {y} by TARSKI:def 1;
then y in {y} /\ G by A5,XBOOLE_0:def 4;
hence thesis;
end;
hence thesis by PRE_TOPC:def 7;
end;
theorem Th35:
for T being non empty TopStruct, x being Point of T, Y being
Subset of T, S being sequence of T st Y = { y where y is Point of T : x in Cl({
y}) } & rng S misses Y & S is_convergent_to x ex S1 being subsequence of S st
S1 is one-to-one
proof
let T be non empty TopStruct, x be Point of T, Y be Subset of T, S be
sequence of T;
assume that
A1: Y = { y where y is Point of T : x in Cl({y}) } and
A2: rng S /\ Y = {} and
A3: S is_convergent_to x;
defpred P[Nat,set,set] means $3 in NAT & for n1,n2,m being
Element of NAT st n1=$2 & n2=$3 & n2 <= m holds S.m <> S.n1;
A4: for z being set st z in rng S ex n0 being Element of NAT st for m being
Element of NAT st n0 <= m holds z <> S.m
proof
let z be set;
defpred P[set] means $1 = z;
assume
A5: z in rng S;
then reconsider z9=z as Point of T;
assume
for n0 being Element of NAT ex m being Element of NAT st n0 <= m & z = S.m;
then
A6: for n being Element of NAT ex m being Element of NAT st n <= m & P[S.m ];
ex S1 being subsequence of S st for n being Element of NAT holds P[S1.n
] from VALUED_1:sch 1(A6 );
then x in Cl({z9}) by A3,Th15,Th34;
then z9 in Y by A1;
hence contradiction by A2,A5,XBOOLE_0:def 4;
end;
A7: for n being Nat for z1 being set ex z2 being set st P[n,z1, z2]
proof
let n be Nat, z1 be set;
per cases;
suppose
A8: not z1 in NAT;
take 0;
thus 0 in NAT;
let n1,n2,m be Element of NAT;
assume that
A9: n1=z1 and
n2=0 and
n2 <= m;
thus thesis by A8,A9;
end;
suppose
z1 in NAT;
then z1 in dom S by NORMSP_1:12;
then S.z1 in rng S by FUNCT_1:def 3;
then consider n0 being Element of NAT such that
A10: for m being Element of NAT st n0 <= m holds S.z1 <> S.m by A4;
take n0;
thus n0 in NAT;
let n1,n2,m be Element of NAT;
assume n1=z1 & n2=n0 & n2 <= m;
hence thesis by A10;
end;
end;
consider f being Function such that
A11: dom f = NAT and
A12: f.0 = 0 and
A13: for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch
1(A7);
A14: for n being Nat holds f.n is Element of NAT
proof
let n be Nat;
A15: n in NAT by ORDINAL1:def 12;
per cases;
suppose
n = 0;
hence thesis by A12;
end;
suppose
n <> 0;
then 0 < n by NAT_1:3;
then 0 + 1 < n + 1 by XREAL_1:6;
then 1 <= n by NAT_1:13;
then reconsider n1=n-1 as Element of NAT by INT_1:5,A15;
n1 + 1 = n;
hence thesis by A13;
end;
end;
then for n be Nat holds f.n is real;
then reconsider f as Real_Sequence by A11,SEQ_1:2;
f is increasing
proof
let n be Nat;
reconsider nn=n, nn1=n+1 as Element of NAT by ORDINAL1:def 12;
reconsider n2=f.(nn1) as Element of NAT by A14;
reconsider n1=f.nn as Element of NAT by A14;
assume f.n >= f.(n+1);
then n2 <= n1;
then S.n1 <> S.n1 by A13;
hence contradiction;
end;
then reconsider f as increasing sequence of NAT by A14,SEQM_3:13;
take S1=S*f;
A16: for n1,n2 being Element of NAT st n1 < n2 holds S1.n1 <> S1.n2
proof
let n1,n2 be Element of NAT;
reconsider n19=f.n1 as Element of NAT;
n2 in NAT;
then n2 in dom S1 by NORMSP_1:12;
then
A17: S.(f.n2) = S1.n2 by FUNCT_1:12;
assume n1 < n2;
then
A18: n1 + 1 <= n2 by NAT_1:13;
f.(n1+1) <= f.n2
proof
per cases;
suppose
n1+1 = n2;
hence thesis;
end;
suppose
n1 + 1 <> n2;
then n1 + 1 < n2 by A18,XXREAL_0:1;
hence thesis by SEQM_3:1;
end;
end;
then
A19: S.(f.n2) <> S.n19 by A13;
n1 in NAT;
then n1 in dom S1 by NORMSP_1:12;
hence thesis by A19,A17,FUNCT_1:12;
end;
let x1,x2 be object;
assume that
A20: x1 in dom S1 and
A21: x2 in dom S1 and
A22: S1.x1 = S1.x2;
reconsider n2=x2 as Element of NAT by A21;
reconsider n1=x1 as Element of NAT by A20;
assume
A23: x1 <> x2;
per cases by A23,XXREAL_0:1;
suppose
n1 < n2;
hence contradiction by A22,A16;
end;
suppose
n2 < n1;
hence contradiction by A22,A16;
end;
end;
theorem Th36:
for T being non empty TopStruct, S1,S2 being sequence of T st
rng S2 c= rng S1 & S2 is one-to-one ex P being Permutation of NAT st S2*P is
subsequence of S1
proof
let T be non empty TopStruct, S1,S2 be sequence of T;
assume that
A1: rng S2 c= rng S1 and
A2: S2 is one-to-one;
defpred P[object,object] means S2.$1=S1.$2;
A3: for n being object st n in NAT ex u being object st u in NAT & P[n,u]
proof
let n be object;
assume n in NAT;
then n in dom S2 by NORMSP_1:12;
then S2.n in rng S2 by FUNCT_1:def 3;
then consider m being object such that
A4: m in dom S1 and
A5: S2.n = S1.m by A1,FUNCT_1:def 3;
take m;
thus m in NAT by A4;
thus thesis by A5;
end;
consider f being Function such that
A6: dom f = NAT and
A7: rng f c= NAT and
A8: for n being object st n in NAT holds P[n,f.n] from FUNCT_1:sch 6(A3);
reconsider A=rng f as non empty Subset of NAT by A6,A7,RELAT_1:42;
defpred P[Nat,set,set] means for B being non empty Subset of NAT,
m being Element of NAT st m=$2 & B={k where k is Element of NAT:k in rng f & k>
m} holds $3=min B;
A9: f is one-to-one
proof
let x1,x2 be object;
assume that
A10: x1 in dom f and
A11: x2 in dom f and
A12: f.x1 = f.x2;
S2.x2 = S1.(f.x2) by A6,A8,A11;
then
A13: S2.x1 = S2.x2 by A6,A8,A10,A12;
x1 in dom S2 & x2 in dom S2 by A6,A10,A11,NORMSP_1:12;
hence thesis by A2,A13;
end;
A14: for m being Element of NAT holds {k where k is Element of NAT : k in
rng f & k>m} <> {}
proof
let m be Element of NAT;
assume
A15: {k where k is Element of NAT : k in rng f & k>m} = {};
rng f c= m + 1
proof
let x be object;
assume
A16: x in rng f;
then reconsider x9=x as Element of NAT by A7;
x9 < m + 1
proof
assume x9>= m + 1;
then x9 > m by NAT_1:13;
then x9 in {k where k is Element of NAT : k in rng f & k>m} by A16;
hence contradiction by A15;
end;
then x9 in {x99 where x99 is Nat:x99< m+1};
hence thesis by AXIOMS:4;
end;
then rng f is finite;
hence contradiction by A6,A9,CARD_1:59;
end;
A17: for m being Element of NAT holds {k where k is Element of NAT : k in
rng f & k>m} c= NAT
proof
let m be Element of NAT;
let z be object;
assume z in {k where k is Element of NAT : k in rng f & k>m};
then ex k being Element of NAT st k = z & k in rng f & k>m;
hence thesis;
end;
A18: for n being Nat for x being set ex y being set st P[n,x,y]
proof
let n be Nat, x be set;
per cases;
suppose
x in NAT;
then reconsider x9=x as Element of NAT;
set B={k where k is Element of NAT:k in rng f & k>x9};
reconsider B as Subset of NAT by A17;
reconsider B as non empty Subset of NAT by A14;
take min B;
let B9 be non empty Subset of NAT, m be Element of NAT;
assume m=x & B9={k where k is Element of NAT:k in rng f & k>m};
hence thesis;
end;
suppose
A19: not x in NAT;
take 0;
let B be non empty Subset of NAT, m be Element of NAT;
assume that
A20: m=x and
B={k where k is Element of NAT:k in rng f & k>m};
thus thesis by A19,A20;
end;
end;
consider g being Function such that
A21: dom g = NAT and
A22: g.0 = min A and
A23: for n being Nat holds P[n,g.n,g.(n+1)] from RECDEF_1:sch 1(A18);
defpred P[Nat] means g.$1 in NAT;
A24: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume g.k in NAT;
then reconsider m=g.k as Element of NAT;
set B={l where l is Element of NAT:l in rng f & l>m};
reconsider B as Subset of NAT by A17;
reconsider B as non empty Subset of NAT by A14;
g.(k+1)= min B by A23;
hence thesis;
end;
A25: P[0] by A22;
A26: for k being Nat holds P[k] from NAT_1:sch 2(A25,A24);
for n being Nat holds g.n is real
proof
let n be Nat;
g.n in NAT by A26;
then reconsider w = g.n as Element of REAL by XREAL_0:def 1;
w is real;
hence thesis;
end;
then reconsider g1=g as Real_Sequence by A21,SEQ_1:2;
A27: g1 is increasing
proof
let n be Nat;
reconsider m=g.n as Element of NAT by A26;
reconsider B={k where k is Element of NAT : k in rng f & k>m} as non empty
Subset of NAT by A14,A17;
g1.(n+1)=min B by A23;
then g1.(n+1) in B by XXREAL_2:def 7;
then ex k being Element of NAT st k = g1.(n+1) & k in rng f & k>m;
hence thesis;
end;
A28: rng g c= NAT
proof
let y be object;
assume y in rng g;
then consider x being object such that
A29: x in dom g and
A30: y = g.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A21,A29;
g.x in NAT by A26;
hence thesis by A30;
end;
then reconsider g1 as increasing sequence of NAT by A21,A27,RELSET_1:4;
A31: g1 is one-to-one
proof
let x1,x2 be object;
assume that
A32: x1 in dom g1 and
A33: x2 in dom g1 and
A34: g1.x1 = g1.x2;
reconsider n2=x2 as Element of NAT by A33;
reconsider n1=x1 as Element of NAT by A32;
assume
A35: x1 <> x2;
per cases by A35,XXREAL_0:1;
suppose
n1 < n2;
hence contradiction by A34,SEQM_3:1;
end;
suppose
n2 < n1;
hence contradiction by A34,SEQM_3:1;
end;
end;
then
A36: rng(g") = NAT by A21,FUNCT_1:33;
A37: rng f = rng g
proof
thus for y being object holds y in rng f implies y in rng g
proof
let y be object;
assume
A38: y in rng f;
then reconsider y9=y as Element of NAT by A7;
defpred P[Nat] means g1.$1 < y9;
assume
A39: not y in rng g;
A40: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
reconsider m = g.n as Element of NAT by A26;
reconsider B={k where k is Element of NAT:k in rng f & k>m} as non
empty Subset of NAT by A14,A17;
A41: g.(n+1)=min B & g.(n+1) in rng g by A21,A23,FUNCT_1:def 3;
assume g1.n < y9;
then y9 in {k where k is Element of NAT:k in rng f & k>m} by A38;
then
A42: min B <= y9 by XXREAL_2:def 7;
assume not g1.(n+1) < y9;
hence contradiction by A39,A42,A41,XXREAL_0:1;
end;
A43: P[0]
proof
assume
A44: not g1.0 < y9;
min A <= y9 & g.0 in rng g by A21,A38,FUNCT_1:def 3,XXREAL_2:def 7;
hence contradiction by A22,A39,A44,XXREAL_0:1;
end;
A45: for n being Nat holds P[n] from NAT_1:sch 2(A43,A40);
rng g c= y9
proof
let y be object;
assume y in rng g;
then consider x being object such that
A46: x in dom g and
A47: y = g.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A21,A46;
g1.x < y9 by A45;
then g1.x in {i where i is Nat:i<y9};
hence thesis by A47,AXIOMS:4;
end;
then rng g is finite;
hence contradiction by A21,A31,CARD_1:59;
end;
let y be object;
assume y in rng g;
then consider x being object such that
A48: x in dom g and
A49: y = g.x by FUNCT_1:def 3;
reconsider n=x as Element of NAT by A21,A48;
per cases;
suppose
n=0;
hence thesis by A22,A49,XXREAL_2:def 7;
end;
suppose
n<>0;
then n > 0 by NAT_1:3;
then n + 1 > 0 + 1 by XREAL_1:6;
then 1 <= n by NAT_1:13;
then reconsider m=n-1 as Element of NAT by INT_1:5;
reconsider l = g.m as Element of NAT by A26;
reconsider B={k where k is Element of NAT:k in rng f & k>l} as non empty
Subset of NAT by A14,A17;
m+1 = n;
then g.n = min B by A23;
then y in B by A49,XXREAL_2:def 7;
then ex k being Element of NAT st k = y & k in rng f & k>l;
hence thesis;
end;
end;
then
A50: rng f = dom(g") by A31,FUNCT_1:33;
then dom(g"*f) = dom f & rng(g"*f) = rng(g") by RELAT_1:27,28;
then reconsider P=g"*f as sequence of NAT by A6,A36,FUNCT_2:def 1
,RELSET_1:4;
rng(g") = dom g by A31,FUNCT_1:33;
then rng P = NAT by A21,A50,RELAT_1:28;
then P is onto by FUNCT_2:def 3;
then reconsider P as Permutation of NAT by A9,A31;
take P";
NAT = dom (S2*P") & NAT = dom (S1*g) & for x being object st x in NAT
holds (S2*P").x = (S1*g).x
proof
thus NAT = dom (S2*(P")) by FUNCT_2:def 1;
rng g c= dom S1 by A28,NORMSP_1:12;
hence NAT = dom (S1*g) by A21,RELAT_1:27;
let x be object;
assume
A51: x in NAT;
then
A52: g. x in rng g by A21,FUNCT_1:def 3;
then
A53: f".(g.x) in dom f by A9,A37,FUNCT_1:32;
dom (P") = NAT by FUNCT_2:def 1;
hence (S2*(P")).x = S2.(((g"*f)").x) by A51,FUNCT_1:13
.= S2.((f"*(g")").x) by A9,A31,FUNCT_1:44
.= S2.((f"*g).x) by A31,FUNCT_1:43
.= S2.(f".(g.x)) by A21,A51,FUNCT_1:13
.= S1.(f.(f".(g.x))) by A6,A8,A53
.= S1.(g.x) by A9,A37,A52,FUNCT_1:35
.= (S1*g).x by A21,A51,FUNCT_1:13;
end;
then S2*(P")=S1*g1;
hence thesis;
end;
scheme
PermSeq {T()->non empty 1-sorted,S()->sequence of T(),p()->Permutation of
NAT, P[set]} : ex n being Element of NAT st for m being Element of NAT st n<=m
holds P[(S()*p()).m]
provided
A1: ex n being Element of NAT st for m being Element of NAT, x being
Point of T() st n<=m & x=S().m holds P[x]
proof
consider n being Element of NAT such that
A2: for m being Element of NAT, x being Point of T() st n<=m & x=S().m
holds P[x] by A1;
n in succ n & dom (p()") = NAT by FUNCT_2:def 1,ORDINAL1:6;
then (p()").n in (p()").:(succ n) by FUNCT_1:def 6;
then reconsider X=(p()").:(succ n) as finite non empty Subset of NAT;
reconsider mX = (max X) + 1 as Element of NAT;
take mX;
let m be Element of NAT;
m in NAT;
then
A3: m in dom p() by FUNCT_2:52;
assume
A4: mX<=m;
n<=p().m
proof
assume p().m<n;
then p().m in {p1 where p1 is Nat : p1 < n};
then p().m in n by AXIOMS:4;
then p().m in succ n by ORDINAL1:8;
then m in p()"(succ n) by A3,FUNCT_1:def 7;
then m in (p()").:(succ n) by FUNCT_1:85;
then m <=max X by XXREAL_2:def 8;
hence contradiction by A4,NAT_1:13;
end;
then
A5: P[S().(p().m)] by A2;
m in NAT;
then m in dom p() by FUNCT_2:def 1;
hence thesis by A5,FUNCT_1:13;
end;
scheme
PermSeq2 {T()->non empty TopStruct,S()->sequence of T(),p()->Permutation of
NAT, P[set]} : ex n being Element of NAT st for m being Element of NAT st n<=m
holds P[(S()*p()).m]
provided
A1: ex n being Element of NAT st for m being Element of NAT, x being
Point of T() st n<=m & x=S().m holds P[x]
proof
reconsider T1=T() as non empty 1-sorted;
reconsider S1=S() as sequence of T1;
A2: ex n being Element of NAT st for m being Element of NAT, x being Point
of T1 st n<=m & x=S1.m holds P[x] by A1;
ex n being Element of NAT st for m being Element of NAT st n<=m holds P[
(S1*p()).m] from PermSeq(A2);
hence thesis;
end;
theorem Th37:
for T being non empty TopStruct, S being sequence of T, P being
Permutation of NAT, x being Point of T st S is_convergent_to x holds S*P
is_convergent_to x
proof
let T be non empty TopStruct, S be sequence of T, P be Permutation of NAT, x
be Point of T;
assume
A1: S is_convergent_to x;
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*P).m in U1
proof
let U1 be Subset of T;
defpred P[set] means $1 in U1;
assume
A2: U1 is open & x in U1;
A3: ex n being Element of NAT st for m being Element of NAT, x being Point
of T st n<=m & x=S.m holds P[x]
proof
consider n being Nat such that
A4: for m being Nat st n<=m holds S.m in U1 by A1,A2;
reconsider n as Element of NAT by ORDINAL1:def 12;
take n;
let m be Element of NAT, x be Point of T;
assume n<=m & x=S.m;
hence thesis by A4;
end;
consider n being Element of NAT such that
A5: for m being Element of NAT st n <= m holds P[(S*P).m] from PermSeq2(A3);
take n;
let m be Nat;
m in NAT by ORDINAL1:def 12;
hence thesis by A5;
end;
hence thesis;
end;
theorem
for n0 being Element of NAT ex NS being increasing sequence of NAT st
for n being Element of NAT holds NS.n=n+n0
proof
let n0 be Element of NAT;
deffunc F(Nat) = $1 + n0;
consider NS being Real_Sequence such that
A1: for n being Nat holds NS.n=F(n) from SEQ_1:sch 1;
A2: NS is increasing
proof
let n be Nat;
n < n + 1 by NAT_1:13;
then n + n0 < (n+1) + n0 by XREAL_1:6;
then NS.n < (n+1) + n0 by A1;
hence thesis by A1;
end;
for n being Nat holds NS.n is Element of NAT
proof
let n be Nat;
n + n0 in NAT;
hence thesis by A1;
end;
then reconsider NS as increasing sequence of NAT by A2,SEQM_3:13;
take NS;
thus thesis by A1;
end;
theorem Th39:
for T being non empty TopStruct, S being sequence of T, x being
Point of T, n0 being Nat st x is_a_cluster_point_of S holds x
is_a_cluster_point_of S^\n0
proof
let T be non empty TopStruct, S be sequence of T, x be Point of T, n0 be Nat;
assume
A1: x is_a_cluster_point_of S;
set S1 = S^\n0;
let O be Subset of T, n be Nat;
assume O is open & x in O;
then consider m0 being Element of NAT such that
A2: n + n0 <= m0 and
A3: S.m0 in O by A1;
n0 in NAT & n0 <= n + n0 by NAT_1:11,ORDINAL1:def 12;
then reconsider m=m0-n0 as Element of NAT by A2,INT_1:5,XXREAL_0:2;
take m;
thus n <= m by A2,XREAL_1:19;
S1.m = S.(m0-n0+n0) by NAT_1:def 3
.= S.m0;
hence thesis by A3;
end;
theorem Th40:
for T being non empty TopStruct, S being sequence of T, x being
Point of T st x is_a_cluster_point_of S holds x in Cl(rng S)
proof
let T be non empty TopStruct, S be sequence of T, x be Point of T;
assume
A1: x is_a_cluster_point_of S;
for G being Subset of T st G is open holds x in G implies rng S meets G
proof
let G be Subset of T;
assume
A2: G is open;
assume x in G;
then consider m being Element of NAT such that
0 <= m and
A3: S.m in G by A1,A2;
m in NAT;
then m in dom S by NORMSP_1:12;
then S.m in rng S by FUNCT_1:def 3;
then S.m in rng S /\ G by A3,XBOOLE_0:def 4;
hence thesis;
end;
hence thesis by PRE_TOPC:def 7;
end;
theorem
for T being non empty TopStruct st T is Frechet for S being sequence
of T, x being Point of T st x is_a_cluster_point_of S holds ex S1 being
subsequence of S st S1 is_convergent_to x
proof
let T be non empty TopStruct;
assume
A1: T is Frechet;
let S be sequence of T, x be Point of T;
assume
A2: x is_a_cluster_point_of S;
defpred P[Point of T] means x in Cl{$1};
reconsider Y={y where y is Point of T : P[y]} as Subset of T from DOMAIN_1:
sch 7;
per cases;
suppose
A3: for n being Element of NAT ex m being Element of NAT st m >= n & S .m in Y;
defpred P[set] means $1 in Y;
A4: for n being Element of NAT ex m being Element of NAT st n <= m & P[S.m
] by A3;
consider S1 being subsequence of S such that
A5: for n being Element of NAT holds P[S1.n] from VALUED_1:sch 1(A4);
take S1;
rng S1 c= Y
proof
let y be object;
assume y in rng S1;
then consider n being object such that
A6: n in dom S1 and
A7: y = S1.n by FUNCT_1:def 3;
reconsider n as Element of NAT by A6;
S1.n in Y by A5;
hence thesis by A7;
end;
hence thesis by Th33;
end;
suppose
ex n being Element of NAT st for m being Element of NAT st m >= n
holds not S.m in Y;
then consider n0 being Element of NAT such that
A8: for m being Element of NAT st m >= n0 holds not S.m in Y;
set S9 = S^\n0;
x in Cl(rng S9) by A2,Th39,Th40;
then consider S2 being sequence of T such that
A9: rng S2 c= rng S9 and
A10: x in Lim S2 by A1;
A11: S2 is_convergent_to x by A10,FRECHET:def 5;
A12: for n being Element of NAT holds not S9.n in Y
proof
let n be Element of NAT;
not S.(n+n0) in Y by A8,NAT_1:11;
hence thesis by NAT_1:def 3;
end;
rng S9 /\ Y = {}
proof
set y = the Element of rng S9 /\ Y;
assume
A13: rng S9 /\ Y <> {};
then y in rng S9 by XBOOLE_0:def 4;
then consider n being object such that
A14: n in dom S9 and
A15: y = S9.n by FUNCT_1:def 3;
reconsider n as Element of NAT by A14;
not S9.n in Y by A12;
hence contradiction by A13,A15,XBOOLE_0:def 4;
end;
then rng S9 misses Y;
then consider S29 being subsequence of S2 such that
A16: S29 is one-to-one by A9,A11,Th35,XBOOLE_1:63;
rng S29 c= rng S2 by VALUED_0:21;
then consider P being Permutation of NAT such that
A17: S29*P is subsequence of S9 by A9,A16,Th36,XBOOLE_1:1;
reconsider S1=S29*P as subsequence of S9 by A17;
reconsider S1 as subsequence of S by VALUED_0:20;
take S1;
S29 is_convergent_to x by A11,Th15;
hence thesis by Th37;
end;
end;
begin :: Auxiliary theorems
theorem
for T being non empty TopSpace st T is first-countable holds for x
being Point of T holds ex B being Basis of x st ex S being Function st dom S =
NAT & rng S = B & for n,m being Element of NAT st m >= n holds S.m c= S.n by
Lm5;
theorem
for T being non empty TopSpace st for p being Point of T holds Cl({p})
= {p} holds T is T_1 by Lm1;
theorem
for T being non empty TopSpace holds T is T_2 implies T is T_1 by Lm4;
theorem
for T being non empty TopSpace st not T is T_1 holds ex x1,x2 being
Point of T, S being sequence of T st S = (NAT --> x1) & x1 <> x2 & S
is_convergent_to x2 by Lm3;