:: On the {K}uratowski Limit Operators
:: by Adam Grabowski
::
:: Received August 12, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


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)
proofend;

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
proofend;

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 &amp; |.(x - p9).| < r holds
x in Ball (p,r)
proofend;

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 &amp; seq is convergent &amp; lim seq = r )
proofend;

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 )
proofend;

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 )
proofend;

registration
let n be Element of NAT ;
cluster TOP-REAL n ->  first-countable ;
coherence
 TOP-REAL n is first-countable
proofend;
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 )
proofend;

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 &amp; x <> y holds
ex r being Real st not y in Ball (x9,r)
proofend;

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 &amp; y in S &amp; dist (x,y) > r ) )
proofend;

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
proofend;

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) &amp; Ball (z,c) meets Ball (y,b) holds
dist (x,y) < (a + b) + (2 * c)
proofend;

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] )
proofend;

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 &amp; ( for i being Nat holds F . i = A ) holds
G = F
proofend;

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 &amp; R . n = S . m )
proofend;

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 )
proofend;
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 ) ) &amp; ( 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
proofend;
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) )
proofend;

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
proofend;

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
proofend;
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
proofend;

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
proofend;

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
proofend;

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)
proofend;

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
proofend;

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 &amp; ( for x being Element of NAT holds s . x in S . x ) &amp; p = lim s ) holds
p in Lim_inf S
proofend;

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
proofend;

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
proofend;

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
proofend;

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 &amp; ( for i being Element of NAT holds S . i c= P ) holds
Lim_inf S is bounded
proofend;

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 &amp; ( 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
proofend;

theorem :: KURATO_2:28
for S being SetSequence of (TOP-REAL 2) holds lim_inf S c= Lim_inf S
proofend;

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))
proofend;

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 )
proofend;
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 ) ) &amp; ( for x being set holds
( x in b2 iff ex A being subsequence of S st x in Lim_inf A ) ) holds
b1 = b2
proofend;
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 &amp; F . m in Ball (x9,r) ) )
proofend;

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
proofend;

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 ) &amp; 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
proofend;

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 ) &amp; 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
proofend;

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
proofend;

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
proofend;

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)
proofend;

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):] ) &amp; C1 is subsequence of C holds
ex A1, B1 being SetSequence of the carrier of (TOP-REAL 2) st
( A1 is subsequence of A &amp; B1 is subsequence of B &amp; ( for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) )
proofend;

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):]
proofend;

:: [WP: ] Kuratowski_convergence
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
proofend;

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
proofend;

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
proofend;