:: KURATO_2 semantic presentation
begin
definition
let T be 1-sorted ;
mode SetSequence of T is SetSequence of the carrier of T;
end;
begin
registration
let f be FinSequence of the carrier of (TOP-REAL 2);
cluster L~ f -> closed ;
coherence
L~ f is closed ;
end;
theorem Th1: :: KURATO_2:1
for n being Element of NAT
for x being Point of (Euclid n)
for r being real number holds Ball (x,r) is open Subset of (TOP-REAL n)
proof
let n be Element of NAT ; ::_thesis: for x being Point of (Euclid n)
for r being real number holds Ball (x,r) is open Subset of (TOP-REAL n)
let x be Point of (Euclid n); ::_thesis: for r being real number holds Ball (x,r) is open Subset of (TOP-REAL n)
let r be real number ; ::_thesis: Ball (x,r) is open Subset of (TOP-REAL n)
reconsider A = Ball (x,r) as Subset of (TOP-REAL n) by TOPREAL3:8;
reconsider A = A as Subset of (TOP-REAL n) ;
r is Real by XREAL_0:def_1;
then A is open by GOBOARD6:3;
hence Ball (x,r) is open Subset of (TOP-REAL n) ; ::_thesis: verum
end;
theorem Th2: :: KURATO_2:2
for n being Element of NAT
for p being Point of (Euclid n)
for x, p9 being Point of (TOP-REAL n)
for r being real number st p = p9 & x in Ball (p,r) holds
|.(x - p9).| < r
proof
let n be Element of NAT ; ::_thesis: for p being Point of (Euclid n)
for x, p9 being Point of (TOP-REAL n)
for r being real number st p = p9 & x in Ball (p,r) holds
|.(x - p9).| < r
let p be Point of (Euclid n); ::_thesis: for x, p9 being Point of (TOP-REAL n)
for r being real number st p = p9 & x in Ball (p,r) holds
|.(x - p9).| < r
let x, p9 be Point of (TOP-REAL n); ::_thesis: for r being real number st p = p9 & x in Ball (p,r) holds
|.(x - p9).| < r
let r be real number ; ::_thesis: ( p = p9 & x in Ball (p,r) implies |.(x - p9).| < r )
reconsider x9 = x as Point of (Euclid n) by TOPREAL3:8;
assume that
A1: p = p9 and
A2: x in Ball (p,r) ; ::_thesis: |.(x - p9).| < r
dist (x9,p) < r by A2, METRIC_1:11;
hence |.(x - p9).| < r by A1, SPPOL_1:39; ::_thesis: verum
end;
theorem Th3: :: KURATO_2:3
for n being Element of NAT
for p being Point of (Euclid n)
for x, p9 being Point of (TOP-REAL n)
for r being real number st p = p9 & |.(x - p9).| < r holds
x in Ball (p,r)
proof
let n be Element of NAT ; ::_thesis: for p being Point of (Euclid n)
for x, p9 being Point of (TOP-REAL n)
for r being real number st p = p9 & |.(x - p9).| < r holds
x in Ball (p,r)
let p be Point of (Euclid n); ::_thesis: for x, p9 being Point of (TOP-REAL n)
for r being real number st p = p9 & |.(x - p9).| < r holds
x in Ball (p,r)
let x, p9 be Point of (TOP-REAL n); ::_thesis: for r being real number st p = p9 & |.(x - p9).| < r holds
x in Ball (p,r)
let r be real number ; ::_thesis: ( p = p9 & |.(x - p9).| < r implies x in Ball (p,r) )
reconsider x9 = x as Point of (Euclid n) by TOPREAL3:8;
assume ( p = p9 & |.(x - p9).| < r ) ; ::_thesis: x in Ball (p,r)
then dist (x9,p) < r by SPPOL_1:39;
hence x in Ball (p,r) by METRIC_1:11; ::_thesis: verum
end;
theorem :: KURATO_2:4
for n being Element of NAT
for r being Point of (TOP-REAL n)
for X being Subset of (TOP-REAL n) st r in Cl X holds
ex seq being Real_Sequence of n st
( rng seq c= X & seq is convergent & lim seq = r )
proof
let n be Element of NAT ; ::_thesis: for r being Point of (TOP-REAL n)
for X being Subset of (TOP-REAL n) st r in Cl X holds
ex seq being Real_Sequence of n st
( rng seq c= X & seq is convergent & lim seq = r )
let r be Point of (TOP-REAL n); ::_thesis: for X being Subset of (TOP-REAL n) st r in Cl X holds
ex seq being Real_Sequence of n st
( rng seq c= X & seq is convergent & lim seq = r )
let X be Subset of (TOP-REAL n); ::_thesis: ( r in Cl X implies ex seq being Real_Sequence of n st
( rng seq c= X & seq is convergent & lim seq = r ) )
reconsider r9 = r as Point of (Euclid n) by TOPREAL3:8;
defpred S1[ set , set ] means ex z being Element of NAT st
( $1 = z & $2 = choose (X /\ (Ball (r9,(1 / (z + 1))))) );
assume A1: r in Cl X ; ::_thesis: ex seq being Real_Sequence of n st
( rng seq c= X & seq is convergent & lim seq = r )
A2: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
ex_u_being_set_st_
(_u_in_the_carrier_of_(TOP-REAL_n)_&_S1[x,u]_)
let x be set ; ::_thesis: ( x in NAT implies ex u being set st
( u in the carrier of (TOP-REAL n) & S1[x,u] ) )
assume x in NAT ; ::_thesis: ex u being set st
( u in the carrier of (TOP-REAL n) & S1[x,u] )
then reconsider k = x as Element of NAT ;
set n1 = k + 1;
set oi = Ball (r9,(1 / (k + 1)));
reconsider oi = Ball (r9,(1 / (k + 1))) as open Subset of (TOP-REAL n) by Th1;
reconsider u = choose (X /\ oi) as set ;
take u = u; ::_thesis: ( u in the carrier of (TOP-REAL n) & S1[x,u] )
dist (r9,r9) < 1 / (k + 1) by METRIC_1:1;
then r in oi by METRIC_1:11;
then X meets oi by A1, PRE_TOPC:24;
then not X /\ oi is empty by XBOOLE_0:def_7;
then u in X /\ oi ;
hence u in the carrier of (TOP-REAL n) ; ::_thesis: S1[x,u]
thus S1[x,u] ; ::_thesis: verum
end;
consider seq being Function such that
A3: ( dom seq = NAT & rng seq c= the carrier of (TOP-REAL n) ) and
A4: for x being set st x in NAT holds
S1[x,seq . x] from FUNCT_1:sch_5(A2);
reconsider seq = seq as Real_Sequence of n by A3, FUNCT_2:def_1, RELSET_1:4;
take seq ; ::_thesis: ( rng seq c= X & seq is convergent & lim seq = r )
thus rng seq c= X ::_thesis: ( seq is convergent & lim seq = r )
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng seq or y in X )
assume y in rng seq ; ::_thesis: y in X
then consider x being set such that
A5: x in dom seq and
A6: seq . x = y by FUNCT_1:def_3;
consider k being Element of NAT such that
x = k and
A7: seq . x = choose (X /\ (Ball (r9,(1 / (k + 1))))) by A4, A5;
set n1 = k + 1;
reconsider oi = Ball (r9,(1 / (k + 1))) as open Subset of (TOP-REAL n) by Th1;
dist (r9,r9) < 1 / (k + 1) by METRIC_1:1;
then r in oi by METRIC_1:11;
then X meets oi by A1, PRE_TOPC:24;
then not X /\ oi is empty by XBOOLE_0:def_7;
hence y in X by A6, A7, XBOOLE_0:def_4; ::_thesis: verum
end;
A8: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
|.((seq_._m)_-_r).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((seq . m) - r).| < p )
set cp = [/(1 / p)\];
A9: 1 / p <= [/(1 / p)\] by INT_1:def_7;
assume A10: 0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((seq . m) - r).| < p
then A11: 0 < [/(1 / p)\] by INT_1:def_7;
then reconsider cp = [/(1 / p)\] as Element of NAT by INT_1:3;
take k = cp; ::_thesis: for m being Element of NAT st k <= m holds
|.((seq . m) - r).| < p
k < k + 1 by NAT_1:13;
then A12: 1 / (k + 1) < 1 / k by A11, XREAL_1:88;
1 / (1 / p) >= 1 / cp by A10, A9, XREAL_1:85;
then A13: 1 / (k + 1) < p by A12, XXREAL_0:2;
let m be Element of NAT ; ::_thesis: ( k <= m implies |.((seq . m) - r).| < p )
assume k <= m ; ::_thesis: |.((seq . m) - r).| < p
then A14: k + 1 <= m + 1 by XREAL_1:6;
set m1 = m + 1;
1 / (m + 1) <= 1 / (k + 1) by A14, XREAL_1:85;
then A15: 1 / (m + 1) < p by A13, XXREAL_0:2;
set oi = Ball (r9,(1 / (m + 1)));
reconsider oi = Ball (r9,(1 / (m + 1))) as open Subset of (TOP-REAL n) by Th1;
dist (r9,r9) < 1 / (m + 1) by METRIC_1:1;
then r in oi by METRIC_1:11;
then X meets oi by A1, PRE_TOPC:24;
then A16: not X /\ oi is empty by XBOOLE_0:def_7;
ex m9 being Element of NAT st
( m9 = m & seq . m = choose (X /\ (Ball (r9,(1 / (m9 + 1))))) ) by A4;
then seq . m in oi by A16, XBOOLE_0:def_4;
hence |.((seq . m) - r).| < p by A15, Th2, XXREAL_0:2; ::_thesis: verum
end;
hence seq is convergent by TOPRNS_1:def_8; ::_thesis: lim seq = r
hence lim seq = r by A8, TOPRNS_1:def_9; ::_thesis: verum
end;
registration
let M be non empty MetrSpace;
cluster TopSpaceMetr M -> first-countable ;
coherence
TopSpaceMetr M is first-countable by FRECHET:20;
end;
Lm1: for T being non empty TopSpace
for x being Point of T
for y being Point of TopStruct(# the carrier of T, the topology of T #)
for A being set st x = y holds
( A is Basis of iff A is Basis of )
proof
let T be non empty TopSpace; ::_thesis: for x being Point of T
for y being Point of TopStruct(# the carrier of T, the topology of T #)
for A being set st x = y holds
( A is Basis of iff A is Basis of )
let x be Point of T; ::_thesis: for y being Point of TopStruct(# the carrier of T, the topology of T #)
for A being set st x = y holds
( A is Basis of iff A is Basis of )
let y be Point of TopStruct(# the carrier of T, the topology of T #); ::_thesis: for A being set st x = y holds
( A is Basis of iff A is Basis of )
let A be set ; ::_thesis: ( x = y implies ( A is Basis of iff A is Basis of ) )
assume A1: x = y ; ::_thesis: ( A is Basis of iff A is Basis of )
thus ( A is Basis of implies A is Basis of ) ::_thesis: ( A is Basis of implies A is Basis of )
proof
assume A2: A is Basis of ; ::_thesis: A is Basis of
then reconsider A = A as Subset-Family of TopStruct(# the carrier of T, the topology of T #) ;
A is Basis of
proof
A c= the topology of TopStruct(# the carrier of T, the topology of T #) by A2, TOPS_2:64;
then A3: A is open by TOPS_2:64;
A is y -quasi_basis
proof
thus y in Intersect A by A1, A2, YELLOW_8:def_1; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #) holds
( not b1 is open or not y in b1 or ex b2 being Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #) st
( b2 in A & b2 c= b1 ) )
let S be Subset of TopStruct(# the carrier of T, the topology of T #); ::_thesis: ( not S is open or not y in S or ex b1 being Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #) st
( b1 in A & b1 c= S ) )
reconsider SS = S as Subset of T ;
assume that
A4: S is open and
A5: y in S ; ::_thesis: ex b1 being Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #) st
( b1 in A & b1 c= S )
SS is open by A4, PRE_TOPC:30;
then consider W being Subset of T such that
A6: ( W in A & W c= SS ) by A1, A2, A5, YELLOW_8:def_1;
reconsider V = W as Subset of TopStruct(# the carrier of T, the topology of T #) ;
take V ; ::_thesis: ( V in A & V c= S )
thus ( V in A & V c= S ) by A6; ::_thesis: verum
end;
hence A is Basis of by A3; ::_thesis: verum
end;
hence A is Basis of ; ::_thesis: verum
end;
assume A7: A is Basis of ; ::_thesis: A is Basis of
then reconsider A = A as Subset-Family of T ;
A is Basis of
proof
A c= the topology of T by A7, TOPS_2:64;
then A8: A is open by TOPS_2:64;
A is x -quasi_basis
proof
thus x in Intersect A by A1, A7, YELLOW_8:def_1; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of T holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of T st
( b2 in A & b2 c= b1 ) )
let S be Subset of T; ::_thesis: ( not S is open or not x in S or ex b1 being Element of bool the carrier of T st
( b1 in A & b1 c= S ) )
reconsider SS = S as Subset of TopStruct(# the carrier of T, the topology of T #) ;
assume that
A9: S is open and
A10: x in S ; ::_thesis: ex b1 being Element of bool the carrier of T st
( b1 in A & b1 c= S )
SS is open by A9, PRE_TOPC:30;
then consider W being Subset of TopStruct(# the carrier of T, the topology of T #) such that
A11: ( W in A & W c= SS ) by A1, A7, A10, YELLOW_8:def_1;
reconsider V = W as Subset of T ;
take V ; ::_thesis: ( V in A & V c= S )
thus ( V in A & V c= S ) by A11; ::_thesis: verum
end;
hence A is Basis of by A8; ::_thesis: verum
end;
hence A is Basis of ; ::_thesis: verum
end;
theorem Th5: :: KURATO_2:5
for T being non empty TopSpace holds
( T is first-countable iff TopStruct(# the carrier of T, the topology of T #) is first-countable )
proof
let T be non empty TopSpace; ::_thesis: ( T is first-countable iff TopStruct(# the carrier of T, the topology of T #) is first-countable )
thus ( T is first-countable implies TopStruct(# the carrier of T, the topology of T #) is first-countable ) ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) is first-countable implies T is first-countable )
proof
assume A1: T is first-countable ; ::_thesis: TopStruct(# the carrier of T, the topology of T #) is first-countable
let x be Point of TopStruct(# the carrier of T, the topology of T #); :: according to FRECHET:def_2 ::_thesis: ex b1 being Element of bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #)) st b1 is countable
reconsider y = x as Point of T ;
consider C being Basis of such that
A2: C is countable by A1, FRECHET:def_2;
reconsider B = C as Basis of by Lm1;
take B ; ::_thesis: B is countable
thus B is countable by A2; ::_thesis: verum
end;
assume A3: TopStruct(# the carrier of T, the topology of T #) is first-countable ; ::_thesis: T is first-countable
let x be Point of T; :: according to FRECHET:def_2 ::_thesis: ex b1 being Element of bool (bool the carrier of T) st b1 is countable
reconsider y = x as Point of TopStruct(# the carrier of T, the topology of T #) ;
consider C being Basis of such that
A4: C is countable by A3, FRECHET:def_2;
reconsider B = C as Basis of by Lm1;
take B ; ::_thesis: B is countable
thus B is countable by A4; ::_thesis: verum
end;
registration
let n be Element of NAT ;
cluster TOP-REAL n -> first-countable ;
coherence
TOP-REAL n is first-countable
proof
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
hence TOP-REAL n is first-countable by Th5; ::_thesis: verum
end;
end;
theorem :: KURATO_2:6
for n being Element of NAT
for A being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
( p in Cl A iff for r being real number st r > 0 holds
Ball (p9,r) meets A )
proof
let n be Element of NAT ; ::_thesis: for A being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
( p in Cl A iff for r being real number st r > 0 holds
Ball (p9,r) meets A )
let A be Subset of (TOP-REAL n); ::_thesis: for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
( p in Cl A iff for r being real number st r > 0 holds
Ball (p9,r) meets A )
let p be Point of (TOP-REAL n); ::_thesis: for p9 being Point of (Euclid n) st p = p9 holds
( p in Cl A iff for r being real number st r > 0 holds
Ball (p9,r) meets A )
let p9 be Point of (Euclid n); ::_thesis: ( p = p9 implies ( p in Cl A iff for r being real number st r > 0 holds
Ball (p9,r) meets A ) )
assume A1: p = p9 ; ::_thesis: ( p in Cl A iff for r being real number st r > 0 holds
Ball (p9,r) meets A )
hereby ::_thesis: ( ( for r being real number st r > 0 holds
Ball (p9,r) meets A ) implies p in Cl A )
assume A2: p in Cl A ; ::_thesis: for r being real number st r > 0 holds
Ball (p9,r) meets A
let r be real number ; ::_thesis: ( r > 0 implies Ball (p9,r) meets A )
reconsider B = Ball (p9,r) as Subset of (TOP-REAL n) by TOPREAL3:8;
assume r > 0 ; ::_thesis: Ball (p9,r) meets A
then B is a_neighborhood of p by A1, GOBOARD6:2;
hence Ball (p9,r) meets A by A2, CONNSP_2:27; ::_thesis: verum
end;
assume A3: for r being real number st r > 0 holds
Ball (p9,r) meets A ; ::_thesis: p in Cl A
for G being a_neighborhood of p holds G meets A
proof
let G be a_neighborhood of p; ::_thesis: G meets A
p in Int G by CONNSP_2:def_1;
then ex r being real number st
( r > 0 & Ball (p9,r) c= G ) by A1, GOBOARD6:5;
hence G meets A by A3, XBOOLE_1:63; ::_thesis: verum
end;
hence p in Cl A by CONNSP_2:27; ::_thesis: verum
end;
theorem :: KURATO_2:7
for n being Element of NAT
for x, y being Point of (TOP-REAL n)
for x9 being Point of (Euclid n) st x9 = x & x <> y holds
ex r being Real st not y in Ball (x9,r)
proof
let n be Element of NAT ; ::_thesis: for x, y being Point of (TOP-REAL n)
for x9 being Point of (Euclid n) st x9 = x & x <> y holds
ex r being Real st not y in Ball (x9,r)
let x, y be Point of (TOP-REAL n); ::_thesis: for x9 being Point of (Euclid n) st x9 = x & x <> y holds
ex r being Real st not y in Ball (x9,r)
let x9 be Point of (Euclid n); ::_thesis: ( x9 = x & x <> y implies ex r being Real st not y in Ball (x9,r) )
reconsider y9 = y as Point of (Euclid n) by TOPREAL3:8;
reconsider r = (dist (x9,y9)) / 2 as Real ;
assume ( x9 = x & x <> y ) ; ::_thesis: not for r being Real holds y in Ball (x9,r)
then A1: dist (x9,y9) <> 0 by METRIC_1:2;
take r ; ::_thesis: not y in Ball (x9,r)
dist (x9,y9) >= 0 by METRIC_1:5;
then dist (x9,y9) > r by A1, XREAL_1:216;
hence not y in Ball (x9,r) by METRIC_1:11; ::_thesis: verum
end;
theorem Th8: :: KURATO_2:8
for n being Element of NAT
for S being Subset of (TOP-REAL n) holds
( not S is bounded iff for r being Real st r > 0 holds
ex x, y being Point of (Euclid n) st
( x in S & y in S & dist (x,y) > r ) )
proof
let n be Element of NAT ; ::_thesis: for S being Subset of (TOP-REAL n) holds
( not S is bounded iff for r being Real st r > 0 holds
ex x, y being Point of (Euclid n) st
( x in S & y in S & dist (x,y) > r ) )
let S be Subset of (TOP-REAL n); ::_thesis: ( not S is bounded iff for r being Real st r > 0 holds
ex x, y being Point of (Euclid n) st
( x in S & y in S & dist (x,y) > r ) )
reconsider S9 = S as Subset of (Euclid n) by TOPREAL3:8;
hereby ::_thesis: ( ( for r being Real st r > 0 holds
ex x, y being Point of (Euclid n) st
( x in S & y in S & dist (x,y) > r ) ) implies not S is bounded )
assume not S is bounded ; ::_thesis: for r being Real st r > 0 holds
ex x, y being Point of (Euclid n) st
( x in S & y in S & dist (x,y) > r )
then not S9 is bounded by JORDAN2C:11;
hence for r being Real st r > 0 holds
ex x, y being Point of (Euclid n) st
( x in S & y in S & dist (x,y) > r ) by TBSP_1:def_7; ::_thesis: verum
end;
assume A1: for r being Real st r > 0 holds
ex x, y being Point of (Euclid n) st
( x in S & y in S & dist (x,y) > r ) ; ::_thesis: not S is bounded
not S is bounded
proof
assume S is bounded ; ::_thesis: contradiction
then S is bounded Subset of (Euclid n) by JORDAN2C:11;
hence contradiction by A1, TBSP_1:def_7; ::_thesis: verum
end;
hence not S is bounded ; ::_thesis: verum
end;
theorem Th9: :: KURATO_2:9
for n being Element of NAT
for a, b being real number
for x, y being Point of (Euclid n) st Ball (x,a) meets Ball (y,b) holds
dist (x,y) < a + b
proof
let n be Element of NAT ; ::_thesis: for a, b being real number
for x, y being Point of (Euclid n) st Ball (x,a) meets Ball (y,b) holds
dist (x,y) < a + b
let a, b be real number ; ::_thesis: for x, y being Point of (Euclid n) st Ball (x,a) meets Ball (y,b) holds
dist (x,y) < a + b
let x, y be Point of (Euclid n); ::_thesis: ( Ball (x,a) meets Ball (y,b) implies dist (x,y) < a + b )
assume Ball (x,a) meets Ball (y,b) ; ::_thesis: dist (x,y) < a + b
then consider z being set such that
A1: z in Ball (x,a) and
A2: z in Ball (y,b) by XBOOLE_0:3;
reconsider z = z as Point of (Euclid n) by A1;
dist (y,z) < b by A2, METRIC_1:11;
then A3: (dist (x,z)) + (dist (y,z)) < (dist (x,z)) + b by XREAL_1:8;
A4: (dist (x,z)) + (dist (y,z)) >= dist (x,y) by METRIC_1:4;
dist (x,z) < a by A1, METRIC_1:11;
then (dist (x,z)) + b < a + b by XREAL_1:8;
then (dist (x,z)) + (dist (y,z)) < a + b by A3, XXREAL_0:2;
hence dist (x,y) < a + b by A4, XXREAL_0:2; ::_thesis: verum
end;
theorem Th10: :: KURATO_2:10
for n being Element of NAT
for a, b, c being real number
for x, y, z being Point of (Euclid n) st Ball (x,a) meets Ball (z,c) & Ball (z,c) meets Ball (y,b) holds
dist (x,y) < (a + b) + (2 * c)
proof
let n be Element of NAT ; ::_thesis: for a, b, c being real number
for x, y, z being Point of (Euclid n) st Ball (x,a) meets Ball (z,c) & Ball (z,c) meets Ball (y,b) holds
dist (x,y) < (a + b) + (2 * c)
let a, b, c be real number ; ::_thesis: for x, y, z being Point of (Euclid n) st Ball (x,a) meets Ball (z,c) & Ball (z,c) meets Ball (y,b) holds
dist (x,y) < (a + b) + (2 * c)
let x, y, z be Point of (Euclid n); ::_thesis: ( Ball (x,a) meets Ball (z,c) & Ball (z,c) meets Ball (y,b) implies dist (x,y) < (a + b) + (2 * c) )
assume ( Ball (x,a) meets Ball (z,c) & Ball (z,c) meets Ball (y,b) ) ; ::_thesis: dist (x,y) < (a + b) + (2 * c)
then ( (dist (x,z)) + (dist (z,y)) < (a + c) + (dist (z,y)) & (a + c) + (dist (z,y)) < (a + c) + (c + b) ) by Th9, XREAL_1:8;
then A1: (dist (x,z)) + (dist (z,y)) < (a + c) + (c + b) by XXREAL_0:2;
dist (x,y) <= (dist (x,z)) + (dist (z,y)) by METRIC_1:4;
hence dist (x,y) < (a + b) + (2 * c) by A1, XXREAL_0:2; ::_thesis: verum
end;
theorem Th11: :: KURATO_2:11
for X, Y being non empty TopSpace
for x being Point of X
for y being Point of Y
for V being Subset of [:X,Y:] holds
( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] )
proof
let X, Y be non empty TopSpace; ::_thesis: for x being Point of X
for y being Point of Y
for V being Subset of [:X,Y:] holds
( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] )
let x be Point of X; ::_thesis: for y being Point of Y
for V being Subset of [:X,Y:] holds
( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] )
let y be Point of Y; ::_thesis: for V being Subset of [:X,Y:] holds
( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] )
let V be Subset of [:X,Y:]; ::_thesis: ( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] )
hereby ::_thesis: ( V is a_neighborhood of [x,y] implies V is a_neighborhood of [:{x},{y}:] )
assume V is a_neighborhood of [:{x},{y}:] ; ::_thesis: V is a_neighborhood of [x,y]
then V is a_neighborhood of {[x,y]} by ZFMISC_1:29;
hence V is a_neighborhood of [x,y] by CONNSP_2:8; ::_thesis: verum
end;
assume V is a_neighborhood of [x,y] ; ::_thesis: V is a_neighborhood of [:{x},{y}:]
then V is a_neighborhood of {[x,y]} by CONNSP_2:8;
hence V is a_neighborhood of [:{x},{y}:] by ZFMISC_1:29; ::_thesis: verum
end;
begin
theorem Th12: :: KURATO_2:12
for T being non empty 1-sorted
for F, G being SetSequence of the carrier of T
for A being Subset of T st G is subsequence of F & ( for i being Nat holds F . i = A ) holds
G = F
proof
let T be non empty 1-sorted ; ::_thesis: for F, G being SetSequence of the carrier of T
for A being Subset of T st G is subsequence of F & ( for i being Nat holds F . i = A ) holds
G = F
let F, G be SetSequence of the carrier of T; ::_thesis: for A being Subset of T st G is subsequence of F & ( for i being Nat holds F . i = A ) holds
G = F
let A be Subset of T; ::_thesis: ( G is subsequence of F & ( for i being Nat holds F . i = A ) implies G = F )
assume that
A1: G is subsequence of F and
A2: for i being Nat holds F . i = A ; ::_thesis: G = F
consider NS being increasing sequence of NAT such that
A3: G = F * NS by A1, VALUED_0:def_17;
for i being Element of NAT holds G . i = F . i
proof
let i be Element of NAT ; ::_thesis: G . i = F . i
dom NS = NAT by FUNCT_2:def_1;
then G . i = F . (NS . i) by A3, FUNCT_1:13
.= A by A2
.= F . i by A2 ;
hence G . i = F . i ; ::_thesis: verum
end;
then A4: for x being set st x in dom F holds
F . x = G . x ;
( NAT = dom G & NAT = dom F ) by FUNCT_2:def_1;
hence G = F by A4, FUNCT_1:2; ::_thesis: verum
end;
theorem :: KURATO_2:13
for T being non empty 1-sorted
for S being SetSequence of the carrier of T
for R being subsequence of S
for n being Element of NAT ex m being Element of NAT st
( m >= n & R . n = S . m )
proof
let T be non empty 1-sorted ; ::_thesis: for S being SetSequence of the carrier of T
for R being subsequence of S
for n being Element of NAT ex m being Element of NAT st
( m >= n & R . n = S . m )
let S be SetSequence of the carrier of T; ::_thesis: for R being subsequence of S
for n being Element of NAT ex m being Element of NAT st
( m >= n & R . n = S . m )
let R be subsequence of S; ::_thesis: for n being Element of NAT ex m being Element of NAT st
( m >= n & R . n = S . m )
let n be Element of NAT ; ::_thesis: ex m being Element of NAT st
( m >= n & R . n = S . m )
consider NS being increasing sequence of NAT such that
A1: R = S * NS by VALUED_0:def_17;
take m = NS . n; ::_thesis: ( m >= n & R . n = S . m )
thus m >= n by SEQM_3:14; ::_thesis: R . n = S . m
n in NAT ;
then n in dom NS by FUNCT_2:def_1;
hence R . n = S . m by A1, FUNCT_1:13; ::_thesis: verum
end;
begin
definition
let T be non empty TopSpace;
let S be SetSequence of the carrier of T;
func Lim_inf S -> Subset of T means :Def1: :: KURATO_2:def 1
for p being Point of T holds
( p in it iff for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G );
existence
ex b1 being Subset of T st
for p being Point of T holds
( p in b1 iff for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G )
proof
defpred S1[ Point of T] means for G being a_neighborhood of $1 ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G;
thus ex IT being Subset of T st
for p being Point of T holds
( p in IT iff S1[p] ) from SUBSET_1:sch_3(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of T st ( for p being Point of T holds
( p in b1 iff for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G ) ) & ( for p being Point of T holds
( p in b2 iff for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G ) ) holds
b1 = b2
proof
defpred S1[ Point of T] means for G being a_neighborhood of $1 ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G;
let a, b be Subset of T; ::_thesis: ( ( for p being Point of T holds
( p in a iff for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G ) ) & ( for p being Point of T holds
( p in b iff for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G ) ) implies a = b )
assume that
A1: for p being Point of T holds
( p in a iff S1[p] ) and
A2: for p being Point of T holds
( p in b iff S1[p] ) ; ::_thesis: a = b
thus a = b from SUBSET_1:sch_2(A1, A2); ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Lim_inf KURATO_2:def_1_:_
for T being non empty TopSpace
for S being SetSequence of the carrier of T
for b3 being Subset of T holds
( b3 = Lim_inf S iff for p being Point of T holds
( p in b3 iff for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G ) );
theorem Th14: :: KURATO_2:14
for n being Element of NAT
for S being SetSequence of the carrier of (TOP-REAL n)
for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
( p in Lim_inf S iff for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r) )
proof
let n be Element of NAT ; ::_thesis: for S being SetSequence of the carrier of (TOP-REAL n)
for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
( p in Lim_inf S iff for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r) )
let S be SetSequence of the carrier of (TOP-REAL n); ::_thesis: for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
( p in Lim_inf S iff for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r) )
let p be Point of (TOP-REAL n); ::_thesis: for p9 being Point of (Euclid n) st p = p9 holds
( p in Lim_inf S iff for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r) )
let p9 be Point of (Euclid n); ::_thesis: ( p = p9 implies ( p in Lim_inf S iff for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r) ) )
assume A1: p = p9 ; ::_thesis: ( p in Lim_inf S iff for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r) )
hereby ::_thesis: ( ( for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r) ) implies p in Lim_inf S )
assume A2: p in Lim_inf S ; ::_thesis: for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r)
let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r) )
assume r > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r)
then reconsider G = Ball (p9,r) as a_neighborhood of p by A1, GOBOARD6:2;
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G by A2, Def1;
hence ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r) ; ::_thesis: verum
end;
assume A3: for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r) ; ::_thesis: p in Lim_inf S
now__::_thesis:_for_G_being_a_neighborhood_of_p_ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_m_>_k_holds_
S_._m_meets_G
let G be a_neighborhood of p; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G
A4: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider G9 = Int G as Subset of (TopSpaceMetr (Euclid n)) ;
A5: p9 in G9 by A1, CONNSP_2:def_1;
G9 is open by A4, PRE_TOPC:30;
then consider r being real number such that
A6: r > 0 and
A7: Ball (p9,r) c= G9 by A5, TOPMETR:15;
consider k being Element of NAT such that
A8: for m being Element of NAT st m > k holds
S . m meets Ball (p9,r) by A3, A6;
take k = k; ::_thesis: for m being Element of NAT st m > k holds
S . m meets G
let m be Element of NAT ; ::_thesis: ( m > k implies S . m meets G )
assume m > k ; ::_thesis: S . m meets G
then ( G9 c= G & S . m meets Ball (p9,r) ) by A8, TOPS_1:16;
hence S . m meets G by A7, XBOOLE_1:1, XBOOLE_1:63; ::_thesis: verum
end;
hence p in Lim_inf S by Def1; ::_thesis: verum
end;
theorem Th15: :: KURATO_2:15
for T being non empty TopSpace
for S being SetSequence of the carrier of T holds Cl (Lim_inf S) = Lim_inf S
proof
let T be non empty TopSpace; ::_thesis: for S being SetSequence of the carrier of T holds Cl (Lim_inf S) = Lim_inf S
let S be SetSequence of the carrier of T; ::_thesis: Cl (Lim_inf S) = Lim_inf S
thus Cl (Lim_inf S) c= Lim_inf S :: according to XBOOLE_0:def_10 ::_thesis: Lim_inf S c= Cl (Lim_inf S)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl (Lim_inf S) or x in Lim_inf S )
assume A1: x in Cl (Lim_inf S) ; ::_thesis: x in Lim_inf S
then reconsider x9 = x as Point of T ;
now__::_thesis:_for_G_being_a_neighborhood_of_x9_ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_m_>_k_holds_
S_._m_meets_G
let G be a_neighborhood of x9; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G
set H = Int G;
x9 in Int G by CONNSP_2:def_1;
then Lim_inf S meets Int G by A1, PRE_TOPC:24;
then consider z being set such that
A2: z in Lim_inf S and
A3: z in Int G by XBOOLE_0:3;
reconsider z = z as Point of T by A2;
z in Int (Int G) by A3;
then Int G is a_neighborhood of z by CONNSP_2:def_1;
then consider k being Element of NAT such that
A4: for m being Element of NAT st m > k holds
S . m meets Int G by A2, Def1;
take k = k; ::_thesis: for m being Element of NAT st m > k holds
S . m meets G
let m be Element of NAT ; ::_thesis: ( m > k implies S . m meets G )
assume m > k ; ::_thesis: S . m meets G
then S . m meets Int G by A4;
hence S . m meets G by TOPS_1:16, XBOOLE_1:63; ::_thesis: verum
end;
hence x in Lim_inf S by Def1; ::_thesis: verum
end;
thus Lim_inf S c= Cl (Lim_inf S) by PRE_TOPC:18; ::_thesis: verum
end;
registration
let T be non empty TopSpace;
let S be SetSequence of the carrier of T;
cluster Lim_inf S -> closed ;
coherence
Lim_inf S is closed
proof
Lim_inf S = Cl (Lim_inf S) by Th15;
hence Lim_inf S is closed ; ::_thesis: verum
end;
end;
theorem :: KURATO_2:16
for T being non empty TopSpace
for R, S being SetSequence of the carrier of T st R is subsequence of S holds
Lim_inf S c= Lim_inf R
proof
let T be non empty TopSpace; ::_thesis: for R, S being SetSequence of the carrier of T st R is subsequence of S holds
Lim_inf S c= Lim_inf R
let R, S be SetSequence of the carrier of T; ::_thesis: ( R is subsequence of S implies Lim_inf S c= Lim_inf R )
assume R is subsequence of S ; ::_thesis: Lim_inf S c= Lim_inf R
then consider Nseq being increasing sequence of NAT such that
A1: R = S * Nseq by VALUED_0:def_17;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_inf S or x in Lim_inf R )
assume A2: x in Lim_inf S ; ::_thesis: x in Lim_inf R
then reconsider p = x as Point of T ;
for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
R . m meets G
proof
let G be a_neighborhood of p; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
R . m meets G
consider k being Element of NAT such that
A3: for m being Element of NAT st m > k holds
S . m meets G by A2, Def1;
take k ; ::_thesis: for m being Element of NAT st m > k holds
R . m meets G
let m1 be Element of NAT ; ::_thesis: ( m1 > k implies R . m1 meets G )
A4: m1 <= Nseq . m1 by SEQM_3:14;
assume m1 > k ; ::_thesis: R . m1 meets G
then A5: Nseq . m1 > k by A4, XXREAL_0:2;
dom Nseq = NAT by FUNCT_2:def_1;
then R . m1 = S . (Nseq . m1) by A1, FUNCT_1:13;
hence R . m1 meets G by A3, A5; ::_thesis: verum
end;
hence x in Lim_inf R by Def1; ::_thesis: verum
end;
theorem Th17: :: KURATO_2:17
for T being non empty TopSpace
for A, B being SetSequence of the carrier of T st ( for i being Element of NAT holds A . i c= B . i ) holds
Lim_inf A c= Lim_inf B
proof
let T be non empty TopSpace; ::_thesis: for A, B being SetSequence of the carrier of T st ( for i being Element of NAT holds A . i c= B . i ) holds
Lim_inf A c= Lim_inf B
let A, B be SetSequence of the carrier of T; ::_thesis: ( ( for i being Element of NAT holds A . i c= B . i ) implies Lim_inf A c= Lim_inf B )
assume A1: for i being Element of NAT holds A . i c= B . i ; ::_thesis: Lim_inf A c= Lim_inf B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_inf A or x in Lim_inf B )
assume A2: x in Lim_inf A ; ::_thesis: x in Lim_inf B
then reconsider p = x as Point of T ;
for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
B . m meets G
proof
let G be a_neighborhood of p; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
B . m meets G
consider k being Element of NAT such that
A3: for m being Element of NAT st m > k holds
A . m meets G by A2, Def1;
take k ; ::_thesis: for m being Element of NAT st m > k holds
B . m meets G
let m1 be Element of NAT ; ::_thesis: ( m1 > k implies B . m1 meets G )
assume m1 > k ; ::_thesis: B . m1 meets G
then A . m1 meets G by A3;
hence B . m1 meets G by A1, XBOOLE_1:63; ::_thesis: verum
end;
hence x in Lim_inf B by Def1; ::_thesis: verum
end;
theorem :: KURATO_2:18
for T being non empty TopSpace
for A, B, C being SetSequence of the carrier of T st ( for i being Element of NAT holds C . i = (A . i) \/ (B . i) ) holds
(Lim_inf A) \/ (Lim_inf B) c= Lim_inf C
proof
let T be non empty TopSpace; ::_thesis: for A, B, C being SetSequence of the carrier of T st ( for i being Element of NAT holds C . i = (A . i) \/ (B . i) ) holds
(Lim_inf A) \/ (Lim_inf B) c= Lim_inf C
let A, B, C be SetSequence of the carrier of T; ::_thesis: ( ( for i being Element of NAT holds C . i = (A . i) \/ (B . i) ) implies (Lim_inf A) \/ (Lim_inf B) c= Lim_inf C )
assume A1: for i being Element of NAT holds C . i = (A . i) \/ (B . i) ; ::_thesis: (Lim_inf A) \/ (Lim_inf B) c= Lim_inf C
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Lim_inf A) \/ (Lim_inf B) or x in Lim_inf C )
assume A2: x in (Lim_inf A) \/ (Lim_inf B) ; ::_thesis: x in Lim_inf C
then reconsider p = x as Point of T ;
percases ( x in Lim_inf A or x in Lim_inf B ) by A2, XBOOLE_0:def_3;
supposeA3: x in Lim_inf A ; ::_thesis: x in Lim_inf C
for H being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
C . m meets H
proof
let H be a_neighborhood of p; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
C . m meets H
consider k being Element of NAT such that
A4: for m being Element of NAT st m > k holds
A . m meets H by A3, Def1;
take k ; ::_thesis: for m being Element of NAT st m > k holds
C . m meets H
let m be Element of NAT ; ::_thesis: ( m > k implies C . m meets H )
assume m > k ; ::_thesis: C . m meets H
then A5: A . m meets H by A4;
C . m = (A . m) \/ (B . m) by A1;
hence C . m meets H by A5, XBOOLE_1:7, XBOOLE_1:63; ::_thesis: verum
end;
hence x in Lim_inf C by Def1; ::_thesis: verum
end;
supposeA6: x in Lim_inf B ; ::_thesis: x in Lim_inf C
for H being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
C . m meets H
proof
let H be a_neighborhood of p; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
C . m meets H
consider k being Element of NAT such that
A7: for m being Element of NAT st m > k holds
B . m meets H by A6, Def1;
take k ; ::_thesis: for m being Element of NAT st m > k holds
C . m meets H
let m be Element of NAT ; ::_thesis: ( m > k implies C . m meets H )
assume m > k ; ::_thesis: C . m meets H
then A8: B . m meets H by A7;
C . m = (A . m) \/ (B . m) by A1;
hence C . m meets H by A8, XBOOLE_1:7, XBOOLE_1:63; ::_thesis: verum
end;
hence x in Lim_inf C by Def1; ::_thesis: verum
end;
end;
end;
theorem :: KURATO_2:19
for T being non empty TopSpace
for A, B, C being SetSequence of the carrier of T st ( for i being Element of NAT holds C . i = (A . i) /\ (B . i) ) holds
Lim_inf C c= (Lim_inf A) /\ (Lim_inf B)
proof
let T be non empty TopSpace; ::_thesis: for A, B, C being SetSequence of the carrier of T st ( for i being Element of NAT holds C . i = (A . i) /\ (B . i) ) holds
Lim_inf C c= (Lim_inf A) /\ (Lim_inf B)
let A, B, C be SetSequence of the carrier of T; ::_thesis: ( ( for i being Element of NAT holds C . i = (A . i) /\ (B . i) ) implies Lim_inf C c= (Lim_inf A) /\ (Lim_inf B) )
assume A1: for i being Element of NAT holds C . i = (A . i) /\ (B . i) ; ::_thesis: Lim_inf C c= (Lim_inf A) /\ (Lim_inf B)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_inf C or x in (Lim_inf A) /\ (Lim_inf B) )
assume A2: x in Lim_inf C ; ::_thesis: x in (Lim_inf A) /\ (Lim_inf B)
then reconsider p = x as Point of T ;
for H being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
B . m meets H
proof
let H be a_neighborhood of p; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
B . m meets H
consider k being Element of NAT such that
A3: for m being Element of NAT st m > k holds
C . m meets H by A2, Def1;
take k ; ::_thesis: for m being Element of NAT st m > k holds
B . m meets H
let m be Element of NAT ; ::_thesis: ( m > k implies B . m meets H )
assume m > k ; ::_thesis: B . m meets H
then A4: C . m meets H by A3;
C . m = (A . m) /\ (B . m) by A1;
hence B . m meets H by A4, XBOOLE_1:17, XBOOLE_1:63; ::_thesis: verum
end;
then A5: x in Lim_inf B by Def1;
for H being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
A . m meets H
proof
let H be a_neighborhood of p; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
A . m meets H
consider k being Element of NAT such that
A6: for m being Element of NAT st m > k holds
C . m meets H by A2, Def1;
take k ; ::_thesis: for m being Element of NAT st m > k holds
A . m meets H
let m be Element of NAT ; ::_thesis: ( m > k implies A . m meets H )
assume m > k ; ::_thesis: A . m meets H
then A7: C . m meets H by A6;
C . m = (A . m) /\ (B . m) by A1;
hence A . m meets H by A7, XBOOLE_1:17, XBOOLE_1:63; ::_thesis: verum
end;
then x in Lim_inf A by Def1;
hence x in (Lim_inf A) /\ (Lim_inf B) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th20: :: KURATO_2:20
for T being non empty TopSpace
for F, G being SetSequence of the carrier of T st ( for i being Element of NAT holds G . i = Cl (F . i) ) holds
Lim_inf G = Lim_inf F
proof
let T be non empty TopSpace; ::_thesis: for F, G being SetSequence of the carrier of T st ( for i being Element of NAT holds G . i = Cl (F . i) ) holds
Lim_inf G = Lim_inf F
let F, G be SetSequence of the carrier of T; ::_thesis: ( ( for i being Element of NAT holds G . i = Cl (F . i) ) implies Lim_inf G = Lim_inf F )
assume A1: for i being Element of NAT holds G . i = Cl (F . i) ; ::_thesis: Lim_inf G = Lim_inf F
thus Lim_inf G c= Lim_inf F :: according to XBOOLE_0:def_10 ::_thesis: Lim_inf F c= Lim_inf G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_inf G or x in Lim_inf F )
assume A2: x in Lim_inf G ; ::_thesis: x in Lim_inf F
then reconsider p = x as Point of T ;
for H being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
F . m meets H
proof
let H be a_neighborhood of p; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
F . m meets H
consider H1 being non empty Subset of T such that
A3: H1 is a_neighborhood of p and
A4: H1 is open and
A5: H1 c= H by CONNSP_2:5;
consider k being Element of NAT such that
A6: for m being Element of NAT st m > k holds
G . m meets H1 by A2, A3, Def1;
take k ; ::_thesis: for m being Element of NAT st m > k holds
F . m meets H
let m be Element of NAT ; ::_thesis: ( m > k implies F . m meets H )
assume m > k ; ::_thesis: F . m meets H
then G . m meets H1 by A6;
then consider y being set such that
A7: y in G . m and
A8: y in H1 by XBOOLE_0:3;
reconsider y = y as Point of T by A7;
H1 is a_neighborhood of y by A4, A8, CONNSP_2:3;
then consider H9 being non empty Subset of T such that
A9: H9 is a_neighborhood of y and
H9 is open and
A10: H9 c= H1 by CONNSP_2:5;
y in Cl (F . m) by A1, A7;
then H9 meets F . m by A9, CONNSP_2:27;
then H1 meets F . m by A10, XBOOLE_1:63;
hence F . m meets H by A5, XBOOLE_1:63; ::_thesis: verum
end;
hence x in Lim_inf F by Def1; ::_thesis: verum
end;
for i being Element of NAT holds F . i c= G . i
proof
let i be Element of NAT ; ::_thesis: F . i c= G . i
G . i = Cl (F . i) by A1;
hence F . i c= G . i by PRE_TOPC:18; ::_thesis: verum
end;
hence Lim_inf F c= Lim_inf G by Th17; ::_thesis: verum
end;
theorem :: KURATO_2:21
for n being Element of NAT
for S being SetSequence of the carrier of (TOP-REAL n)
for p being Point of (TOP-REAL n) st ex s being Real_Sequence of n st
( s is convergent & ( for x being Element of NAT holds s . x in S . x ) & p = lim s ) holds
p in Lim_inf S
proof
let n be Element of NAT ; ::_thesis: for S being SetSequence of the carrier of (TOP-REAL n)
for p being Point of (TOP-REAL n) st ex s being Real_Sequence of n st
( s is convergent & ( for x being Element of NAT holds s . x in S . x ) & p = lim s ) holds
p in Lim_inf S
let S be SetSequence of the carrier of (TOP-REAL n); ::_thesis: for p being Point of (TOP-REAL n) st ex s being Real_Sequence of n st
( s is convergent & ( for x being Element of NAT holds s . x in S . x ) & p = lim s ) holds
p in Lim_inf S
let p be Point of (TOP-REAL n); ::_thesis: ( ex s being Real_Sequence of n st
( s is convergent & ( for x being Element of NAT holds s . x in S . x ) & p = lim s ) implies p in Lim_inf S )
reconsider p9 = p as Point of (Euclid n) by TOPREAL3:8;
given s being Real_Sequence of n such that A1: s is convergent and
A2: for x being Element of NAT holds s . x in S . x and
A3: p = lim s ; ::_thesis: p in Lim_inf S
for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r)
proof
let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r) )
reconsider r9 = r as Real by XREAL_0:def_1;
assume r > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r)
then consider l being Element of NAT such that
A4: for m being Element of NAT st l <= m holds
|.((s . m) - p).| < r9 by A1, A3, TOPRNS_1:def_9;
take v = max (0,l); ::_thesis: for m being Element of NAT st m > v holds
S . m meets Ball (p9,r)
let m be Element of NAT ; ::_thesis: ( m > v implies S . m meets Ball (p9,r) )
assume v < m ; ::_thesis: S . m meets Ball (p9,r)
then l <= m by XXREAL_0:30;
then |.((s . m) - p).| < r9 by A4;
then A5: s . m in Ball (p9,r) by Th3;
s . m in S . m by A2;
hence S . m meets Ball (p9,r) by A5, XBOOLE_0:3; ::_thesis: verum
end;
hence p in Lim_inf S by Th14; ::_thesis: verum
end;
theorem Th22: :: KURATO_2:22
for T being non empty TopSpace
for P being Subset of T
for s being SetSequence of the carrier of T st ( for i being Nat holds s . i c= P ) holds
Lim_inf s c= Cl P
proof
let T be non empty TopSpace; ::_thesis: for P being Subset of T
for s being SetSequence of the carrier of T st ( for i being Nat holds s . i c= P ) holds
Lim_inf s c= Cl P
let P be Subset of T; ::_thesis: for s being SetSequence of the carrier of T st ( for i being Nat holds s . i c= P ) holds
Lim_inf s c= Cl P
let s be SetSequence of the carrier of T; ::_thesis: ( ( for i being Nat holds s . i c= P ) implies Lim_inf s c= Cl P )
assume A1: for i being Nat holds s . i c= P ; ::_thesis: Lim_inf s c= Cl P
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_inf s or x in Cl P )
assume A2: x in Lim_inf s ; ::_thesis: x in Cl P
then reconsider p = x as Point of T ;
for G being Subset of T st G is open & p in G holds
P meets G
proof
let G be Subset of T; ::_thesis: ( G is open & p in G implies P meets G )
assume A3: G is open ; ::_thesis: ( not p in G or P meets G )
assume p in G ; ::_thesis: P meets G
then reconsider G9 = G as a_neighborhood of p by A3, CONNSP_2:3;
consider k being Element of NAT such that
A4: for m being Element of NAT st m > k holds
s . m meets G9 by A2, Def1;
set m = k + 1;
k + 1 > k by NAT_1:13;
then s . (k + 1) meets G9 by A4;
hence P meets G by A1, XBOOLE_1:63; ::_thesis: verum
end;
hence x in Cl P by PRE_TOPC:def_7; ::_thesis: verum
end;
theorem Th23: :: KURATO_2:23
for T being non empty TopSpace
for F being SetSequence of the carrier of T
for A being Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = Cl A
proof
let T be non empty TopSpace; ::_thesis: for F being SetSequence of the carrier of T
for A being Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = Cl A
let F be SetSequence of the carrier of T; ::_thesis: for A being Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = Cl A
let A be Subset of T; ::_thesis: ( ( for i being Nat holds F . i = A ) implies Lim_inf F = Cl A )
assume A1: for i being Nat holds F . i = A ; ::_thesis: Lim_inf F = Cl A
then for i being Nat holds F . i c= A ;
hence Lim_inf F c= Cl A by Th22; :: according to XBOOLE_0:def_10 ::_thesis: Cl A c= Lim_inf F
thus Cl A c= Lim_inf F ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in Lim_inf F )
assume A2: x in Cl A ; ::_thesis: x in Lim_inf F
then reconsider p = x as Point of T ;
for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
F . m meets G
proof
let G be a_neighborhood of p; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
F . m meets G
take k = 1; ::_thesis: for m being Element of NAT st m > k holds
F . m meets G
let m be Element of NAT ; ::_thesis: ( m > k implies F . m meets G )
assume m > k ; ::_thesis: F . m meets G
F . m = A by A1;
hence F . m meets G by A2, CONNSP_2:27; ::_thesis: verum
end;
hence x in Lim_inf F by Def1; ::_thesis: verum
end;
end;
theorem :: KURATO_2:24
for T being non empty TopSpace
for F being SetSequence of the carrier of T
for A being closed Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = A
proof
let T be non empty TopSpace; ::_thesis: for F being SetSequence of the carrier of T
for A being closed Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = A
let F be SetSequence of the carrier of T; ::_thesis: for A being closed Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = A
let A be closed Subset of T; ::_thesis: ( ( for i being Nat holds F . i = A ) implies Lim_inf F = A )
assume for i being Nat holds F . i = A ; ::_thesis: Lim_inf F = A
then Lim_inf F = Cl A by Th23;
hence Lim_inf F = A by PRE_TOPC:22; ::_thesis: verum
end;
theorem Th25: :: KURATO_2:25
for n being Element of NAT
for S being SetSequence of the carrier of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st P is bounded & ( for i being Element of NAT holds S . i c= P ) holds
Lim_inf S is bounded
proof
let n be Element of NAT ; ::_thesis: for S being SetSequence of the carrier of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st P is bounded & ( for i being Element of NAT holds S . i c= P ) holds
Lim_inf S is bounded
let S be SetSequence of the carrier of (TOP-REAL n); ::_thesis: for P being Subset of (TOP-REAL n) st P is bounded & ( for i being Element of NAT holds S . i c= P ) holds
Lim_inf S is bounded
let P be Subset of (TOP-REAL n); ::_thesis: ( P is bounded & ( for i being Element of NAT holds S . i c= P ) implies Lim_inf S is bounded )
assume that
A1: P is bounded and
A2: for i being Element of NAT holds S . i c= P ; ::_thesis: Lim_inf S is bounded
reconsider P9 = P as bounded Subset of (Euclid n) by A1, JORDAN2C:11;
consider t being Real, z being Point of (Euclid n) such that
A3: 0 < t and
A4: P9 c= Ball (z,t) by METRIC_6:def_3;
set r = 1;
set R = (1 + 1) + (3 * t);
assume not Lim_inf S is bounded ; ::_thesis: contradiction
then consider x, y being Point of (Euclid n) such that
A5: x in Lim_inf S and
A6: y in Lim_inf S and
A7: dist (x,y) > (1 + 1) + (3 * t) by A3, Th8;
consider k1 being Element of NAT such that
A8: for m being Element of NAT st m > k1 holds
S . m meets Ball (x,1) by A5, Th14;
consider k2 being Element of NAT such that
A9: for m being Element of NAT st m > k2 holds
S . m meets Ball (y,1) by A6, Th14;
set k = (max (k1,k2)) + 1;
S . ((max (k1,k2)) + 1) c= P9 by A2;
then A10: S . ((max (k1,k2)) + 1) c= Ball (z,t) by A4, XBOOLE_1:1;
2 * t < 3 * t by A3, XREAL_1:68;
then A11: (1 + 1) + (2 * t) < (1 + 1) + (3 * t) by XREAL_1:8;
max (k1,k2) >= k2 by XXREAL_0:25;
then (max (k1,k2)) + 1 > k2 by NAT_1:13;
then A12: Ball (z,t) meets Ball (y,1) by A9, A10, XBOOLE_1:63;
max (k1,k2) >= k1 by XXREAL_0:25;
then (max (k1,k2)) + 1 > k1 by NAT_1:13;
then Ball (z,t) meets Ball (x,1) by A8, A10, XBOOLE_1:63;
hence contradiction by A7, A12, A11, Th10, XXREAL_0:2; ::_thesis: verum
end;
theorem :: KURATO_2:26
for S being SetSequence of the carrier of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st P is bounded & ( for i being Element of NAT holds S . i c= P ) holds
Lim_inf S is compact by Th25, TOPREAL6:79;
theorem Th27: :: KURATO_2:27
for n being Element of NAT
for A, B being SetSequence of the carrier of (TOP-REAL n)
for C being SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):] st ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) holds
[:(Lim_inf A),(Lim_inf B):] = Lim_inf C
proof
let n be Element of NAT ; ::_thesis: for A, B being SetSequence of the carrier of (TOP-REAL n)
for C being SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):] st ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) holds
[:(Lim_inf A),(Lim_inf B):] = Lim_inf C
let A, B be SetSequence of the carrier of (TOP-REAL n); ::_thesis: for C being SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):] st ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) holds
[:(Lim_inf A),(Lim_inf B):] = Lim_inf C
let C be SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):]; ::_thesis: ( ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) implies [:(Lim_inf A),(Lim_inf B):] = Lim_inf C )
assume A1: for i being Element of NAT holds C . i = [:(A . i),(B . i):] ; ::_thesis: [:(Lim_inf A),(Lim_inf B):] = Lim_inf C
thus [:(Lim_inf A),(Lim_inf B):] c= Lim_inf C :: according to XBOOLE_0:def_10 ::_thesis: Lim_inf C c= [:(Lim_inf A),(Lim_inf B):]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:(Lim_inf A),(Lim_inf B):] or x in Lim_inf C )
assume A2: x in [:(Lim_inf A),(Lim_inf B):] ; ::_thesis: x in Lim_inf C
then consider x1, x2 being set such that
A3: x1 in Lim_inf A and
A4: x2 in Lim_inf B and
A5: x = [x1,x2] by ZFMISC_1:def_2;
reconsider p = x as Point of [:(TOP-REAL n),(TOP-REAL n):] by A2;
reconsider x1 = x1, x2 = x2 as Point of (TOP-REAL n) by A3, A4;
for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
C . m meets G
proof
let G be a_neighborhood of p; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
C . m meets G
G is a_neighborhood of [:{x1},{x2}:] by A5, Th11;
then consider V being a_neighborhood of {x1}, W being a_neighborhood of x2 such that
A6: [:V,W:] c= G by BORSUK_1:25;
consider k2 being Element of NAT such that
A7: for m being Element of NAT st m > k2 holds
B . m meets W by A4, Def1;
V is a_neighborhood of x1 by CONNSP_2:8;
then consider k1 being Element of NAT such that
A8: for m being Element of NAT st m > k1 holds
A . m meets V by A3, Def1;
take k = max (k1,k2); ::_thesis: for m being Element of NAT st m > k holds
C . m meets G
let m be Element of NAT ; ::_thesis: ( m > k implies C . m meets G )
assume A9: m > k ; ::_thesis: C . m meets G
k >= k2 by XXREAL_0:25;
then m > k2 by A9, XXREAL_0:2;
then A10: B . m meets W by A7;
k >= k1 by XXREAL_0:25;
then m > k1 by A9, XXREAL_0:2;
then A . m meets V by A8;
then [:(A . m),(B . m):] meets [:V,W:] by A10, KURATO_0:2;
then C . m meets [:V,W:] by A1;
hence C . m meets G by A6, XBOOLE_1:63; ::_thesis: verum
end;
hence x in Lim_inf C by Def1; ::_thesis: verum
end;
thus Lim_inf C c= [:(Lim_inf A),(Lim_inf B):] ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_inf C or x in [:(Lim_inf A),(Lim_inf B):] )
assume A11: x in Lim_inf C ; ::_thesis: x in [:(Lim_inf A),(Lim_inf B):]
then x in the carrier of [:(TOP-REAL n),(TOP-REAL n):] ;
then A12: x in [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] by BORSUK_1:def_2;
then reconsider p1 = x `1 , p2 = x `2 as Point of (TOP-REAL n) by MCART_1:10;
set H = the a_neighborhood of p2;
set F = the a_neighborhood of p1;
A13: x = [p1,p2] by A12, MCART_1:21;
for G being a_neighborhood of p2 ex k being Element of NAT st
for m being Element of NAT st m > k holds
B . m meets G
proof
let G be a_neighborhood of p2; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
B . m meets G
consider k being Element of NAT such that
A14: for m being Element of NAT st m > k holds
C . m meets [: the a_neighborhood of p1,G:] by A11, A13, Def1;
take k ; ::_thesis: for m being Element of NAT st m > k holds
B . m meets G
let m be Element of NAT ; ::_thesis: ( m > k implies B . m meets G )
assume m > k ; ::_thesis: B . m meets G
then C . m meets [: the a_neighborhood of p1,G:] by A14;
then consider y being set such that
A15: y in C . m and
A16: y in [: the a_neighborhood of p1,G:] by XBOOLE_0:3;
y in [:(A . m),(B . m):] by A1, A15;
then A17: y `2 in B . m by MCART_1:10;
y `2 in G by A16, MCART_1:10;
hence B . m meets G by A17, XBOOLE_0:3; ::_thesis: verum
end;
then A18: p2 in Lim_inf B by Def1;
for G being a_neighborhood of p1 ex k being Element of NAT st
for m being Element of NAT st m > k holds
A . m meets G
proof
let G be a_neighborhood of p1; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
A . m meets G
consider k being Element of NAT such that
A19: for m being Element of NAT st m > k holds
C . m meets [:G, the a_neighborhood of p2:] by A11, A13, Def1;
take k ; ::_thesis: for m being Element of NAT st m > k holds
A . m meets G
let m be Element of NAT ; ::_thesis: ( m > k implies A . m meets G )
assume m > k ; ::_thesis: A . m meets G
then C . m meets [:G, the a_neighborhood of p2:] by A19;
then consider y being set such that
A20: y in C . m and
A21: y in [:G, the a_neighborhood of p2:] by XBOOLE_0:3;
y in [:(A . m),(B . m):] by A1, A20;
then A22: y `1 in A . m by MCART_1:10;
y `1 in G by A21, MCART_1:10;
hence A . m meets G by A22, XBOOLE_0:3; ::_thesis: verum
end;
then p1 in Lim_inf A by Def1;
hence x in [:(Lim_inf A),(Lim_inf B):] by A13, A18, ZFMISC_1:87; ::_thesis: verum
end;
end;
theorem :: KURATO_2:28
for S being SetSequence of (TOP-REAL 2) holds lim_inf S c= Lim_inf S
proof
let S be SetSequence of (TOP-REAL 2); ::_thesis: lim_inf S c= Lim_inf S
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_inf S or x in Lim_inf S )
assume A1: x in lim_inf S ; ::_thesis: x in Lim_inf S
then reconsider p = x as Point of (Euclid 2) by TOPREAL3:8;
reconsider y = x as Point of (TOP-REAL 2) by A1;
consider k being Element of NAT such that
A2: for n being Element of NAT holds x in S . (k + n) by A1, KURATO_0:4;
for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p,r)
proof
let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p,r) )
assume r > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p,r)
then A3: x in Ball (p,r) by GOBOARD6:1;
take k ; ::_thesis: for m being Element of NAT st m > k holds
S . m meets Ball (p,r)
let m be Element of NAT ; ::_thesis: ( m > k implies S . m meets Ball (p,r) )
assume m > k ; ::_thesis: S . m meets Ball (p,r)
then consider h being Nat such that
A4: m = k + h by NAT_1:10;
h in NAT by ORDINAL1:def_12;
then x in S . m by A2, A4;
hence S . m meets Ball (p,r) by A3, XBOOLE_0:3; ::_thesis: verum
end;
then y in Lim_inf S by Th14;
hence x in Lim_inf S ; ::_thesis: verum
end;
theorem :: KURATO_2:29
for C being Simple_closed_curve
for i being Element of NAT holds Fr ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i))
proof
let C be Simple_closed_curve; ::_thesis: for i being Element of NAT holds Fr ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i))
let i be Element of NAT ; ::_thesis: Fr ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i))
set K = (UBD (L~ (Cage (C,i)))) ` ;
set R = L~ (Cage (C,i));
A1: (BDD (L~ (Cage (C,i)))) \/ ((BDD (L~ (Cage (C,i)))) `) = [#] (TOP-REAL 2) by PRE_TOPC:2;
UBD (L~ (Cage (C,i))) c= (L~ (Cage (C,i))) ` by JORDAN2C:26;
then A2: UBD (L~ (Cage (C,i))) misses L~ (Cage (C,i)) by SUBSET_1:23;
UBD (L~ (Cage (C,i))) misses BDD (L~ (Cage (C,i))) by JORDAN2C:24;
then A3: UBD (L~ (Cage (C,i))) misses (BDD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i))) by A2, XBOOLE_1:70;
[#] (TOP-REAL 2) = ((L~ (Cage (C,i))) `) \/ (L~ (Cage (C,i))) by PRE_TOPC:2
.= ((BDD (L~ (Cage (C,i)))) \/ (UBD (L~ (Cage (C,i))))) \/ (L~ (Cage (C,i))) by JORDAN2C:27 ;
then A4: (UBD (L~ (Cage (C,i)))) ` = ((UBD (L~ (Cage (C,i)))) \/ ((BDD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i))))) \ (UBD (L~ (Cage (C,i)))) by XBOOLE_1:4
.= (L~ (Cage (C,i))) \/ (BDD (L~ (Cage (C,i)))) by A3, XBOOLE_1:88 ;
((BDD (L~ (Cage (C,i)))) \/ (UBD (L~ (Cage (C,i))))) ` = ((L~ (Cage (C,i))) `) ` by JORDAN2C:27;
then ((BDD (L~ (Cage (C,i)))) `) /\ ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i)) by XBOOLE_1:53;
then (BDD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i))) = ((BDD (L~ (Cage (C,i)))) \/ ((BDD (L~ (Cage (C,i)))) `)) /\ ((BDD (L~ (Cage (C,i)))) \/ ((UBD (L~ (Cage (C,i)))) `)) by XBOOLE_1:24
.= (BDD (L~ (Cage (C,i)))) \/ ((UBD (L~ (Cage (C,i)))) `) by A1, XBOOLE_1:28
.= (UBD (L~ (Cage (C,i)))) ` by A4, XBOOLE_1:7, XBOOLE_1:12 ;
then A5: Cl ((UBD (L~ (Cage (C,i)))) `) = (BDD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i))) by PRE_TOPC:22;
A6: ((UBD (L~ (Cage (C,i)))) `) ` = LeftComp (Cage (C,i)) by GOBRD14:36;
BDD (L~ (Cage (C,i))) misses UBD (L~ (Cage (C,i))) by JORDAN2C:24;
then A7: (BDD (L~ (Cage (C,i)))) /\ (UBD (L~ (Cage (C,i)))) = {} by XBOOLE_0:def_7;
Fr ((UBD (L~ (Cage (C,i)))) `) = (Cl ((UBD (L~ (Cage (C,i)))) `)) /\ (Cl (((UBD (L~ (Cage (C,i)))) `) `)) by TOPS_1:def_2
.= ((BDD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i)))) /\ ((UBD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i)))) by A5, A6, GOBRD14:22
.= ((BDD (L~ (Cage (C,i)))) /\ (UBD (L~ (Cage (C,i))))) \/ (L~ (Cage (C,i))) by XBOOLE_1:24
.= L~ (Cage (C,i)) by A7 ;
hence Fr ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i)) ; ::_thesis: verum
end;
begin
definition
let T be non empty TopSpace;
let S be SetSequence of the carrier of T;
func Lim_sup S -> Subset of T means :Def2: :: KURATO_2:def 2
for x being set holds
( x in it iff ex A being subsequence of S st x in Lim_inf A );
existence
ex b1 being Subset of T st
for x being set holds
( x in b1 iff ex A being subsequence of S st x in Lim_inf A )
proof
defpred S1[ set ] means ex A being subsequence of S st $1 in Lim_inf A;
consider X being set such that
A1: for x being set holds
( x in X iff ( x in the carrier of T & S1[x] ) ) from XBOOLE_0:sch_1();
X c= the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in the carrier of T )
assume x in X ; ::_thesis: x in the carrier of T
hence x in the carrier of T by A1; ::_thesis: verum
end;
then reconsider X = X as Subset of T ;
take X ; ::_thesis: for x being set holds
( x in X iff ex A being subsequence of S st x in Lim_inf A )
thus for x being set holds
( x in X iff ex A being subsequence of S st x in Lim_inf A ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of T st ( for x being set holds
( x in b1 iff ex A being subsequence of S st x in Lim_inf A ) ) & ( for x being set holds
( x in b2 iff ex A being subsequence of S st x in Lim_inf A ) ) holds
b1 = b2
proof
defpred S1[ set ] means ex A being subsequence of S st $1 in Lim_inf A;
let A1, A2 be Subset of T; ::_thesis: ( ( for x being set holds
( x in A1 iff ex A being subsequence of S st x in Lim_inf A ) ) & ( for x being set holds
( x in A2 iff ex A being subsequence of S st x in Lim_inf A ) ) implies A1 = A2 )
assume that
A2: for x being set holds
( x in A1 iff S1[x] ) and
A3: for x being set holds
( x in A2 iff S1[x] ) ; ::_thesis: A1 = A2
A1 = A2 from XBOOLE_0:sch_2(A2, A3);
hence A1 = A2 ; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Lim_sup KURATO_2:def_2_:_
for T being non empty TopSpace
for S being SetSequence of the carrier of T
for b3 being Subset of T holds
( b3 = Lim_sup S iff for x being set holds
( x in b3 iff ex A being subsequence of S st x in Lim_inf A ) );
theorem :: KURATO_2:30
for N being Element of NAT
for F being sequence of (TOP-REAL N)
for x being Point of (TOP-REAL N)
for x9 being Point of (Euclid N) st x = x9 holds
( x is_a_cluster_point_of F iff for r being real number
for n being Element of NAT st r > 0 holds
ex m being Element of NAT st
( n <= m & F . m in Ball (x9,r) ) )
proof
let N be Element of NAT ; ::_thesis: for F being sequence of (TOP-REAL N)
for x being Point of (TOP-REAL N)
for x9 being Point of (Euclid N) st x = x9 holds
( x is_a_cluster_point_of F iff for r being real number
for n being Element of NAT st r > 0 holds
ex m being Element of NAT st
( n <= m & F . m in Ball (x9,r) ) )
let F be sequence of (TOP-REAL N); ::_thesis: for x being Point of (TOP-REAL N)
for x9 being Point of (Euclid N) st x = x9 holds
( x is_a_cluster_point_of F iff for r being real number
for n being Element of NAT st r > 0 holds
ex m being Element of NAT st
( n <= m & F . m in Ball (x9,r) ) )
let x be Point of (TOP-REAL N); ::_thesis: for x9 being Point of (Euclid N) st x = x9 holds
( x is_a_cluster_point_of F iff for r being real number
for n being Element of NAT st r > 0 holds
ex m being Element of NAT st
( n <= m & F . m in Ball (x9,r) ) )
let x9 be Point of (Euclid N); ::_thesis: ( x = x9 implies ( x is_a_cluster_point_of F iff for r being real number
for n being Element of NAT st r > 0 holds
ex m being Element of NAT st
( n <= m & F . m in Ball (x9,r) ) ) )
assume A1: x = x9 ; ::_thesis: ( x is_a_cluster_point_of F iff for r being real number
for n being Element of NAT st r > 0 holds
ex m being Element of NAT st
( n <= m & F . m in Ball (x9,r) ) )
hereby ::_thesis: ( ( for r being real number
for n being Element of NAT st r > 0 holds
ex m being Element of NAT st
( n <= m & F . m in Ball (x9,r) ) ) implies x is_a_cluster_point_of F )
assume A2: x is_a_cluster_point_of F ; ::_thesis: for r being real number
for n being Element of NAT st r > 0 holds
ex m being Element of NAT st
( n <= m & F . m in Ball (x9,r) )
let r be real number ; ::_thesis: for n being Element of NAT st r > 0 holds
ex m being Element of NAT st
( n <= m & F . m in Ball (x9,r) )
let n be Element of NAT ; ::_thesis: ( r > 0 implies ex m being Element of NAT st
( n <= m & F . m in Ball (x9,r) ) )
reconsider O = Ball (x9,r) as open Subset of (TOP-REAL N) by Th1;
assume r > 0 ; ::_thesis: ex m being Element of NAT st
( n <= m & F . m in Ball (x9,r) )
then x in O by A1, GOBOARD6:1;
then consider m being Element of NAT such that
A3: ( n <= m & F . m in O ) by A2, FRECHET2:def_3;
reconsider m = m as Element of NAT ;
take m = m; ::_thesis: ( n <= m & F . m in Ball (x9,r) )
thus ( n <= m & F . m in Ball (x9,r) ) by A3; ::_thesis: verum
end;
assume A4: for r being real number
for n being Element of NAT st r > 0 holds
ex m being Element of NAT st
( n <= m & F . m in Ball (x9,r) ) ; ::_thesis: x is_a_cluster_point_of F
for O being Subset of (TOP-REAL N)
for n being Element of NAT st O is open & x in O holds
ex m being Element of NAT st
( n <= m & F . m in O )
proof
let O be Subset of (TOP-REAL N); ::_thesis: for n being Element of NAT st O is open & x in O holds
ex m being Element of NAT st
( n <= m & F . 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 & F . m in O ) )
assume that
A5: O is open and
A6: x in O ; ::_thesis: ex m being Element of NAT st
( n <= m & F . m in O )
reconsider n9 = n as Element of NAT ;
A7: TopStruct(# the carrier of (TOP-REAL N), the topology of (TOP-REAL N) #) = TopSpaceMetr (Euclid N) by EUCLID:def_8;
then reconsider G9 = O as Subset of (TopSpaceMetr (Euclid N)) ;
G9 is open by A5, A7, PRE_TOPC:30;
then consider r being real number such that
A8: r > 0 and
A9: Ball (x9,r) c= G9 by A1, A6, TOPMETR:15;
consider m being Element of NAT such that
A10: ( n9 <= m & F . m in Ball (x9,r) ) by A4, A8;
take m ; ::_thesis: ( n <= m & F . m in O )
thus ( n <= m & F . m in O ) by A9, A10; ::_thesis: verum
end;
hence x is_a_cluster_point_of F by FRECHET2:def_3; ::_thesis: verum
end;
theorem Th31: :: KURATO_2:31
for T being non empty TopSpace
for A being SetSequence of the carrier of T holds Lim_inf A c= Lim_sup A
proof
let T be non empty TopSpace; ::_thesis: for A being SetSequence of the carrier of T holds Lim_inf A c= Lim_sup A
let A be SetSequence of the carrier of T; ::_thesis: Lim_inf A c= Lim_sup A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_inf A or x in Lim_sup A )
assume A1: x in Lim_inf A ; ::_thesis: x in Lim_sup A
ex K being subsequence of A st x in Lim_inf K
proof
reconsider B = A as subsequence of A by VALUED_0:19;
take B ; ::_thesis: x in Lim_inf B
thus x in Lim_inf B by A1; ::_thesis: verum
end;
hence x in Lim_sup A by Def2; ::_thesis: verum
end;
theorem Th32: :: KURATO_2:32
for A, B, C being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds A . i c= B . i ) & C is subsequence of A holds
ex D being subsequence of B st
for i being Element of NAT holds C . i c= D . i
proof
let A, B, C be SetSequence of the carrier of (TOP-REAL 2); ::_thesis: ( ( for i being Element of NAT holds A . i c= B . i ) & C is subsequence of A implies ex D being subsequence of B st
for i being Element of NAT holds C . i c= D . i )
assume that
A1: for i being Element of NAT holds A . i c= B . i and
A2: C is subsequence of A ; ::_thesis: ex D being subsequence of B st
for i being Element of NAT holds C . i c= D . i
consider NS being increasing sequence of NAT such that
A3: C = A * NS by A2, VALUED_0:def_17;
set D = B * NS;
reconsider D = B * NS as SetSequence of (TOP-REAL 2) ;
reconsider D = D as subsequence of B ;
take D ; ::_thesis: for i being Element of NAT holds C . i c= D . i
for i being Element of NAT holds C . i c= D . i
proof
let i be Element of NAT ; ::_thesis: C . i c= D . i
A4: dom NS = NAT by FUNCT_2:def_1;
C . i c= D . i
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C . i or x in D . i )
assume x in C . i ; ::_thesis: x in D . i
then A5: x in A . (NS . i) by A3, A4, FUNCT_1:13;
A . (NS . i) c= B . (NS . i) by A1;
then x in B . (NS . i) by A5;
hence x in D . i by A4, FUNCT_1:13; ::_thesis: verum
end;
hence C . i c= D . i ; ::_thesis: verum
end;
hence for i being Element of NAT holds C . i c= D . i ; ::_thesis: verum
end;
theorem :: KURATO_2:33
for A, B, C being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds A . i c= B . i ) & C is subsequence of B holds
ex D being subsequence of A st
for i being Element of NAT holds D . i c= C . i
proof
let A, B, C be SetSequence of the carrier of (TOP-REAL 2); ::_thesis: ( ( for i being Element of NAT holds A . i c= B . i ) & C is subsequence of B implies ex D being subsequence of A st
for i being Element of NAT holds D . i c= C . i )
assume that
A1: for i being Element of NAT holds A . i c= B . i and
A2: C is subsequence of B ; ::_thesis: ex D being subsequence of A st
for i being Element of NAT holds D . i c= C . i
consider NS being increasing sequence of NAT such that
A3: C = B * NS by A2, VALUED_0:def_17;
set D = A * NS;
reconsider D = A * NS as SetSequence of (TOP-REAL 2) ;
reconsider D = D as subsequence of A ;
take D ; ::_thesis: for i being Element of NAT holds D . i c= C . i
for i being Element of NAT holds D . i c= C . i
proof
let i be Element of NAT ; ::_thesis: D . i c= C . i
A4: dom NS = NAT by FUNCT_2:def_1;
D . i c= C . i
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D . i or x in C . i )
assume x in D . i ; ::_thesis: x in C . i
then A5: x in A . (NS . i) by A4, FUNCT_1:13;
A . (NS . i) c= B . (NS . i) by A1;
then x in B . (NS . i) by A5;
hence x in C . i by A3, A4, FUNCT_1:13; ::_thesis: verum
end;
hence D . i c= C . i ; ::_thesis: verum
end;
hence for i being Element of NAT holds D . i c= C . i ; ::_thesis: verum
end;
theorem Th34: :: KURATO_2:34
for A, B being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds A . i c= B . i ) holds
Lim_sup A c= Lim_sup B
proof
let A, B be SetSequence of the carrier of (TOP-REAL 2); ::_thesis: ( ( for i being Element of NAT holds A . i c= B . i ) implies Lim_sup A c= Lim_sup B )
assume A1: for i being Element of NAT holds A . i c= B . i ; ::_thesis: Lim_sup A c= Lim_sup B
Lim_sup A c= Lim_sup B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_sup A or x in Lim_sup B )
assume x in Lim_sup A ; ::_thesis: x in Lim_sup B
then consider A1 being subsequence of A such that
A2: x in Lim_inf A1 by Def2;
consider D being subsequence of B such that
A3: for i being Element of NAT holds A1 . i c= D . i by A1, Th32;
Lim_inf A1 c= Lim_inf D by A3, Th17;
hence x in Lim_sup B by A2, Def2; ::_thesis: verum
end;
hence Lim_sup A c= Lim_sup B ; ::_thesis: verum
end;
theorem :: KURATO_2:35
for A, B, C being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds C . i = (A . i) \/ (B . i) ) holds
(Lim_sup A) \/ (Lim_sup B) c= Lim_sup C
proof
let A, B, C be SetSequence of the carrier of (TOP-REAL 2); ::_thesis: ( ( for i being Element of NAT holds C . i = (A . i) \/ (B . i) ) implies (Lim_sup A) \/ (Lim_sup B) c= Lim_sup C )
assume A1: for i being Element of NAT holds C . i = (A . i) \/ (B . i) ; ::_thesis: (Lim_sup A) \/ (Lim_sup B) c= Lim_sup C
A2: for i being Element of NAT holds B . i c= C . i
proof
let i be Element of NAT ; ::_thesis: B . i c= C . i
C . i = (A . i) \/ (B . i) by A1;
hence B . i c= C . i by XBOOLE_1:7; ::_thesis: verum
end;
A3: for i being Element of NAT holds A . i c= C . i
proof
let i be Element of NAT ; ::_thesis: A . i c= C . i
C . i = (A . i) \/ (B . i) by A1;
hence A . i c= C . i by XBOOLE_1:7; ::_thesis: verum
end;
thus (Lim_sup A) \/ (Lim_sup B) c= Lim_sup C ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Lim_sup A) \/ (Lim_sup B) or x in Lim_sup C )
assume A4: x in (Lim_sup A) \/ (Lim_sup B) ; ::_thesis: x in Lim_sup C
percases ( x in Lim_sup A or x in Lim_sup B ) by A4, XBOOLE_0:def_3;
suppose x in Lim_sup A ; ::_thesis: x in Lim_sup C
then consider A1 being subsequence of A such that
A5: x in Lim_inf A1 by Def2;
consider C1 being subsequence of C such that
A6: for i being Element of NAT holds A1 . i c= C1 . i by A3, Th32;
Lim_inf A1 c= Lim_inf C1 by A6, Th17;
hence x in Lim_sup C by A5, Def2; ::_thesis: verum
end;
suppose x in Lim_sup B ; ::_thesis: x in Lim_sup C
then consider B1 being subsequence of B such that
A7: x in Lim_inf B1 by Def2;
consider C1 being subsequence of C such that
A8: for i being Element of NAT holds B1 . i c= C1 . i by A2, Th32;
Lim_inf B1 c= Lim_inf C1 by A8, Th17;
hence x in Lim_sup C by A7, Def2; ::_thesis: verum
end;
end;
end;
end;
theorem :: KURATO_2:36
for A, B, C being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds C . i = (A . i) /\ (B . i) ) holds
Lim_sup C c= (Lim_sup A) /\ (Lim_sup B)
proof
let A, B, C be SetSequence of the carrier of (TOP-REAL 2); ::_thesis: ( ( for i being Element of NAT holds C . i = (A . i) /\ (B . i) ) implies Lim_sup C c= (Lim_sup A) /\ (Lim_sup B) )
assume A1: for i being Element of NAT holds C . i = (A . i) /\ (B . i) ; ::_thesis: Lim_sup C c= (Lim_sup A) /\ (Lim_sup B)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_sup C or x in (Lim_sup A) /\ (Lim_sup B) )
assume x in Lim_sup C ; ::_thesis: x in (Lim_sup A) /\ (Lim_sup B)
then consider C1 being subsequence of C such that
A2: x in Lim_inf C1 by Def2;
for i being Element of NAT holds C . i c= B . i
proof
let i be Element of NAT ; ::_thesis: C . i c= B . i
C . i = (A . i) /\ (B . i) by A1;
hence C . i c= B . i by XBOOLE_1:17; ::_thesis: verum
end;
then consider E1 being subsequence of B such that
A3: for i being Element of NAT holds C1 . i c= E1 . i by Th32;
Lim_inf C1 c= Lim_inf E1 by A3, Th17;
then A4: x in Lim_sup B by A2, Def2;
for i being Element of NAT holds C . i c= A . i
proof
let i be Element of NAT ; ::_thesis: C . i c= A . i
C . i = (A . i) /\ (B . i) by A1;
hence C . i c= A . i by XBOOLE_1:17; ::_thesis: verum
end;
then consider D1 being subsequence of A such that
A5: for i being Element of NAT holds C1 . i c= D1 . i by Th32;
Lim_inf C1 c= Lim_inf D1 by A5, Th17;
then x in Lim_sup A by A2, Def2;
hence x in (Lim_sup A) /\ (Lim_sup B) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th37: :: KURATO_2:37
for A, B being SetSequence of the carrier of (TOP-REAL 2)
for C, C1 being SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) & C1 is subsequence of C holds
ex A1, B1 being SetSequence of the carrier of (TOP-REAL 2) st
( A1 is subsequence of A & B1 is subsequence of B & ( for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) )
proof
let A, B be SetSequence of the carrier of (TOP-REAL 2); ::_thesis: for C, C1 being SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) & C1 is subsequence of C holds
ex A1, B1 being SetSequence of the carrier of (TOP-REAL 2) st
( A1 is subsequence of A & B1 is subsequence of B & ( for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) )
let C, C1 be SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ( ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) & C1 is subsequence of C implies ex A1, B1 being SetSequence of the carrier of (TOP-REAL 2) st
( A1 is subsequence of A & B1 is subsequence of B & ( for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) ) )
assume that
A1: for i being Element of NAT holds C . i = [:(A . i),(B . i):] and
A2: C1 is subsequence of C ; ::_thesis: ex A1, B1 being SetSequence of the carrier of (TOP-REAL 2) st
( A1 is subsequence of A & B1 is subsequence of B & ( for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) )
consider NS being increasing sequence of NAT such that
A3: C1 = C * NS by A2, VALUED_0:def_17;
set B1 = B * NS;
set A1 = A * NS;
reconsider A1 = A * NS as SetSequence of (TOP-REAL 2) ;
reconsider B1 = B * NS as SetSequence of (TOP-REAL 2) ;
take A1 ; ::_thesis: ex B1 being SetSequence of the carrier of (TOP-REAL 2) st
( A1 is subsequence of A & B1 is subsequence of B & ( for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) )
take B1 ; ::_thesis: ( A1 is subsequence of A & B1 is subsequence of B & ( for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) )
for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):]
proof
let i be Element of NAT ; ::_thesis: C1 . i = [:(A1 . i),(B1 . i):]
A4: dom NS = NAT by FUNCT_2:def_1;
then A5: ( A1 . i = A . (NS . i) & B1 . i = B . (NS . i) ) by FUNCT_1:13;
C1 . i = C . (NS . i) by A3, A4, FUNCT_1:13
.= [:(A1 . i),(B1 . i):] by A1, A5 ;
hence C1 . i = [:(A1 . i),(B1 . i):] ; ::_thesis: verum
end;
hence ( A1 is subsequence of A & B1 is subsequence of B & ( for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) ) ; ::_thesis: verum
end;
theorem :: KURATO_2:38
for A, B being SetSequence of the carrier of (TOP-REAL 2)
for C being SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) holds
Lim_sup C c= [:(Lim_sup A),(Lim_sup B):]
proof
let A, B be SetSequence of the carrier of (TOP-REAL 2); ::_thesis: for C being SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) holds
Lim_sup C c= [:(Lim_sup A),(Lim_sup B):]
let C be SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ( ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) implies Lim_sup C c= [:(Lim_sup A),(Lim_sup B):] )
assume A1: for i being Element of NAT holds C . i = [:(A . i),(B . i):] ; ::_thesis: Lim_sup C c= [:(Lim_sup A),(Lim_sup B):]
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_sup C or x in [:(Lim_sup A),(Lim_sup B):] )
assume x in Lim_sup C ; ::_thesis: x in [:(Lim_sup A),(Lim_sup B):]
then consider C1 being subsequence of C such that
A2: x in Lim_inf C1 by Def2;
x in the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] by A2;
then x in [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] by BORSUK_1:def_2;
then consider x1, x2 being set such that
A3: x = [x1,x2] by RELAT_1:def_1;
consider A1, B1 being SetSequence of the carrier of (TOP-REAL 2) such that
A4: A1 is subsequence of A and
A5: B1 is subsequence of B and
A6: for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] by A1, Th37;
A7: x in [:(Lim_inf A1),(Lim_inf B1):] by A2, A6, Th27;
then x2 in Lim_inf B1 by A3, ZFMISC_1:87;
then A8: x2 in Lim_sup B by A5, Def2;
x1 in Lim_inf A1 by A3, A7, ZFMISC_1:87;
then x1 in Lim_sup A by A4, Def2;
hence x in [:(Lim_sup A),(Lim_sup B):] by A3, A8, ZFMISC_1:87; ::_thesis: verum
end;
theorem Th39: :: KURATO_2:39
for T being non empty TopSpace
for F being SetSequence of the carrier of T
for A being Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = Lim_sup F
proof
let T be non empty TopSpace; ::_thesis: for F being SetSequence of the carrier of T
for A being Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = Lim_sup F
let F be SetSequence of the carrier of T; ::_thesis: for A being Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = Lim_sup F
let A be Subset of T; ::_thesis: ( ( for i being Nat holds F . i = A ) implies Lim_inf F = Lim_sup F )
assume A1: for i being Nat holds F . i = A ; ::_thesis: Lim_inf F = Lim_sup F
thus Lim_inf F c= Lim_sup F by Th31; :: according to XBOOLE_0:def_10 ::_thesis: Lim_sup F c= Lim_inf F
thus Lim_sup F c= Lim_inf F ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_sup F or x in Lim_inf F )
assume x in Lim_sup F ; ::_thesis: x in Lim_inf F
then ex G being subsequence of F st x in Lim_inf G by Def2;
hence x in Lim_inf F by A1, Th12; ::_thesis: verum
end;
end;
theorem :: KURATO_2:40
for F being SetSequence of the carrier of (TOP-REAL 2)
for A being Subset of (TOP-REAL 2) st ( for i being Nat holds F . i = A ) holds
Lim_sup F = Cl A
proof
let F be SetSequence of the carrier of (TOP-REAL 2); ::_thesis: for A being Subset of (TOP-REAL 2) st ( for i being Nat holds F . i = A ) holds
Lim_sup F = Cl A
let A be Subset of (TOP-REAL 2); ::_thesis: ( ( for i being Nat holds F . i = A ) implies Lim_sup F = Cl A )
assume A1: for i being Nat holds F . i = A ; ::_thesis: Lim_sup F = Cl A
then Lim_inf F = Lim_sup F by Th39;
hence Lim_sup F = Cl A by A1, Th23; ::_thesis: verum
end;
theorem :: KURATO_2:41
for F, G being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds G . i = Cl (F . i) ) holds
Lim_sup G = Lim_sup F
proof
let F, G be SetSequence of the carrier of (TOP-REAL 2); ::_thesis: ( ( for i being Element of NAT holds G . i = Cl (F . i) ) implies Lim_sup G = Lim_sup F )
assume A1: for i being Element of NAT holds G . i = Cl (F . i) ; ::_thesis: Lim_sup G = Lim_sup F
thus Lim_sup G c= Lim_sup F :: according to XBOOLE_0:def_10 ::_thesis: Lim_sup F c= Lim_sup G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_sup G or x in Lim_sup F )
assume x in Lim_sup G ; ::_thesis: x in Lim_sup F
then consider H being subsequence of G such that
A2: x in Lim_inf H by Def2;
consider NS being increasing sequence of NAT such that
A3: H = G * NS by VALUED_0:def_17;
set P = F * NS;
reconsider P = F * NS as SetSequence of (TOP-REAL 2) ;
reconsider P = P as subsequence of F ;
for i being Element of NAT holds H . i = Cl (P . i)
proof
let i be Element of NAT ; ::_thesis: H . i = Cl (P . i)
A4: dom NS = NAT by FUNCT_2:def_1;
then H . i = G . (NS . i) by A3, FUNCT_1:13
.= Cl (F . (NS . i)) by A1
.= Cl (P . i) by A4, FUNCT_1:13 ;
hence H . i = Cl (P . i) ; ::_thesis: verum
end;
then Lim_inf H = Lim_inf P by Th20;
hence x in Lim_sup F by A2, Def2; ::_thesis: verum
end;
for i being Element of NAT holds F . i c= G . i
proof
let i be Element of NAT ; ::_thesis: F . i c= G . i
G . i = Cl (F . i) by A1;
hence F . i c= G . i by PRE_TOPC:18; ::_thesis: verum
end;
hence Lim_sup F c= Lim_sup G by Th34; ::_thesis: verum
end;