:: FRECHET2 semantic presentation
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; ::_thesis: ( ( for p being Point of T holds Cl {p} = {p} ) implies T is T_1 )
assume A1: for p being Point of T holds Cl {p} = {p} ; ::_thesis: T is T_1
for p being Point of T holds {p} is closed
proof
let p be Point of T; ::_thesis: {p} is closed
Cl {p} = {p} by A1;
hence {p} is closed by PRE_TOPC:22; ::_thesis: verum
end;
hence T is T_1 by URYSOHN1:19; ::_thesis: verum
end;
Lm2: for T being non empty TopSpace st not T is T_1 holds
ex x1, x2 being Point of T st
( x1 <> x2 & x2 in Cl {x1} )
proof
let T be non empty TopSpace; ::_thesis: ( not T is T_1 implies ex x1, x2 being Point of T st
( x1 <> x2 & x2 in Cl {x1} ) )
assume not T is T_1 ; ::_thesis: ex x1, x2 being Point of T st
( x1 <> x2 & x2 in Cl {x1} )
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, XBOOLE_0:def_10;
then consider x2 being set such that
A2: x2 in Cl {x1} and
A3: not x2 in {x1} by PRE_TOPC:18, TARSKI:def_3;
reconsider x2 = x2 as Point of T by A2;
take x1 ; ::_thesis: ex x2 being Point of T st
( x1 <> x2 & x2 in Cl {x1} )
take x2 ; ::_thesis: ( x1 <> x2 & x2 in Cl {x1} )
thus x1 <> x2 by A3, TARSKI:def_1; ::_thesis: x2 in Cl {x1}
thus x2 in Cl {x1} by A2; ::_thesis: verum
end;
Lm3: for T being non empty TopSpace st not T is T_1 holds
ex x1, x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 )
proof
let T be non empty TopSpace; ::_thesis: ( not T is T_1 implies ex x1, x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 ) )
assume not T is T_1 ; ::_thesis: ex x1, x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 )
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 ; ::_thesis: ex x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 )
take x2 ; ::_thesis: ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 )
take NAT --> x1 ; ::_thesis: ( NAT --> x1 = NAT --> x1 & x1 <> x2 & NAT --> x1 is_convergent_to x2 )
thus NAT --> x1 = NAT --> x1 ; ::_thesis: ( x1 <> x2 & NAT --> x1 is_convergent_to x2 )
thus x1 <> x2 by A1; ::_thesis: NAT --> x1 is_convergent_to x2
thus NAT --> x1 is_convergent_to x2 ::_thesis: verum
proof
let U1 be Subset of T; :: according to FRECHET:def_3 ::_thesis: ( not U1 is open or not x2 in U1 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or (NAT --> x1) . b2 in U1 ) )
assume A3: ( U1 is open & x2 in U1 ) ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or (NAT --> x1) . b2 in U1 )
take 0 ; ::_thesis: for b1 being Element of NAT holds
( not 0 <= b1 or (NAT --> x1) . b1 in U1 )
{x1} meets U1 by A2, A3, PRE_TOPC:def_7;
then x1 in U1 by ZFMISC_1:50;
hence for b1 being Element of NAT holds
( not 0 <= b1 or (NAT --> x1) . b1 in U1 ) by FUNCOP_1:7; ::_thesis: verum
end;
end;
Lm4: for T being non empty TopSpace st T is T_2 holds
T is T_1
proof
let T be non empty TopSpace; ::_thesis: ( T is T_2 implies T is T_1 )
assume T is T_2 ; ::_thesis: T is T_1
then for p being Point of T holds {p} is closed by PCOMPS_1:7;
hence T is T_1 by URYSOHN1:19; ::_thesis: verum
end;
theorem :: FRECHET2:1
for T being non empty 1-sorted
for S being sequence of T
for NS being increasing sequence of NAT holds S * NS is sequence of T ;
theorem :: FRECHET2:2
for RS being Real_Sequence st RS = id NAT holds
RS is increasing sequence of NAT ;
theorem Th3: :: FRECHET2:3
for T being non empty 1-sorted
for S being sequence of T
for A being Subset of T st ( for S1 being subsequence of S holds not rng S1 c= A ) holds
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 ; ::_thesis: for S being sequence of T
for A being Subset of T st ( for S1 being subsequence of S holds not rng S1 c= A ) holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
not S . m in A
let S be sequence of T; ::_thesis: for A being Subset of T st ( for S1 being subsequence of S holds not rng S1 c= A ) holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
not S . m in A
let A be Subset of T; ::_thesis: ( ( 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 )
assume A1: for S1 being subsequence of S holds not rng S1 c= A ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
not S . m in A
defpred S1[ 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 ) ; ::_thesis: contradiction
then A2: for n being Element of NAT ex m being Element of NAT st
( n <= m & S1[S . m] ) ;
consider S1 being subsequence of S such that
A3: for n being Element of NAT holds S1[S1 . n] from VALUED_1:sch_1(A2);
rng S1 c= A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng S1 or y in A )
assume y in rng S1 ; ::_thesis: y in A
then consider x1 being set 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 y in A by A5; ::_thesis: verum
end;
hence contradiction by A1; ::_thesis: verum
end;
theorem Th4: :: FRECHET2:4
for T being non empty 1-sorted
for S being sequence of T
for 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 ; ::_thesis: for S being sequence of T
for 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 )
let S be sequence of T; ::_thesis: for 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 )
let A, B be Subset of T; ::_thesis: ( rng S c= A \/ B implies ex S1 being subsequence of S st
( rng S1 c= A or rng S1 c= B ) )
assume A1: rng S c= A \/ B ; ::_thesis: ex S1 being subsequence of S st
( rng S1 c= A or rng S1 c= B )
assume A2: for S1 being subsequence of S holds
( not rng S1 c= A & not rng S1 c= B ) ; ::_thesis: contradiction
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; ::_thesis: verum
end;
Lm5: for T being non empty TopSpace st T is first-countable holds
for x being Point of T ex B being Basis of x 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; ::_thesis: ( T is first-countable implies for x being Point of T ex B being Basis of x 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 ) ) )
assume A1: T is first-countable ; ::_thesis: for x being Point of T ex B being Basis of x 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 ) )
let x be Point of T; ::_thesis: ex B being Basis of x 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 ) )
consider B1 being Basis of x such that
A2: B1 is countable by A1, FRECHET:def_2;
consider f being Function of NAT,B1 such that
A3: rng f = B1 by A2, CARD_3:96;
defpred S1[ set , set ] means $2 = meet (f .: (succ $1));
A4: for n being set st n in NAT holds
ex A being set st S1[n,A] ;
consider S being Function such that
A5: dom S = NAT and
A6: for n being set st n in NAT holds
S1[n,S . n] from CLASSES1:sch_1(A4);
A7: rng S c= bool the carrier of T
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in rng S or A in bool the carrier of T )
assume A in rng S ; ::_thesis: A in bool the carrier of T
then consider n being set such that
A8: ( n in dom S & A = S . n ) by FUNCT_1:def_3;
reconsider fsuccn = f .: (succ n) as Subset-Family of T by XBOOLE_1:1;
meet fsuccn = meet (f .: (succ n)) ;
then meet (f .: (succ n)) in bool the carrier of T ;
hence A in bool the carrier of T by A5, A6, A8; ::_thesis: verum
end;
then reconsider B = rng S as Subset-Family of T ;
reconsider B = B as Subset-Family of T ;
A9: ex A being set st A in B
proof
take A = meet (f .: (succ 0)); ::_thesis: A in B
A = S . 0 by A6;
hence A in B by A5, FUNCT_1:def_3; ::_thesis: verum
end;
then A10: 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 ; ::_thesis: ( A in B implies x in A )
assume A in B ; ::_thesis: x in A
then consider n being set such that
A11: n in dom S and
A12: A = S . n by FUNCT_1:def_3;
( dom f = NAT & n in succ n ) by FUNCT_2:def_1, ORDINAL1:6;
then A13: f . n in f .: (succ n) by A5, A11, FUNCT_1:def_6;
A14: for A1 being set st A1 in f .: (succ n) holds
x in A1
proof
let A1 be set ; ::_thesis: ( A1 in f .: (succ n) implies x in A1 )
assume A1 in f .: (succ n) ; ::_thesis: x in A1
then consider m being set such that
A15: m in dom f and
m in succ n and
A16: A1 = f . m by FUNCT_1:def_6;
f . m in rng f by A15, FUNCT_1:def_3;
then reconsider A2 = A1 as Subset of T by A3, A16;
reconsider A2 = A2 as Subset of T ;
A2 in B1 by A3, A15, A16, FUNCT_1:def_3;
hence x in A1 by YELLOW_8:12; ::_thesis: verum
end;
A = meet (f .: (succ n)) by A5, A6, A11, A12;
hence x in A by A14, A13, SETFAM_1:def_1; ::_thesis: verum
end;
then A17: x in meet B by A9, SETFAM_1:def_1;
A18: B c= the topology of T
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in B or A in the topology of T )
assume A in B ; ::_thesis: A in the topology of T
then consider n being set such that
A19: n in dom S and
A20: A = S . n by FUNCT_1:def_3;
reconsider n9 = n as Element of NAT by A5, A19;
reconsider C = f .: (succ n) as Subset-Family of T by XBOOLE_1:1;
A21: C is open
proof
let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not P in C or P is open )
assume P in C ; ::_thesis: P is open
hence P is open by YELLOW_8:12; ::_thesis: verum
end;
succ n9 is finite ;
then f .: (succ n) is finite ;
then A22: meet C is open by A21, TOPS_2:20;
A = meet (f .: (succ n)) by A5, A6, A19, A20;
hence A in the topology of T by A22, PRE_TOPC:def_2; ::_thesis: verum
end;
for O being Subset of T st O is open & x in O holds
ex A being Subset of T st
( A in B & A c= O )
proof
let O be Subset of T; ::_thesis: ( O is open & x in O implies ex A being Subset of T st
( A in B & A c= O ) )
assume ( O is open & x in O ) ; ::_thesis: ex A being Subset of T st
( A in B & A c= O )
then consider A1 being Subset of T such that
A23: A1 in B1 and
A24: A1 c= O by YELLOW_8:def_1;
consider n being set such that
A25: n in dom f and
A26: A1 = f . n by A3, A23, FUNCT_1:def_3;
S . n in rng S by A5, A25, FUNCT_1:def_3;
then reconsider A = S . n as Subset of T by A7;
reconsider A = A as Subset of T ;
take A ; ::_thesis: ( A in B & A c= O )
thus A in B by A5, A25, FUNCT_1:def_3; ::_thesis: A c= O
n in succ n by ORDINAL1:6;
then f . n in f .: (succ n) by A25, FUNCT_1:def_6;
then meet (f .: (succ n)) c= A1 by A26, SETFAM_1:3;
then S . n c= A1 by A6, A25;
hence A c= O by A24, XBOOLE_1:1; ::_thesis: verum
end;
then reconsider B = B as Basis of x by A18, A10, A17, TOPS_2:64, YELLOW_8:def_1;
take B ; ::_thesis: 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 ) )
take S ; ::_thesis: ( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
thus dom S = NAT by A5; ::_thesis: ( rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
thus rng S = B ; ::_thesis: for n, m being Element of NAT st m >= n holds
S . m c= S . n
for n, m being Element of NAT st m >= n holds
S . m c= S . n
proof
let n, m be Element of NAT ; ::_thesis: ( m >= n implies S . m c= S . n )
assume m >= n ; ::_thesis: S . m c= S . n
then n + 1 <= m + 1 by XREAL_1:6;
then n + 1 c= m + 1 by NAT_1:39;
then succ n c= m + 1 by NAT_1:38;
then succ n c= succ m by NAT_1:38;
then A27: 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 meet (f .: (succ m)) c= meet (f .: (succ n)) by A27, SETFAM_1:6;
then S . m c= meet (f .: (succ n)) by A6;
hence S . m c= S . n by A6; ::_thesis: verum
end;
hence for n, m being Element of NAT st m >= n holds
S . m c= S . n ; ::_thesis: verum
end;
theorem :: FRECHET2:5
for T being non empty TopSpace st ( for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 ) holds
T is T_1
proof
let T be non empty TopSpace; ::_thesis: ( ( for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 ) implies T is T_1 )
assume A1: for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 ; ::_thesis: T is T_1
assume not T is T_1 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
theorem Th6: :: FRECHET2:6
for T being non empty TopSpace st T is T_2 holds
for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2
proof
let T be non empty TopSpace; ::_thesis: ( T is T_2 implies for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 )
assume A1: T is T_2 ; ::_thesis: for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2
assume ex S being sequence of T ex x1, x2 being Point of T st
( x1 in Lim S & x2 in Lim S & not x1 = x2 ) ; ::_thesis: contradiction
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, PRE_TOPC:def_10;
S is_convergent_to x1 by A3, FRECHET:def_5;
then consider n1 being Element of NAT such that
A11: for m being Element of NAT st n1 <= m holds
S . m in U1 by A6, A8, FRECHET:def_3;
S is_convergent_to x2 by A4, FRECHET:def_5;
then consider n2 being Element of NAT such that
A12: for m being Element of NAT st n2 <= m holds
S . m in U2 by A7, A9, FRECHET:def_3;
reconsider n = max (n1,n2) as Element of NAT ;
A13: S . n in U1 by A11, XXREAL_0:25;
A14: S . n in U2 by A12, XXREAL_0:25;
U1 /\ U2 = {} by A10, XBOOLE_0:def_7;
hence contradiction by A13, A14, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: FRECHET2:7
for T being non empty TopSpace st T is first-countable holds
( T is T_2 iff for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 )
proof
let T be non empty TopSpace; ::_thesis: ( T is first-countable implies ( T is T_2 iff for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 ) )
assume A1: T is first-countable ; ::_thesis: ( T is T_2 iff for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 )
thus ( T is T_2 implies for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 ) by Th6; ::_thesis: ( ( for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 ) implies T is T_2 )
assume A2: for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 ; ::_thesis: T is T_2
assume not T is T_2 ; ::_thesis: contradiction
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 by PRE_TOPC:def_10;
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 S1[ set , set ] means $2 in (S1 . $1) /\ (S2 . $1);
A13: for n being set st n in NAT holds
ex x being set st
( x in the carrier of T & S1[n,x] )
proof
let n be set ; ::_thesis: ( n in NAT implies ex x being set st
( x in the carrier of T & S1[n,x] ) )
set x = the Element of (S1 . n) /\ (S2 . n);
assume A14: n in NAT ; ::_thesis: ex x being set st
( x in the carrier of T & S1[n,x] )
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 the Element of (S1 . n) /\ (S2 . n) ; ::_thesis: ( the Element of (S1 . n) /\ (S2 . n) in the carrier of T & S1[n, the Element of (S1 . n) /\ (S2 . n)] )
reconsider U1 = U1 as Subset of T ;
reconsider U2 = 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 <> {} by XBOOLE_0:def_7;
then the Element of (S1 . n) /\ (S2 . n) in U1 /\ U2 ;
hence the Element of (S1 . n) /\ (S2 . n) in the carrier of T ; ::_thesis: S1[n, the Element of (S1 . n) /\ (S2 . n)]
thus S1[n, the Element of (S1 . n) /\ (S2 . n)] by A18; ::_thesis: verum
end;
consider S being Function such that
A19: ( dom S = NAT & rng S c= the carrier of T ) and
A20: for n being set st n in NAT holds
S1[n,S . n] from FUNCT_1:sch_5(A13);
reconsider S = S as Function of NAT, 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; :: according to FRECHET:def_3 ::_thesis: ( not U2 is open or not x2 in U2 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or S . b2 in U2 ) )
assume ( U2 is open & x2 in U2 ) ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or S . b2 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 set such that
A23: n in dom S2 and
A24: V2 = S2 . n by A11, A21, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A10, A23;
take n ; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or S . b1 in U2 )
let m be Element of NAT ; ::_thesis: ( not n <= m or S . m in U2 )
( S . m in (S1 . m) /\ (S2 . m) & (S1 . m) /\ (S2 . m) c= S2 . m ) by A20, XBOOLE_1:17;
then A25: S . m in S2 . m ;
assume n <= m ; ::_thesis: S . m in U2
then S2 . m c= S2 . n by A12;
then S . m in S2 . n by A25;
hence S . m in U2 by A22, A24; ::_thesis: verum
end;
then A26: x2 in Lim S by FRECHET:def_5;
S is_convergent_to x1
proof
let U1 be Subset of T; :: according to FRECHET:def_3 ::_thesis: ( not U1 is open or not x1 in U1 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or S . b2 in U1 ) )
assume ( U1 is open & x1 in U1 ) ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or S . b2 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 set such that
A29: n in dom S1 and
A30: V1 = S1 . n by A8, A27, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A7, A29;
take n ; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or S . b1 in U1 )
let m be Element of NAT ; ::_thesis: ( not n <= m or S . m in U1 )
( S . m in (S1 . m) /\ (S2 . m) & (S1 . m) /\ (S2 . m) c= S1 . m ) by A20, XBOOLE_1:17;
then A31: S . m in S1 . m ;
assume n <= m ; ::_thesis: S . m in U1
then S1 . m c= S1 . n by A9;
then S . m in S1 . n by A31;
hence S . m in U1 by A28, A30; ::_thesis: verum
end;
then x1 in Lim S by FRECHET:def_5;
hence contradiction by A2, A3, A26; ::_thesis: verum
end;
theorem :: FRECHET2:8
for T being non empty TopStruct
for S being sequence of T st not S is convergent holds
Lim S = {}
proof
let T be non empty TopStruct ; ::_thesis: for S being sequence of T st not S is convergent holds
Lim S = {}
let S be sequence of T; ::_thesis: ( not S is convergent implies Lim S = {} )
assume A1: not S is convergent ; ::_thesis: Lim S = {}
set x = the Element of Lim S;
assume A2: Lim S <> {} ; ::_thesis: contradiction
then the Element of Lim S in Lim S ;
then reconsider x = the Element of Lim S as Point of T ;
S is_convergent_to x by A2, FRECHET:def_5;
hence contradiction by A1, FRECHET:def_4; ::_thesis: verum
end;
theorem Th9: :: FRECHET2:9
for T being non empty TopSpace
for A being Subset of T st A is closed holds
for S being sequence of T st rng S c= A holds
Lim S c= A by FRECHET:24;
theorem :: FRECHET2:10
for T being non empty TopStruct
for S being sequence of T
for 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 ; ::_thesis: for S being sequence of T
for 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
let S be sequence of T; ::_thesis: for 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
let x be Point of T; ::_thesis: ( not S is_convergent_to x implies ex S1 being subsequence of S st
for S2 being subsequence of S1 holds not S2 is_convergent_to x )
assume not S is_convergent_to x ; ::_thesis: ex S1 being subsequence of S st
for S2 being subsequence of S1 holds not S2 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 Element of NAT ex m being Element of NAT st
( n <= m & not S . m in A ) by FRECHET:def_3;
defpred S1[ set ] means not $1 in A;
A3: for n being Element of NAT ex m being Element of NAT st
( n <= m & S1[S . m] ) by A2;
consider S1 being subsequence of S such that
A4: for n being Element of NAT holds S1[S1 . n] from VALUED_1:sch_1(A3);
take S1 ; ::_thesis: for S2 being subsequence of S1 holds not S2 is_convergent_to x
let S2 be subsequence of S1; ::_thesis: not S2 is_convergent_to x
ex U1 being Subset of T st
( U1 is open & x in U1 & ( for n being Element of NAT ex m being Element of NAT st
( n <= m & not S2 . m in U1 ) ) )
proof
take A ; ::_thesis: ( A is open & x in A & ( for n being Element of NAT ex m being Element of NAT st
( n <= m & not S2 . m in A ) ) )
consider NS being increasing sequence of NAT such that
A5: S2 = S1 * NS by VALUED_0:def_17;
thus ( A is open & x in A ) by A1; ::_thesis: for n being Element of NAT ex m being Element of NAT st
( n <= m & not S2 . m in A )
let n be Element of NAT ; ::_thesis: ex m being Element of NAT st
( n <= m & not S2 . m in A )
take n ; ::_thesis: ( n <= n & not S2 . n in A )
thus n <= n ; ::_thesis: not S2 . n in A
n in NAT ;
then n in dom S2 by NORMSP_1:12;
then S2 . n = S1 . (NS . n) by A5, FUNCT_1:12;
hence not S2 . n in A by A4; ::_thesis: verum
end;
hence not S2 is_convergent_to x by FRECHET:def_3; ::_thesis: verum
end;
begin
theorem Th11: :: FRECHET2:11
for T1, T2 being non empty TopSpace
for f being Function of T1,T2 st f is continuous holds
for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2
proof
let T1, T2 be non empty TopSpace; ::_thesis: for f being Function of T1,T2 st f is continuous holds
for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2
let f be Function of T1,T2; ::_thesis: ( f is continuous implies for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 )
assume A1: f is continuous ; ::_thesis: for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2
let S1 be sequence of T1; ::_thesis: for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2
let S2 be sequence of T2; ::_thesis: ( S2 = f * S1 implies f .: (Lim S1) c= Lim S2 )
assume A2: S2 = f * S1 ; ::_thesis: f .: (Lim S1) c= Lim S2
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: (Lim S1) or y in Lim S2 )
assume A3: y in f .: (Lim S1) ; ::_thesis: y in Lim S2
then reconsider y9 = y as Point of T2 ;
S2 is_convergent_to y9
proof
let U2 be Subset of T2; :: according to FRECHET:def_3 ::_thesis: ( not U2 is open or not y9 in U2 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or S2 . b2 in U2 ) )
assume that
A4: U2 is open and
A5: y9 in U2 ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or S2 . b2 in U2 )
consider x being set 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 = x as Point of T1 by A6;
S1 is_convergent_to x by A7, FRECHET:def_5;
then consider n being Element of NAT such that
A11: for m being Element of NAT st n <= m holds
S1 . m in f " U2 by A10, A9, FRECHET:def_3;
take n ; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or S2 . b1 in U2 )
let m be Element of NAT ; ::_thesis: ( not n <= m or S2 . m in U2 )
assume n <= m ; ::_thesis: S2 . m in U2
then S1 . m in f " U2 by A11;
then A12: 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, A12, FUNCT_1:13; ::_thesis: verum
end;
hence y in Lim S2 by FRECHET:def_5; ::_thesis: verum
end;
theorem :: FRECHET2:12
for T1, T2 being non empty TopSpace
for f being Function of T1,T2 st T1 is sequential holds
( f is continuous iff for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 )
proof
let T1, T2 be non empty TopSpace; ::_thesis: for f being Function of T1,T2 st T1 is sequential holds
( f is continuous iff for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 )
let f be Function of T1,T2; ::_thesis: ( T1 is sequential implies ( f is continuous iff for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 ) )
assume A1: T1 is sequential ; ::_thesis: ( f is continuous iff for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 )
thus ( f is continuous implies for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 ) by Th11; ::_thesis: ( ( for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 ) implies f is continuous )
assume A2: for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 ; ::_thesis: f is continuous
let B be Subset of T2; :: according to PRE_TOPC:def_6 ::_thesis: ( not B is closed or f " B is closed )
reconsider A = f " B as Subset of T1 ;
assume A3: B is closed ; ::_thesis: f " 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; ::_thesis: ( S is convergent & rng S c= A implies Lim S c= A )
assume that
S is convergent and
A4: rng S c= A ; ::_thesis: Lim S c= A
set S2 = f * S;
rng (f * S) c= B9
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (f * S) or z in B9 )
assume z in rng (f * S) ; ::_thesis: z in B9
then consider n being set such that
A5: n in dom (f * S) and
A6: z = (f * S) . 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 z in B9 by A5, A6, FUNCT_1:12; ::_thesis: verum
end;
then A7: Lim (f * S) c= B9 by A3, Th9;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim S or x in A )
A8: dom f = the carrier of T1 by FUNCT_2:def_1;
A9: f .: (Lim S) c= Lim (f * S) by A2;
assume A10: x in Lim S ; ::_thesis: x in A
then f . x in f .: (Lim S) by A8, FUNCT_1:def_6;
then f . x in Lim (f * S) by A9;
hence x in A by A10, A8, A7, FUNCT_1:def_7; ::_thesis: verum
end;
hence f " B is closed by A1, FRECHET:def_7; ::_thesis: verum
end;
begin
definition
let T be non empty TopStruct ;
let A be Subset of T;
func Cl_Seq A -> Subset of T means :Def1: :: FRECHET2:def 1
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
ex b1 being Subset of T st
for x being Point of T holds
( x in b1 iff ex S being sequence of T st
( rng S c= A & x in Lim S ) )
proof
defpred S1[ 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 : S1[x] } as Subset of T from DOMAIN_1:sch_7();
reconsider X = X as Subset of T ;
take X ; ::_thesis: for x being Point of T holds
( x in X iff ex S being sequence of T st
( rng S c= A & x in Lim S ) )
let x be Point of T; ::_thesis: ( x in X iff ex S being sequence of T st
( rng S c= A & x in Lim S ) )
thus ( x in X implies ex S being sequence of T st
( rng S c= A & x in Lim S ) ) ::_thesis: ( ex S being sequence of T st
( rng S c= A & x in Lim S ) implies x in X )
proof
assume x in X ; ::_thesis: ex S being sequence of T st
( rng S c= A & x in Lim S )
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 ex S being sequence of T st
( rng S c= A & x in Lim S ) ; ::_thesis: verum
end;
assume ex S being sequence of T st
( rng S c= A & x in Lim S ) ; ::_thesis: x in X
hence x in X ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of T st ( for x being Point of T holds
( x in b1 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 b2 iff ex S being sequence of T st
( rng S c= A & x in Lim S ) ) ) holds
b1 = b2
proof
let A1, A2 be Subset of T; ::_thesis: ( ( 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 ) ) ) & ( 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 ) ) ) implies A1 = A2 )
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 ) ) ; ::_thesis: A1 = A2
for x being Point of T holds
( x in A1 iff x in A2 )
proof
let x be Point of T; ::_thesis: ( x in A1 iff x in A2 )
( x in A1 iff ex S being sequence of T st
( rng S c= A & x in Lim S ) ) by A1;
hence ( x in A1 iff x in A2 ) by A2; ::_thesis: verum
end;
hence A1 = A2 by SUBSET_1:3; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Cl_Seq FRECHET2:def_1_:_
for T being non empty TopStruct
for A, b3 being Subset of T holds
( b3 = Cl_Seq A iff for x being Point of T holds
( x in b3 iff ex S being sequence of T st
( rng S c= A & x in Lim S ) ) );
theorem Th13: :: FRECHET2:13
for T being non empty TopStruct
for A being Subset of T
for S being sequence of T
for 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 ; ::_thesis: for A being Subset of T
for S being sequence of T
for x being Point of T st rng S c= A & x in Lim S holds
x in Cl A
let A be Subset of T; ::_thesis: for S being sequence of T
for x being Point of T st rng S c= A & x in Lim S holds
x in Cl A
let S be sequence of T; ::_thesis: for x being Point of T st rng S c= A & x in Lim S holds
x in Cl A
let x be Point of T; ::_thesis: ( rng S c= A & x in Lim S implies x in Cl A )
assume that
A1: rng S c= A and
A2: x in Lim S ; ::_thesis: x in Cl A
for O being Subset of T st O is open & x in O holds
A meets O
proof
let O be Subset of T; ::_thesis: ( O is open & x in O implies A meets O )
assume A3: O is open ; ::_thesis: ( not x in O or A meets O )
A4: S is_convergent_to x by A2, FRECHET:def_5;
assume x in O ; ::_thesis: A meets O
then consider n being Element of NAT such that
A5: for m being Element of NAT st n <= m holds
S . m in O by A3, A4, FRECHET:def_3;
n in NAT ;
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 A meets O by XBOOLE_0:def_7; ::_thesis: verum
end;
hence x in Cl A by PRE_TOPC:def_7; ::_thesis: verum
end;
theorem Th14: :: FRECHET2:14
for T being non empty TopStruct
for A being Subset of T holds Cl_Seq A c= Cl A
proof
let T be non empty TopStruct ; ::_thesis: for A being Subset of T holds Cl_Seq A c= Cl A
let A be Subset of T; ::_thesis: Cl_Seq A c= Cl A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl_Seq A or x in Cl A )
assume A1: x in Cl_Seq A ; ::_thesis: x in Cl 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 x in Cl A by Th13; ::_thesis: verum
end;
theorem Th15: :: FRECHET2:15
for T being non empty TopStruct
for S being sequence of T
for S1 being subsequence of S
for x being Point of T st S is_convergent_to x holds
S1 is_convergent_to x
proof
let T be non empty TopStruct ; ::_thesis: for S being sequence of T
for S1 being subsequence of S
for x being Point of T st S is_convergent_to x holds
S1 is_convergent_to x
let S be sequence of T; ::_thesis: for S1 being subsequence of S
for x being Point of T st S is_convergent_to x holds
S1 is_convergent_to x
let S1 be subsequence of S; ::_thesis: for x being Point of T st S is_convergent_to x holds
S1 is_convergent_to x
let x be Point of T; ::_thesis: ( S is_convergent_to x implies S1 is_convergent_to x )
assume A1: S is_convergent_to x ; ::_thesis: S1 is_convergent_to x
let U1 be Subset of T; :: according to FRECHET:def_3 ::_thesis: ( not U1 is open or not x in U1 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or S1 . b2 in U1 ) )
assume ( U1 is open & x in U1 ) ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or S1 . b2 in U1 )
then consider n being Element of NAT such that
A2: for m being Element of NAT st n <= m holds
S . m in U1 by A1, FRECHET:def_3;
take n ; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or S1 . b1 in U1 )
let m be Element of NAT ; ::_thesis: ( not n <= m or S1 . m in U1 )
assume A3: n <= m ; ::_thesis: S1 . m in U1
m in NAT ;
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; ::_thesis: verum
end;
theorem Th16: :: FRECHET2:16
for T being non empty TopStruct
for S being sequence of T
for S1 being subsequence of S holds Lim S c= Lim S1
proof
let T be non empty TopStruct ; ::_thesis: for S being sequence of T
for S1 being subsequence of S holds Lim S c= Lim S1
let S be sequence of T; ::_thesis: for S1 being subsequence of S holds Lim S c= Lim S1
let S1 be subsequence of S; ::_thesis: Lim S c= Lim S1
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim S or x in Lim S1 )
assume A1: x in Lim S ; ::_thesis: x in Lim S1
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 x in Lim S1 by FRECHET:def_5; ::_thesis: verum
end;
theorem Th17: :: FRECHET2:17
for T being non empty TopStruct holds Cl_Seq ({} T) = {}
proof
let T be non empty TopStruct ; ::_thesis: Cl_Seq ({} T) = {}
set x = the Element of Cl_Seq ({} T);
assume A1: Cl_Seq ({} T) <> {} ; ::_thesis: contradiction
then the Element of Cl_Seq ({} T) in Cl_Seq ({} T) ;
then reconsider x = the Element of Cl_Seq ({} T) 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; ::_thesis: verum
end;
theorem Th18: :: FRECHET2:18
for T being non empty TopStruct
for A being Subset of T holds A c= Cl_Seq A
proof
let T be non empty TopStruct ; ::_thesis: for A being Subset of T holds A c= Cl_Seq A
let A be Subset of T; ::_thesis: A c= Cl_Seq A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in Cl_Seq A )
assume A1: x in A ; ::_thesis: 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 )
proof
set S = NAT --> x9;
take NAT --> x9 ; ::_thesis: ( rng (NAT --> x9) c= A & x9 in Lim (NAT --> x9) )
{x9} c= A
proof
let x99 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x99 in {x9} or x99 in A )
assume x99 in {x9} ; ::_thesis: x99 in A
hence x99 in A by A1, TARSKI:def_1; ::_thesis: verum
end;
hence rng (NAT --> x9) c= A by FUNCOP_1:8; ::_thesis: x9 in Lim (NAT --> x9)
NAT --> x9 is_convergent_to x9 by FRECHET:22;
hence x9 in Lim (NAT --> x9) by FRECHET:def_5; ::_thesis: verum
end;
hence x in Cl_Seq A by Def1; ::_thesis: verum
end;
theorem Th19: :: FRECHET2:19
for T being non empty TopStruct
for A, B being Subset of T holds (Cl_Seq A) \/ (Cl_Seq B) = Cl_Seq (A \/ B)
proof
let T be non empty TopStruct ; ::_thesis: for A, B being Subset of T holds (Cl_Seq A) \/ (Cl_Seq B) = Cl_Seq (A \/ B)
let A, B be Subset of T; ::_thesis: (Cl_Seq A) \/ (Cl_Seq B) = Cl_Seq (A \/ B)
thus (Cl_Seq A) \/ (Cl_Seq B) c= Cl_Seq (A \/ B) :: according to XBOOLE_0:def_10 ::_thesis: Cl_Seq (A \/ B) c= (Cl_Seq A) \/ (Cl_Seq B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Cl_Seq A) \/ (Cl_Seq B) or x in Cl_Seq (A \/ B) )
assume A1: x in (Cl_Seq A) \/ (Cl_Seq B) ; ::_thesis: x in Cl_Seq (A \/ B)
percases ( x in Cl_Seq A or x in Cl_Seq B ) by A1, XBOOLE_0:def_3;
supposeA2: x in Cl_Seq A ; ::_thesis: x in Cl_Seq (A \/ B)
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, XBOOLE_1:1;
hence x in Cl_Seq (A \/ B) by A4, Def1; ::_thesis: verum
end;
supposeA5: x in Cl_Seq B ; ::_thesis: x in Cl_Seq (A \/ 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, XBOOLE_1:1;
hence x in Cl_Seq (A \/ B) by A7, Def1; ::_thesis: verum
end;
end;
end;
thus Cl_Seq (A \/ B) c= (Cl_Seq A) \/ (Cl_Seq B) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl_Seq (A \/ B) or x in (Cl_Seq A) \/ (Cl_Seq B) )
assume A8: x in Cl_Seq (A \/ B) ; ::_thesis: x in (Cl_Seq A) \/ (Cl_Seq 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;
percases ( rng S1 c= A or rng S1 c= B ) by A11;
suppose rng S1 c= A ; ::_thesis: x in (Cl_Seq A) \/ (Cl_Seq B)
then x9 in Cl_Seq A by A10, A12, Def1;
hence x in (Cl_Seq A) \/ (Cl_Seq B) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose rng S1 c= B ; ::_thesis: x in (Cl_Seq A) \/ (Cl_Seq B)
then x9 in Cl_Seq B by A10, A12, Def1;
hence x in (Cl_Seq A) \/ (Cl_Seq B) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;
theorem Th20: :: FRECHET2:20
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 ; ::_thesis: ( T is Frechet iff for A being Subset of T holds Cl A = Cl_Seq A )
thus ( T is Frechet implies for A being Subset of T holds Cl A = Cl_Seq A ) ::_thesis: ( ( for A being Subset of T holds Cl A = Cl_Seq A ) implies T is Frechet )
proof
assume A1: T is Frechet ; ::_thesis: for A being Subset of T holds Cl A = Cl_Seq A
let A be Subset of T; ::_thesis: Cl A = Cl_Seq A
reconsider A9 = A as Subset of T ;
thus Cl A c= Cl_Seq A :: according to XBOOLE_0:def_10 ::_thesis: Cl_Seq A c= Cl A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in Cl_Seq A )
assume A2: x in Cl A ; ::_thesis: x in Cl_Seq 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, FRECHET:def_6;
hence x in Cl_Seq A by Def1; ::_thesis: verum
end;
thus Cl_Seq A c= Cl A by Th14; ::_thesis: verum
end;
assume A3: for A being Subset of T holds Cl A = Cl_Seq A ; ::_thesis: T is Frechet
let A be Subset of T; :: according to FRECHET:def_6 ::_thesis: for b1 being Element of the carrier of T holds
( not b1 in Cl A or ex b2 being Element of K10(K11(NAT, the carrier of T)) st
( rng b2 c= A & b1 in Lim b2 ) )
let x be Point of T; ::_thesis: ( not x in Cl A or ex b1 being Element of K10(K11(NAT, the carrier of T)) st
( rng b1 c= A & x in Lim b1 ) )
assume x in Cl A ; ::_thesis: ex b1 being Element of K10(K11(NAT, the carrier of T)) st
( rng b1 c= A & x in Lim b1 )
then x in Cl_Seq A by A3;
hence ex b1 being Element of K10(K11(NAT, the carrier of T)) st
( rng b1 c= A & x in Lim b1 ) by Def1; ::_thesis: verum
end;
theorem Th21: :: FRECHET2:21
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; ::_thesis: ( T is Frechet implies 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 ) )
assume A1: T is Frechet ; ::_thesis: 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 )
let A, B be Subset of T; ::_thesis: ( 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 )
thus ( Cl_Seq ({} T) = {} & A c= Cl_Seq A & Cl_Seq (A \/ B) = (Cl_Seq A) \/ (Cl_Seq B) ) by Th17, Th18, Th19; ::_thesis: Cl_Seq (Cl_Seq A) = Cl_Seq A
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 ; ::_thesis: verum
end;
theorem Th22: :: FRECHET2:22
for T being non empty TopSpace st T is sequential & ( for A being Subset of T holds Cl_Seq (Cl_Seq A) = Cl_Seq A ) holds
T is Frechet
proof
let T be non empty TopSpace; ::_thesis: ( T is sequential & ( for A being Subset of T holds Cl_Seq (Cl_Seq A) = Cl_Seq A ) implies T is Frechet )
assume A1: T is sequential ; ::_thesis: ( ex A being Subset of T st not Cl_Seq (Cl_Seq A) = Cl_Seq A or T is Frechet )
assume A2: for A being Subset of T holds Cl_Seq (Cl_Seq A) = Cl_Seq A ; ::_thesis: T is Frechet
assume not T is Frechet ; ::_thesis: contradiction
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 st rng S c= A holds
not x in Lim S ) ) by FRECHET:def_6;
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; ::_thesis: ( Sq is convergent & rng Sq c= Cl_Seq A implies Lim Sq c= Cl_Seq A )
assume that
Sq is convergent and
A4: rng Sq c= Cl_Seq A ; ::_thesis: Lim Sq c= Cl_Seq A
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Lim Sq or y in Cl_Seq A )
assume A5: y in Lim Sq ; ::_thesis: y in Cl_Seq A
then reconsider y9 = y as Point of T ;
y9 in Cl_Seq (Cl_Seq A) by A4, A5, Def1;
hence y in Cl_Seq A by A2; ::_thesis: verum
end;
then A6: Cl_Seq A is closed by A1, FRECHET:def_7;
consider x being Point of T such that
A7: x in Cl A and
A8: for S being sequence of T st rng S c= A holds
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; ::_thesis: verum
end;
theorem :: FRECHET2:23
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
definition
let T be non empty TopSpace;
let 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: :: FRECHET2:def 2
S is_convergent_to it;
existence
ex b1 being Point of T st S is_convergent_to b1
proof
consider x being Point of T such that
A2: Lim S = {x} by A1;
take x ; ::_thesis: S is_convergent_to x
x in {x} by TARSKI:def_1;
hence S is_convergent_to x by A2, FRECHET:def_5; ::_thesis: verum
end;
uniqueness
for b1, b2 being Point of T st S is_convergent_to b1 & S is_convergent_to b2 holds
b1 = b2
proof
let x1, x2 be Point of T; ::_thesis: ( S is_convergent_to x1 & S is_convergent_to x2 implies x1 = x2 )
assume that
A3: S is_convergent_to x1 and
A4: S is_convergent_to x2 ; ::_thesis: x1 = 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 x1 = x2 by A6, TARSKI:def_1; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines lim FRECHET2:def_2_:_
for T being non empty TopSpace
for S being sequence of T st ex x being Point of T st Lim S = {x} holds
for b3 being Point of T holds
( b3 = lim S iff S is_convergent_to b3 );
theorem Th24: :: FRECHET2:24
for T being non empty TopSpace st T is T_2 holds
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; ::_thesis: ( T is T_2 implies for S being sequence of T st S is convergent holds
ex x being Point of T st Lim S = {x} )
assume A1: T is T_2 ; ::_thesis: for S being sequence of T st S is convergent holds
ex x being Point of T st Lim S = {x}
let S be sequence of T; ::_thesis: ( S is convergent implies ex x being Point of T st Lim S = {x} )
assume S is convergent ; ::_thesis: ex x being Point of T st Lim S = {x}
then consider x being Point of T such that
A2: S is_convergent_to x by FRECHET:def_4;
take x ; ::_thesis: Lim S = {x}
A3: x in Lim S by A2, FRECHET:def_5;
thus Lim S c= {x} :: according to XBOOLE_0:def_10 ::_thesis: {x} c= Lim S
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Lim S or y in {x} )
assume A4: y in Lim S ; ::_thesis: y in {x}
then reconsider y9 = y as Point of T ;
y9 = x by A1, A3, A4, Th6;
hence y in {x} by TARSKI:def_1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {x} or y in Lim S )
assume y in {x} ; ::_thesis: y in Lim S
hence y in Lim S by A3, TARSKI:def_1; ::_thesis: verum
end;
theorem Th25: :: FRECHET2:25
for T being non empty TopSpace st T is T_2 holds
for S being sequence of T
for 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; ::_thesis: ( T is T_2 implies for S being sequence of T
for x being Point of T holds
( S is_convergent_to x iff ( S is convergent & x = lim S ) ) )
assume A1: T is T_2 ; ::_thesis: for S being sequence of T
for x being Point of T holds
( S is_convergent_to x iff ( S is convergent & x = lim S ) )
let S be sequence of T; ::_thesis: for x being Point of T holds
( S is_convergent_to x iff ( S is convergent & x = lim S ) )
let x be Point of T; ::_thesis: ( S is_convergent_to x iff ( S is convergent & x = lim S ) )
thus ( S is_convergent_to x implies ( S is convergent & x = lim S ) ) ::_thesis: ( S is convergent & x = lim S implies S is_convergent_to x )
proof
assume A2: S is_convergent_to x ; ::_thesis: ( S is convergent & x = lim S )
hence S is convergent by FRECHET:def_4; ::_thesis: x = lim S
then ex y being Point of T st Lim S = {y} by A1, Th24;
hence x = lim S by A2, Def2; ::_thesis: verum
end;
assume that
A3: S is convergent and
A4: x = lim S ; ::_thesis: S is_convergent_to x
ex x being Point of T st Lim S = {x} by A1, A3, Th24;
hence S is_convergent_to x by A4, Def2; ::_thesis: verum
end;
theorem :: FRECHET2:26
for M being MetrStruct
for S being sequence of M holds S is sequence of (TopSpaceMetr M)
proof
let M be MetrStruct ; ::_thesis: for S being sequence of M holds S is sequence of (TopSpaceMetr M)
let S be sequence of M; ::_thesis: S is sequence of (TopSpaceMetr M)
the carrier of M = the carrier of (TopSpaceMetr M) by TOPMETR:12;
hence S is sequence of (TopSpaceMetr M) ; ::_thesis: verum
end;
theorem :: FRECHET2:27
for M being non empty MetrStruct
for S being sequence of (TopSpaceMetr M) holds S is sequence of M by TOPMETR:12;
theorem Th28: :: FRECHET2:28
for M being non empty MetrSpace
for S being sequence of M
for x being Point of M
for S9 being sequence of (TopSpaceMetr M)
for 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; ::_thesis: for S being sequence of M
for x being Point of M
for S9 being sequence of (TopSpaceMetr M)
for 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 )
let S be sequence of M; ::_thesis: for x being Point of M
for S9 being sequence of (TopSpaceMetr M)
for 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 )
let x be Point of M; ::_thesis: for S9 being sequence of (TopSpaceMetr M)
for 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 )
let S9 be sequence of (TopSpaceMetr M); ::_thesis: for 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 )
let x9 be Point of (TopSpaceMetr M); ::_thesis: ( S = S9 & x = x9 implies ( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 ) )
assume that
A1: S = S9 and
A2: x = x9 ; ::_thesis: ( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 )
thus ( S is_convergent_in_metrspace_to x implies S9 is_convergent_to x9 ) ::_thesis: ( S9 is_convergent_to x9 implies S is_convergent_in_metrspace_to x )
proof
assume A3: S is_convergent_in_metrspace_to x ; ::_thesis: S9 is_convergent_to x9
let U1 be Subset of (TopSpaceMetr M); :: according to FRECHET:def_3 ::_thesis: ( not U1 is open or not x9 in U1 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or S9 . b2 in U1 ) )
assume ( U1 is open & x9 in U1 ) ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or S9 . b2 in U1 )
then consider r being real number such that
A4: r > 0 and
A5: Ball (x,r) c= U1 by A2, TOPMETR:15;
reconsider r = r as Real by XREAL_0:def_1;
Ball (x,r) contains_almost_all_sequence S by A3, A4, METRIC_6:15;
then consider n being Element of NAT such that
A6: for m being Element of NAT st n <= m holds
S . m in Ball (x,r) by METRIC_6:def_5;
take n ; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or S9 . b1 in U1 )
let m be Element of NAT ; ::_thesis: ( not n <= m or S9 . m in U1 )
assume n <= m ; ::_thesis: S9 . m in U1
then S . m in Ball (x,r) by A6;
hence S9 . m in U1 by A1, A5; ::_thesis: verum
end;
assume A7: S9 is_convergent_to x9 ; ::_thesis: S is_convergent_in_metrspace_to x
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; ::_thesis: ( x in V & V in Family_open_set M implies V contains_almost_all_sequence S )
assume that
A8: x in V and
A9: V in Family_open_set M ; ::_thesis: V contains_almost_all_sequence S
reconsider V9 = V as Subset of (TopSpaceMetr M) by TOPMETR:12;
reconsider V9 = V9 as Subset of (TopSpaceMetr M) ;
V9 in the topology of (TopSpaceMetr M) by A9, TOPMETR:12;
then V9 is open by PRE_TOPC:def_2;
then consider n being Element of NAT such that
A10: for m being Element of NAT st n <= m holds
S9 . m in V9 by A2, A7, A8, FRECHET:def_3;
take n ; :: according to METRIC_6:def_5 ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or S . b1 in V )
let m be Element of NAT ; ::_thesis: ( not n <= m or S . m in V )
assume n <= m ; ::_thesis: S . m in V
hence S . m in V by A1, A10; ::_thesis: verum
end;
hence S is_convergent_in_metrspace_to x by METRIC_6:17; ::_thesis: verum
end;
theorem :: FRECHET2:29
for M being non empty MetrSpace
for Sm being sequence of M
for St being sequence of (TopSpaceMetr M) st Sm = St holds
( Sm is convergent iff St is convergent )
proof
let M be non empty MetrSpace; ::_thesis: for Sm being sequence of M
for St being sequence of (TopSpaceMetr M) st Sm = St holds
( Sm is convergent iff St is convergent )
let Sm be sequence of M; ::_thesis: for St being sequence of (TopSpaceMetr M) st Sm = St holds
( Sm is convergent iff St is convergent )
let St be sequence of (TopSpaceMetr M); ::_thesis: ( Sm = St implies ( Sm is convergent iff St is convergent ) )
assume A1: Sm = St ; ::_thesis: ( Sm is convergent iff St is convergent )
thus ( Sm is convergent implies St is convergent ) ::_thesis: ( St is convergent implies Sm is convergent )
proof
assume Sm is convergent ; ::_thesis: St 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 St is convergent by FRECHET:def_4; ::_thesis: verum
end;
assume St is convergent ; ::_thesis: Sm is convergent
then consider x9 being Point of (TopSpaceMetr M) such that
A3: St is_convergent_to x9 by FRECHET:def_4;
reconsider x = x9 as Point of M by TOPMETR:12;
Sm is_convergent_in_metrspace_to x by A1, A3, Th28;
hence Sm is convergent by METRIC_6:9; ::_thesis: verum
end;
theorem :: FRECHET2:30
for M being non empty MetrSpace
for Sm being sequence of M
for St being sequence of (TopSpaceMetr M) st Sm = St & Sm is convergent holds
lim Sm = lim St
proof
let M be non empty MetrSpace; ::_thesis: for Sm being sequence of M
for St being sequence of (TopSpaceMetr M) st Sm = St & Sm is convergent holds
lim Sm = lim St
let Sm be sequence of M; ::_thesis: for St being sequence of (TopSpaceMetr M) st Sm = St & Sm is convergent holds
lim Sm = lim St
let St be sequence of (TopSpaceMetr M); ::_thesis: ( Sm = St & Sm is convergent implies lim Sm = lim St )
assume that
A1: Sm = St and
A2: Sm is convergent ; ::_thesis: lim Sm = lim St
set x = lim Sm;
reconsider x9 = lim Sm as Point of (TopSpaceMetr M) by TOPMETR:12;
Sm is_convergent_in_metrspace_to lim Sm by A2, METRIC_6:12;
then ( TopSpaceMetr M is T_2 & St is_convergent_to x9 ) by A1, Th28, PCOMPS_1:34;
hence lim Sm = lim St by Th25; ::_thesis: verum
end;
begin
definition
let T be TopStruct ;
let S be sequence of T;
let x be Point of T;
predx is_a_cluster_point_of S means :Def3: :: FRECHET2:def 3
for O being Subset of T
for n being Element of NAT st O is open & x in O holds
ex m being Element of NAT st
( n <= m & S . m in O );
end;
:: deftheorem Def3 defines is_a_cluster_point_of FRECHET2:def_3_:_
for T being TopStruct
for S being sequence of T
for x being Point of T holds
( x is_a_cluster_point_of S iff for O being Subset of T
for n being Element of NAT st O is open & x in O holds
ex m being Element of NAT st
( n <= m & S . m in O ) );
theorem Th31: :: FRECHET2:31
for T being non empty TopStruct
for S being sequence of T
for 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 ; ::_thesis: for S being sequence of T
for 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
let S be sequence of T; ::_thesis: for 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
let x be Point of T; ::_thesis: ( ex S1 being subsequence of S st S1 is_convergent_to x implies x is_a_cluster_point_of S )
given S1 being subsequence of S such that A1: S1 is_convergent_to x ; ::_thesis: x is_a_cluster_point_of S
let O be Subset of T; :: according to FRECHET2:def_3 ::_thesis: for n being Element of NAT st O is open & x in O holds
ex m being Element of NAT st
( n <= m & S . m in O )
let n be Element of NAT ; ::_thesis: ( O is open & x in O implies ex m being Element of NAT st
( n <= m & S . m in O ) )
assume ( O is open & x in O ) ; ::_thesis: ex m being Element of NAT st
( n <= m & S . m in O )
then consider n1 being Element of NAT such that
A2: for m being Element of NAT st n1 <= m holds
S1 . m in O by A1, FRECHET:def_3;
set n2 = max (n1,n);
A3: S1 . (max (n1,n)) 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 . (max (n1,n)) ; ::_thesis: ( n <= NS . (max (n1,n)) & S . (NS . (max (n1,n))) in O )
( n <= max (n1,n) & max (n1,n) <= NS . (max (n1,n)) ) by SEQM_3:14, XXREAL_0:25;
hence n <= NS . (max (n1,n)) by XXREAL_0:2; ::_thesis: S . (NS . (max (n1,n))) in O
max (n1,n) in NAT ;
then max (n1,n) in dom NS by FUNCT_2:def_1;
hence S . (NS . (max (n1,n))) in O by A4, A3, FUNCT_1:13; ::_thesis: verum
end;
theorem :: FRECHET2:32
for T being non empty TopStruct
for S being sequence of T
for 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 ; ::_thesis: for S being sequence of T
for x being Point of T st S is_convergent_to x holds
x is_a_cluster_point_of S
let S be sequence of T; ::_thesis: for x being Point of T st S is_convergent_to x holds
x is_a_cluster_point_of S
let x be Point of T; ::_thesis: ( S is_convergent_to x implies x is_a_cluster_point_of S )
assume A1: S is_convergent_to x ; ::_thesis: x is_a_cluster_point_of S
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 ; ::_thesis: S1 is_convergent_to x
thus S1 is_convergent_to x by A1; ::_thesis: verum
end;
hence x is_a_cluster_point_of S by Th31; ::_thesis: verum
end;
theorem Th33: :: FRECHET2:33
for T being non empty TopStruct
for S being sequence of T
for x being Point of T
for 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 ; ::_thesis: for S being sequence of T
for x being Point of T
for 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
let S be sequence of T; ::_thesis: for x being Point of T
for 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
let x be Point of T; ::_thesis: for 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
let Y be Subset of T; ::_thesis: ( Y = { y where y is Point of T : x in Cl {y} } & rng S c= Y implies S is_convergent_to x )
assume that
A1: Y = { y where y is Point of T : x in Cl {y} } and
A2: rng S c= Y ; ::_thesis: S is_convergent_to x
let U1 be Subset of T; :: according to FRECHET:def_3 ::_thesis: ( not U1 is open or not x in U1 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or S . b2 in U1 ) )
assume A3: ( U1 is open & x in U1 ) ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or S . b2 in U1 )
take 0 ; ::_thesis: for b1 being Element of NAT holds
( not 0 <= b1 or S . b1 in U1 )
let m be Element of NAT ; ::_thesis: ( not 0 <= m or S . m in U1 )
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 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 ; ::_thesis: S . m in U1
{y} meets U1 by A3, A5, PRE_TOPC:def_7;
hence S . m in U1 by A4, ZFMISC_1:50; ::_thesis: verum
end;
theorem Th34: :: FRECHET2:34
for T being non empty TopStruct
for S being sequence of T
for 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 ; ::_thesis: for S being sequence of T
for 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}
let S be sequence of T; ::_thesis: for 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}
let x, y be Point of T; ::_thesis: ( ( for n being Element of NAT holds
( S . n = y & S is_convergent_to x ) ) implies x in Cl {y} )
assume A1: for n being Element of NAT holds
( S . n = y & S is_convergent_to x ) ; ::_thesis: x in Cl {y}
for G being Subset of T st G is open & x in G holds
{y} meets G
proof
let G be Subset of T; ::_thesis: ( G is open & x in G implies {y} meets G )
assume A2: G is open ; ::_thesis: ( not x in G or {y} meets G )
assume x in G ; ::_thesis: {y} meets G
then consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
S . m in G by A1, A2, FRECHET:def_3;
S . n in G by A3;
then A4: y in G by A1;
y in {y} by TARSKI:def_1;
then y in {y} /\ G by A4, XBOOLE_0:def_4;
hence {y} meets G by XBOOLE_0:def_7; ::_thesis: verum
end;
hence x in Cl {y} by PRE_TOPC:def_7; ::_thesis: verum
end;
theorem Th35: :: FRECHET2:35
for T being non empty TopStruct
for x being Point of T
for Y being Subset of T
for 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 holds
ex S1 being subsequence of S st S1 is one-to-one
proof
let T be non empty TopStruct ; ::_thesis: for x being Point of T
for Y being Subset of T
for 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 holds
ex S1 being subsequence of S st S1 is one-to-one
let x be Point of T; ::_thesis: for Y being Subset of T
for 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 holds
ex S1 being subsequence of S st S1 is one-to-one
let Y be Subset of T; ::_thesis: for 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 holds
ex S1 being subsequence of S st S1 is one-to-one
let S be sequence of T; ::_thesis: ( Y = { y where y is Point of T : x in Cl {y} } & rng S misses Y & S is_convergent_to x implies ex S1 being subsequence of S st S1 is one-to-one )
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 ; :: according to XBOOLE_0:def_7 ::_thesis: ex S1 being subsequence of S st S1 is one-to-one
defpred S1[ Element of 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 holds
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 ; ::_thesis: ( z in rng S implies ex n0 being Element of NAT st
for m being Element of NAT st n0 <= m holds
z <> S . m )
defpred S2[ set ] means $1 = z;
assume A5: z in rng S ; ::_thesis: ex n0 being Element of NAT st
for m being Element of NAT st n0 <= m holds
z <> S . m
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 ) ; ::_thesis: contradiction
then A6: for n being Element of NAT ex m being Element of NAT st
( n <= m & S2[S . m] ) ;
ex S1 being subsequence of S st
for n being Element of NAT holds S2[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; ::_thesis: verum
end;
A7: for n being Element of NAT
for z1 being set ex z2 being set st S1[n,z1,z2]
proof
let n be Element of NAT ; ::_thesis: for z1 being set ex z2 being set st S1[n,z1,z2]
let z1 be set ; ::_thesis: ex z2 being set st S1[n,z1,z2]
percases ( not z1 in NAT or z1 in NAT ) ;
supposeA8: not z1 in NAT ; ::_thesis: ex z2 being set st S1[n,z1,z2]
take 0 ; ::_thesis: S1[n,z1, 0 ]
thus 0 in NAT ; ::_thesis: for n1, n2, m being Element of NAT st n1 = z1 & n2 = 0 & n2 <= m holds
S . m <> S . n1
let n1, n2, m be Element of NAT ; ::_thesis: ( n1 = z1 & n2 = 0 & n2 <= m implies S . m <> S . n1 )
assume that
A9: n1 = z1 and
n2 = 0 and
n2 <= m ; ::_thesis: S . m <> S . n1
thus S . m <> S . n1 by A8, A9; ::_thesis: verum
end;
suppose z1 in NAT ; ::_thesis: ex z2 being set st S1[n,z1,z2]
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 ; ::_thesis: S1[n,z1,n0]
thus n0 in NAT ; ::_thesis: for n1, n2, m being Element of NAT st n1 = z1 & n2 = n0 & n2 <= m holds
S . m <> S . n1
let n1, n2, m be Element of NAT ; ::_thesis: ( n1 = z1 & n2 = n0 & n2 <= m implies S . m <> S . n1 )
assume ( n1 = z1 & n2 = n0 & n2 <= m ) ; ::_thesis: S . m <> S . n1
hence S . m <> S . n1 by A10; ::_thesis: verum
end;
end;
end;
consider f being Function such that
A11: dom f = NAT and
A12: f . 0 = 0 and
A13: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch_1(A7);
A14: for n being Element of NAT holds f . n is Element of NAT
proof
let n be Element of NAT ; ::_thesis: f . n is Element of NAT
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: f . n is Element of NAT
hence f . n is Element of NAT by A12; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: f . n is Element of NAT
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;
n1 + 1 = n ;
hence f . n is Element of NAT by A13; ::_thesis: verum
end;
end;
end;
then for n being Element of NAT holds f . n is real ;
then reconsider f = f as Real_Sequence by A11, SEQ_1:2;
f is increasing
proof
let n be Element of NAT ; :: according to SEQM_3:def_6 ::_thesis: not f . (n + 1) <= f . n
reconsider n2 = f . (n + 1) as Element of NAT by A14;
reconsider n1 = f . n as Element of NAT by A14;
assume f . n >= f . (n + 1) ; ::_thesis: contradiction
then n2 <= n1 ;
then S . n1 <> S . n1 by A13;
hence contradiction ; ::_thesis: verum
end;
then reconsider f = f as increasing sequence of NAT by A14, SEQM_3:13;
take S1 = S * f; ::_thesis: S1 is one-to-one
A15: for n1, n2 being Element of NAT st n1 < n2 holds
S1 . n1 <> S1 . n2
proof
let n1, n2 be Element of NAT ; ::_thesis: ( n1 < n2 implies S1 . n1 <> S1 . n2 )
reconsider n19 = f . n1 as Element of NAT ;
n2 in NAT ;
then n2 in dom S1 by NORMSP_1:12;
then A16: S . (f . n2) = S1 . n2 by FUNCT_1:12;
assume n1 < n2 ; ::_thesis: S1 . n1 <> S1 . n2
then A17: n1 + 1 <= n2 by NAT_1:13;
f . (n1 + 1) <= f . n2
proof
percases ( n1 + 1 = n2 or n1 + 1 <> n2 ) ;
suppose n1 + 1 = n2 ; ::_thesis: f . (n1 + 1) <= f . n2
hence f . (n1 + 1) <= f . n2 ; ::_thesis: verum
end;
suppose n1 + 1 <> n2 ; ::_thesis: f . (n1 + 1) <= f . n2
then n1 + 1 < n2 by A17, XXREAL_0:1;
hence f . (n1 + 1) <= f . n2 by SEQM_3:1; ::_thesis: verum
end;
end;
end;
then A18: S . (f . n2) <> S . n19 by A13;
n1 in NAT ;
then n1 in dom S1 by NORMSP_1:12;
hence S1 . n1 <> S1 . n2 by A18, A16, FUNCT_1:12; ::_thesis: verum
end;
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom S1 or not x2 in dom S1 or not S1 . x1 = S1 . x2 or x1 = x2 )
assume that
A19: x1 in dom S1 and
A20: x2 in dom S1 and
A21: S1 . x1 = S1 . x2 ; ::_thesis: x1 = x2
reconsider n2 = x2 as Element of NAT by A20;
reconsider n1 = x1 as Element of NAT by A19;
assume A22: x1 <> x2 ; ::_thesis: contradiction
percases ( n1 < n2 or n2 < n1 ) by A22, XXREAL_0:1;
suppose n1 < n2 ; ::_thesis: contradiction
hence contradiction by A21, A15; ::_thesis: verum
end;
suppose n2 < n1 ; ::_thesis: contradiction
hence contradiction by A21, A15; ::_thesis: verum
end;
end;
end;
theorem Th36: :: FRECHET2:36
for T being non empty TopStruct
for S1, S2 being sequence of T st rng S2 c= rng S1 & S2 is one-to-one holds
ex P being Permutation of NAT st S2 * P is subsequence of S1
proof
let T be non empty TopStruct ; ::_thesis: for S1, S2 being sequence of T st rng S2 c= rng S1 & S2 is one-to-one holds
ex P being Permutation of NAT st S2 * P is subsequence of S1
let S1, S2 be sequence of T; ::_thesis: ( rng S2 c= rng S1 & S2 is one-to-one implies ex P being Permutation of NAT st S2 * P is subsequence of S1 )
assume that
A1: rng S2 c= rng S1 and
A2: S2 is one-to-one ; ::_thesis: ex P being Permutation of NAT st S2 * P is subsequence of S1
defpred S1[ set , set ] means S2 . $1 = S1 . $2;
A3: for n being set st n in NAT holds
ex u being set st
( u in NAT & S1[n,u] )
proof
let n be set ; ::_thesis: ( n in NAT implies ex u being set st
( u in NAT & S1[n,u] ) )
assume n in NAT ; ::_thesis: ex u being set st
( u in NAT & S1[n,u] )
then n in dom S2 by NORMSP_1:12;
then S2 . n in rng S2 by FUNCT_1:def_3;
then consider m being set such that
A4: m in dom S1 and
A5: S2 . n = S1 . m by A1, FUNCT_1:def_3;
take m ; ::_thesis: ( m in NAT & S1[n,m] )
thus m in NAT by A4; ::_thesis: S1[n,m]
thus S1[n,m] by A5; ::_thesis: verum
end;
consider f being Function such that
A6: dom f = NAT and
A7: rng f c= NAT and
A8: for n being set st n in NAT holds
S1[n,f . n] from FUNCT_1:sch_5(A3);
reconsider A = rng f as non empty Subset of NAT by A6, A7, RELAT_1:42;
defpred S2[ Element of NAT , set , set ] means for B being non empty Subset of NAT
for 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 set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A10: x1 in dom f and
A11: x2 in dom f and
A12: f . x1 = f . x2 ; ::_thesis: x1 = 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 x1 = x2 by A2, A13, FUNCT_1:def_4; ::_thesis: verum
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 ; ::_thesis: { k where k is Element of NAT : ( k in rng f & k > m ) } <> {}
assume A15: { k where k is Element of NAT : ( k in rng f & k > m ) } = {} ; ::_thesis: contradiction
rng f c= m + 1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in m + 1 )
assume A16: x in rng f ; ::_thesis: x in m + 1
then reconsider x9 = x as Element of NAT by A7;
x9 < m + 1
proof
assume x9 >= m + 1 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
then x9 in { x99 where x99 is Element of NAT : x99 < m + 1 } ;
hence x in m + 1 by AXIOMS:4; ::_thesis: verum
end;
then rng f is finite ;
hence contradiction by A6, A9, CARD_1:59; ::_thesis: verum
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 ; ::_thesis: { k where k is Element of NAT : ( k in rng f & k > m ) } c= NAT
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { k where k is Element of NAT : ( k in rng f & k > m ) } or z in NAT )
assume z in { k where k is Element of NAT : ( k in rng f & k > m ) } ; ::_thesis: z in NAT
then ex k being Element of NAT st
( k = z & k in rng f & k > m ) ;
hence z in NAT ; ::_thesis: verum
end;
A18: for n being Element of NAT
for x being set ex y being set st S2[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being set ex y being set st S2[n,x,y]
let x be set ; ::_thesis: ex y being set st S2[n,x,y]
percases ( x in NAT or not x in NAT ) ;
suppose x in NAT ; ::_thesis: ex y being set st S2[n,x,y]
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 = { k where k is Element of NAT : ( k in rng f & k > x9 ) } as Subset of NAT by A17;
reconsider B = B as non empty Subset of NAT by A14;
take min B ; ::_thesis: S2[n,x, min B]
let B9 be non empty Subset of NAT; ::_thesis: for m being Element of NAT st m = x & B9 = { k where k is Element of NAT : ( k in rng f & k > m ) } holds
min B = min B9
let m be Element of NAT ; ::_thesis: ( m = x & B9 = { k where k is Element of NAT : ( k in rng f & k > m ) } implies min B = min B9 )
assume ( m = x & B9 = { k where k is Element of NAT : ( k in rng f & k > m ) } ) ; ::_thesis: min B = min B9
hence min B = min B9 ; ::_thesis: verum
end;
supposeA19: not x in NAT ; ::_thesis: ex y being set st S2[n,x,y]
take 0 ; ::_thesis: S2[n,x, 0 ]
let B be non empty Subset of NAT; ::_thesis: for m being Element of NAT st m = x & B = { k where k is Element of NAT : ( k in rng f & k > m ) } holds
0 = min B
let m be Element of NAT ; ::_thesis: ( m = x & B = { k where k is Element of NAT : ( k in rng f & k > m ) } implies 0 = min B )
assume that
A20: m = x and
B = { k where k is Element of NAT : ( k in rng f & k > m ) } ; ::_thesis: 0 = min B
thus 0 = min B by A19, A20; ::_thesis: verum
end;
end;
end;
consider g being Function such that
A21: dom g = NAT and
A22: g . 0 = min A and
A23: for n being Element of NAT holds S2[n,g . n,g . (n + 1)] from RECDEF_1:sch_1(A18);
defpred S3[ Element of NAT ] means g . $1 in NAT ;
A24: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] )
assume g . k in NAT ; ::_thesis: S3[k + 1]
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 = { l where l is Element of NAT : ( l in rng f & l > m ) } as Subset of NAT by A17;
reconsider B = B as non empty Subset of NAT by A14;
g . (k + 1) = min B by A23;
hence S3[k + 1] ; ::_thesis: verum
end;
A25: S3[ 0 ] by A22;
A26: for k being Element of NAT holds S3[k] from NAT_1:sch_1(A25, A24);
for n being Element of NAT holds g . n is real
proof
let n be Element of NAT ; ::_thesis: g . n is real
g . n in NAT by A26;
then reconsider w = g . n as Element of REAL ;
w is real ;
hence g . n is real ; ::_thesis: verum
end;
then reconsider g1 = g as Real_Sequence by A21, SEQ_1:2;
A27: g1 is increasing
proof
let n be Element of NAT ; :: according to SEQM_3:def_6 ::_thesis: not g1 . (n + 1) <= g1 . n
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 not g1 . (n + 1) <= g1 . n ; ::_thesis: verum
end;
A28: rng g c= NAT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in NAT )
assume y in rng g ; ::_thesis: y in NAT
then consider x being set such that
A29: x in dom g and
A30: y = g . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A21, A29;
g . x in NAT by A26;
hence y in NAT by A30; ::_thesis: verum
end;
then reconsider g1 = g1 as increasing sequence of NAT by A21, A27, RELSET_1:4;
A31: g1 is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom g1 or not x2 in dom g1 or not g1 . x1 = g1 . x2 or x1 = x2 )
assume that
A32: x1 in dom g1 and
A33: x2 in dom g1 and
A34: g1 . x1 = g1 . x2 ; ::_thesis: x1 = x2
reconsider n2 = x2 as Element of NAT by A33;
reconsider n1 = x1 as Element of NAT by A32;
assume A35: x1 <> x2 ; ::_thesis: contradiction
percases ( n1 < n2 or n2 < n1 ) by A35, XXREAL_0:1;
suppose n1 < n2 ; ::_thesis: contradiction
hence contradiction by A34, SEQM_3:1; ::_thesis: verum
end;
suppose n2 < n1 ; ::_thesis: contradiction
hence contradiction by A34, SEQM_3:1; ::_thesis: verum
end;
end;
end;
then A36: rng (g ") = NAT by A21, FUNCT_1:33;
A37: rng f = rng g
proof
thus for y being set st y in rng f holds
y in rng g :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: rng g c= rng f
proof
let y be set ; ::_thesis: ( y in rng f implies y in rng g )
assume A38: y in rng f ; ::_thesis: y in rng g
then reconsider y9 = y as Element of NAT by A7;
defpred S4[ Element of NAT ] means g1 . $1 < y9;
assume A39: not y in rng g ; ::_thesis: contradiction
A40: for n being Element of NAT st S4[n] holds
S4[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S4[n] implies S4[n + 1] )
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 ; ::_thesis: S4[n + 1]
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 ; ::_thesis: contradiction
hence contradiction by A39, A42, A41, XXREAL_0:1; ::_thesis: verum
end;
A43: S4[ 0 ]
proof
assume A44: not g1 . 0 < y9 ; ::_thesis: contradiction
( 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; ::_thesis: verum
end;
A45: for n being Element of NAT holds S4[n] from NAT_1:sch_1(A43, A40);
rng g c= y9
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in y9 )
assume y in rng g ; ::_thesis: y in y9
then consider x being set such that
A46: x in dom g and
A47: y = g . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A21, A46;
g1 . x < y9 by A45;
then g1 . x in { i where i is Element of NAT : i < y9 } ;
hence y in y9 by A47, AXIOMS:4; ::_thesis: verum
end;
then rng g is finite ;
hence contradiction by A21, A31, CARD_1:59; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in rng f )
assume y in rng g ; ::_thesis: y in rng f
then consider x being set 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;
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: y in rng f
hence y in rng f by A22, A49, XXREAL_2:def_7; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: y in rng f
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 y in rng f ; ::_thesis: verum
end;
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, RELAT_1:28;
then reconsider P = (g ") * f as Function of NAT,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 = P as Permutation of NAT by A9, A31;
take P " ; ::_thesis: S2 * (P ") is subsequence of S1
( NAT = dom (S2 * (P ")) & NAT = dom (S1 * g) & ( for x being set st x in NAT holds
(S2 * (P ")) . x = (S1 * g) . x ) )
proof
thus NAT = dom (S2 * (P ")) by FUNCT_2:def_1; ::_thesis: ( NAT = dom (S1 * g) & ( for x being set st x in NAT holds
(S2 * (P ")) . x = (S1 * g) . x ) )
rng g c= dom S1 by A28, NORMSP_1:12;
hence NAT = dom (S1 * g) by A21, RELAT_1:27; ::_thesis: for x being set st x in NAT holds
(S2 * (P ")) . x = (S1 * g) . x
let x be set ; ::_thesis: ( x in NAT implies (S2 * (P ")) . x = (S1 * g) . x )
assume A51: x in NAT ; ::_thesis: (S2 * (P ")) . x = (S1 * g) . x
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 ;
::_thesis: verum
end;
then S2 * (P ") = S1 * g1 by FUNCT_1:2;
hence S2 * (P ") is subsequence of S1 ; ::_thesis: verum
end;
scheme :: FRECHET2:sch 1
PermSeq{ F1() -> non empty 1-sorted , F2() -> sequence of F1(), F3() -> Permutation of NAT, P1[ set ] } :
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
P1[(F2() * F3()) . m]
provided
A1: ex n being Element of NAT st
for m being Element of NAT
for x being Point of F1() st n <= m & x = F2() . m holds
P1[x]
proof
consider n being Element of NAT such that
A2: for m being Element of NAT
for x being Point of F1() st n <= m & x = F2() . m holds
P1[x] by A1;
( n in succ n & dom (F3() ") = NAT ) by FUNCT_2:def_1, ORDINAL1:6;
then (F3() ") . n in (F3() ") .: (succ n) by FUNCT_1:def_6;
then reconsider X = (F3() ") .: (succ n) as non empty finite Subset of NAT ;
reconsider mX = (max X) + 1 as Element of NAT ;
take mX ; ::_thesis: for m being Element of NAT st mX <= m holds
P1[(F2() * F3()) . m]
let m be Element of NAT ; ::_thesis: ( mX <= m implies P1[(F2() * F3()) . m] )
m in NAT ;
then A3: m in dom F3() by FUNCT_2:52;
assume A4: mX <= m ; ::_thesis: P1[(F2() * F3()) . m]
n <= F3() . m
proof
assume F3() . m < n ; ::_thesis: contradiction
then F3() . m in { p1 where p1 is Element of NAT : p1 < n } ;
then F3() . m in n by AXIOMS:4;
then F3() . m in succ n by ORDINAL1:8;
then m in F3() " (succ n) by A3, FUNCT_1:def_7;
then m in (F3() ") .: (succ n) by FUNCT_1:85;
then m <= max X by XXREAL_2:def_8;
hence contradiction by A4, NAT_1:13; ::_thesis: verum
end;
then A5: P1[F2() . (F3() . m)] by A2;
m in NAT ;
then m in dom F3() by FUNCT_2:def_1;
hence P1[(F2() * F3()) . m] by A5, FUNCT_1:13; ::_thesis: verum
end;
scheme :: FRECHET2:sch 2
PermSeq2{ F1() -> non empty TopStruct , F2() -> sequence of F1(), F3() -> Permutation of NAT, P1[ set ] } :
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
P1[(F2() * F3()) . m]
provided
A1: ex n being Element of NAT st
for m being Element of NAT
for x being Point of F1() st n <= m & x = F2() . m holds
P1[x]
proof
reconsider T1 = F1() as non empty 1-sorted ;
reconsider S1 = F2() as sequence of T1 ;
A2: ex n being Element of NAT st
for m being Element of NAT
for x being Point of T1 st n <= m & x = S1 . m holds
P1[x] by A1;
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
P1[(S1 * F3()) . m] from FRECHET2:sch_1(A2);
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
P1[(F2() * F3()) . m] ; ::_thesis: verum
end;
theorem Th37: :: FRECHET2:37
for T being non empty TopStruct
for S being sequence of T
for P being Permutation of NAT
for 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 ; ::_thesis: for S being sequence of T
for P being Permutation of NAT
for x being Point of T st S is_convergent_to x holds
S * P is_convergent_to x
let S be sequence of T; ::_thesis: for P being Permutation of NAT
for x being Point of T st S is_convergent_to x holds
S * P is_convergent_to x
let P be Permutation of NAT; ::_thesis: for x being Point of T st S is_convergent_to x holds
S * P is_convergent_to x
let x be Point of T; ::_thesis: ( S is_convergent_to x implies S * P is_convergent_to x )
assume A1: S is_convergent_to x ; ::_thesis: S * P is_convergent_to x
for U1 being Subset of T st U1 is open & x in U1 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(S * P) . m in U1
proof
let U1 be Subset of T; ::_thesis: ( U1 is open & x in U1 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(S * P) . m in U1 )
defpred S1[ set ] means $1 in U1;
assume A2: ( U1 is open & x in U1 ) ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(S * P) . m in U1
A3: ex n being Element of NAT st
for m being Element of NAT
for x being Point of T st n <= m & x = S . m holds
S1[x]
proof
consider n being Element of NAT such that
A4: for m being Element of NAT st n <= m holds
S . m in U1 by A1, A2, FRECHET:def_3;
take n ; ::_thesis: for m being Element of NAT
for x being Point of T st n <= m & x = S . m holds
S1[x]
let m be Element of NAT ; ::_thesis: for x being Point of T st n <= m & x = S . m holds
S1[x]
let x be Point of T; ::_thesis: ( n <= m & x = S . m implies S1[x] )
assume ( n <= m & x = S . m ) ; ::_thesis: S1[x]
hence S1[x] by A4; ::_thesis: verum
end;
thus ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S1[(S * P) . m] from FRECHET2:sch_2(A3); ::_thesis: verum
end;
hence S * P is_convergent_to x by FRECHET:def_3; ::_thesis: verum
end;
theorem :: FRECHET2:38
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 ; ::_thesis: ex NS being increasing sequence of NAT st
for n being Element of NAT holds NS . n = n + n0
deffunc H1( Element of NAT ) -> Element of NAT = $1 + n0;
consider NS being Real_Sequence such that
A1: for n being Element of NAT holds NS . n = H1(n) from SEQ_1:sch_1();
A2: NS is increasing
proof
let n be Element of NAT ; :: according to SEQM_3:def_6 ::_thesis: not NS . (n + 1) <= NS . n
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 not NS . (n + 1) <= NS . n by A1; ::_thesis: verum
end;
for n being Element of NAT holds NS . n is Element of NAT
proof
let n be Element of NAT ; ::_thesis: NS . n is Element of NAT
n + n0 in NAT ;
hence NS . n is Element of NAT by A1; ::_thesis: verum
end;
then reconsider NS = NS as increasing sequence of NAT by A2, SEQM_3:13;
take NS ; ::_thesis: for n being Element of NAT holds NS . n = n + n0
thus for n being Element of NAT holds NS . n = n + n0 by A1; ::_thesis: verum
end;
theorem Th39: :: FRECHET2:39
for T being non empty TopStruct
for S being sequence of T
for x being Point of T
for 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 ; ::_thesis: for S being sequence of T
for x being Point of T
for n0 being Nat st x is_a_cluster_point_of S holds
x is_a_cluster_point_of S ^\ n0
let S be sequence of T; ::_thesis: for x being Point of T
for n0 being Nat st x is_a_cluster_point_of S holds
x is_a_cluster_point_of S ^\ n0
let x be Point of T; ::_thesis: for n0 being Nat st x is_a_cluster_point_of S holds
x is_a_cluster_point_of S ^\ n0
let n0 be Nat; ::_thesis: ( x is_a_cluster_point_of S implies x is_a_cluster_point_of S ^\ n0 )
assume A1: x is_a_cluster_point_of S ; ::_thesis: x is_a_cluster_point_of S ^\ n0
set S1 = S ^\ n0;
let O be Subset of T; :: according to FRECHET2:def_3 ::_thesis: for n being Element of NAT st O is open & x in O holds
ex m being Element of NAT st
( n <= m & (S ^\ n0) . m in O )
let n be Element of NAT ; ::_thesis: ( O is open & x in O implies ex m being Element of NAT st
( n <= m & (S ^\ n0) . m in O ) )
assume ( O is open & x in O ) ; ::_thesis: ex m being Element of NAT st
( n <= m & (S ^\ n0) . m in O )
then consider m0 being Element of NAT such that
A2: n + n0 <= m0 and
A3: S . m0 in O by A1, Def3;
( 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 ; ::_thesis: ( n <= m & (S ^\ n0) . m in O )
thus n <= m by A2, XREAL_1:19; ::_thesis: (S ^\ n0) . m in O
(S ^\ n0) . m = S . ((m0 - n0) + n0) by NAT_1:def_3
.= S . m0 ;
hence (S ^\ n0) . m in O by A3; ::_thesis: verum
end;
theorem Th40: :: FRECHET2:40
for T being non empty TopStruct
for S being sequence of T
for 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 ; ::_thesis: for S being sequence of T
for x being Point of T st x is_a_cluster_point_of S holds
x in Cl (rng S)
let S be sequence of T; ::_thesis: for x being Point of T st x is_a_cluster_point_of S holds
x in Cl (rng S)
let x be Point of T; ::_thesis: ( x is_a_cluster_point_of S implies x in Cl (rng S) )
assume A1: x is_a_cluster_point_of S ; ::_thesis: x in Cl (rng S)
for G being Subset of T st G is open & x in G holds
rng S meets G
proof
let G be Subset of T; ::_thesis: ( G is open & x in G implies rng S meets G )
assume A2: G is open ; ::_thesis: ( not x in G or rng S meets G )
assume x in G ; ::_thesis: rng S meets G
then consider m being Element of NAT such that
0 <= m and
A3: S . m in G by A1, A2, Def3;
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 rng S meets G by XBOOLE_0:def_7; ::_thesis: verum
end;
hence x in Cl (rng S) by PRE_TOPC:def_7; ::_thesis: verum
end;
theorem :: FRECHET2:41
for T being non empty TopStruct st T is Frechet holds
for S being sequence of T
for 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 ; ::_thesis: ( T is Frechet implies for S being sequence of T
for 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 )
assume A1: T is Frechet ; ::_thesis: for S being sequence of T
for 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
let S be sequence of T; ::_thesis: for 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
let x be Point of T; ::_thesis: ( x is_a_cluster_point_of S implies ex S1 being subsequence of S st S1 is_convergent_to x )
assume A2: x is_a_cluster_point_of S ; ::_thesis: ex S1 being subsequence of S st S1 is_convergent_to x
defpred S1[ Point of T] means x in Cl {$1};
reconsider Y = { y where y is Point of T : S1[y] } as Subset of T from DOMAIN_1:sch_7();
percases ( for n being Element of NAT ex m being Element of NAT st
( m >= n & S . m in Y ) or ex n being Element of NAT st
for m being Element of NAT st m >= n holds
not S . m in Y ) ;
supposeA3: for n being Element of NAT ex m being Element of NAT st
( m >= n & S . m in Y ) ; ::_thesis: ex S1 being subsequence of S st S1 is_convergent_to x
defpred S2[ set ] means $1 in Y;
A4: for n being Element of NAT ex m being Element of NAT st
( n <= m & S2[S . m] ) by A3;
consider S1 being subsequence of S such that
A5: for n being Element of NAT holds S2[S1 . n] from VALUED_1:sch_1(A4);
take S1 ; ::_thesis: S1 is_convergent_to x
rng S1 c= Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng S1 or y in Y )
assume y in rng S1 ; ::_thesis: y in Y
then consider n being set such that
A6: n in dom S1 and
A7: y = S1 . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A6;
S1 . n in Y by A5;
hence y in Y by A7; ::_thesis: verum
end;
hence S1 is_convergent_to x by Th33; ::_thesis: verum
end;
suppose ex n being Element of NAT st
for m being Element of NAT st m >= n holds
not S . m in Y ; ::_thesis: ex S1 being subsequence of S st S1 is_convergent_to x
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 (S ^\ n0)) by A2, Th39, Th40;
then consider S2 being sequence of T such that
A9: rng S2 c= rng (S ^\ n0) and
A10: x in Lim S2 by A1, FRECHET:def_6;
A11: S2 is_convergent_to x by A10, FRECHET:def_5;
A12: for n being Element of NAT holds not (S ^\ n0) . n in Y
proof
let n be Element of NAT ; ::_thesis: not (S ^\ n0) . n in Y
not S . (n + n0) in Y by A8, NAT_1:11;
hence not (S ^\ n0) . n in Y by NAT_1:def_3; ::_thesis: verum
end;
(rng (S ^\ n0)) /\ Y = {}
proof
set y = the Element of (rng (S ^\ n0)) /\ Y;
assume A13: (rng (S ^\ n0)) /\ Y <> {} ; ::_thesis: contradiction
then the Element of (rng (S ^\ n0)) /\ Y in rng (S ^\ n0) by XBOOLE_0:def_4;
then consider n being set such that
A14: n in dom (S ^\ n0) and
A15: the Element of (rng (S ^\ n0)) /\ Y = (S ^\ n0) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A14;
not (S ^\ n0) . n in Y by A12;
hence contradiction by A13, A15, XBOOLE_0:def_4; ::_thesis: verum
end;
then rng (S ^\ n0) misses Y by XBOOLE_0:def_7;
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 S ^\ n0 by A9, A16, Th36, XBOOLE_1:1;
reconsider S1 = S29 * P as subsequence of S ^\ n0 by A17;
reconsider S1 = S1 as subsequence of S by VALUED_0:20;
take S1 ; ::_thesis: S1 is_convergent_to x
S29 is_convergent_to x by A11, Th15;
hence S1 is_convergent_to x by Th37; ::_thesis: verum
end;
end;
end;
begin
theorem :: FRECHET2:42
for T being non empty TopSpace st T is first-countable holds
for x being Point of T ex B being Basis of x 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 :: FRECHET2:43
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 :: FRECHET2:44
for T being non empty TopSpace st T is T_2 holds
T is T_1 by Lm4;
theorem :: FRECHET2:45
for T being non empty TopSpace st not T is T_1 holds
ex x1, x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 ) by Lm3;