:: On the {K}uratowski Limit Operators
::
:: Copyright (c) 2003-2018 Association of Mizar Users

definition
let T be 1-sorted ;
mode SetSequence of T is SetSequence of the carrier of T;
end;

registration
let f be FinSequence of the carrier of ();
cluster L~ f -> closed ;
coherence
L~ f is closed
;
end;

theorem Th1: :: KURATO_2:1
for n being Nat
for x being Point of ()
for r being Real holds Ball (x,r) is open Subset of () by ;

theorem Th2: :: KURATO_2:2
for n being Nat
for p being Point of ()
for x, p9 being Point of ()
for r being Real st p = p9 & x in Ball (p,r) holds
|.(x - p9).| < r
proof end;

theorem Th3: :: KURATO_2:3
for n being Nat
for p being Point of ()
for x, p9 being Point of ()
for r being Real st p = p9 & |.(x - p9).| < r holds
x in Ball (p,r)
proof end;

theorem :: KURATO_2:4
for n being Nat
for r being Point of ()
for X being Subset of () 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 end;

registration
let M be non empty MetrSpace;
coherence 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 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 end;

registration
let n be Nat;
coherence
proof end;
end;

theorem :: KURATO_2:6
for n being Nat
for A being Subset of ()
for p being Point of ()
for p9 being Point of () st p = p9 holds
( p in Cl A iff for r being Real st r > 0 holds
Ball (p9,r) meets A )
proof end;

theorem :: KURATO_2:7
for n being Nat
for x, y being Point of ()
for x9 being Point of () st x9 = x & x <> y holds
ex r being Real st not y in Ball (x9,r)
proof end;

theorem Th8: :: KURATO_2:8
for n being Nat
for S being Subset of () holds
( not S is bounded iff for r being Real st r > 0 holds
ex x, y being Point of () st
( x in S & y in S & dist (x,y) > r ) )
proof end;

theorem Th9: :: KURATO_2:9
for n being Nat
for a, b being Real
for x, y being Point of () st Ball (x,a) meets Ball (y,b) holds
dist (x,y) < a + b
proof end;

theorem Th10: :: KURATO_2:10
for n being Nat
for a, b, c being Real
for x, y, z being Point of () st Ball (x,a) meets Ball (z,c) & Ball (z,c) meets Ball (y,b) holds
dist (x,y) < (a + b) + (2 * c)
proof 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 end;

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 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 Nat ex m being Element of NAT st
( m >= n & R . n = S . m )
proof end;

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 Nat st
for m being 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 Nat st
for m being Nat st m > k holds
S . m meets G )
proof 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 Nat st
for m being 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 Nat st
for m being Nat st m > k holds
S . m meets G ) ) holds
b1 = b2
proof 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 Nat st
for m being Nat st m > k holds
S . m meets G ) );

theorem Th14: :: KURATO_2:14
for n being Nat
for S being SetSequence of the carrier of ()
for p being Point of ()
for p9 being Point of () st p = p9 holds
( p in Lim_inf S iff for r being Real st r > 0 holds
ex k being Nat st
for m being Nat st m > k holds
S . m meets Ball (p9,r) )
proof 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
proof end;

registration
let T be non empty TopSpace;
let S be SetSequence of the carrier of T;
coherence
proof 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 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 Nat holds A . i c= B . i ) holds
Lim_inf A c= Lim_inf B
proof 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 Nat holds C . i = (A . i) \/ (B . i) ) holds
() \/ () c= Lim_inf C
proof 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 Nat holds C . i = (A . i) /\ (B . i) ) holds
Lim_inf C c= () /\ ()
proof 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 Nat holds G . i = Cl (F . i) ) holds
Lim_inf G = Lim_inf F
proof end;

theorem :: KURATO_2:21
for n being Nat
for S being SetSequence of the carrier of ()
for p being Point of () st ex s being Real_Sequence of n st
( s is convergent & ( for x being Nat holds s . x in S . x ) & p = lim s ) holds
p in Lim_inf S
proof 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 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 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 end;

theorem Th25: :: KURATO_2:25
for n being Nat
for S being SetSequence of the carrier of ()
for P being Subset of () st P is bounded & ( for i being Nat holds S . i c= P ) holds
Lim_inf S is bounded
proof end;

theorem :: KURATO_2:26
for S being SetSequence of the carrier of ()
for P being Subset of () st P is bounded & ( for i being Nat holds S . i c= P ) holds
Lim_inf S is compact by ;

theorem Th27: :: KURATO_2:27
for n being Nat
for A, B being SetSequence of the carrier of ()
for C being SetSequence of the carrier of [:(),():] st ( for i being Nat holds C . i = [:(A . i),(B . i):] ) holds
[:(),():] = Lim_inf C
proof end;

theorem :: KURATO_2:28
for S being SetSequence of () holds lim_inf S c= Lim_inf S
proof end;

theorem :: KURATO_2:29
for C being Simple_closed_curve
for i being Nat holds Fr ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i))
proof end;

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 object 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 object holds
( x in b1 iff ex A being subsequence of S st x in Lim_inf A )
proof end;
uniqueness
for b1, b2 being Subset of T st ( for x being object holds
( x in b1 iff ex A being subsequence of S st x in Lim_inf A ) ) & ( for x being object holds
( x in b2 iff ex A being subsequence of S st x in Lim_inf A ) ) holds
b1 = b2
proof 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 object holds
( x in b3 iff ex A being subsequence of S st x in Lim_inf A ) );

theorem :: KURATO_2:30
for N being Nat
for F being sequence of ()
for x being Point of ()
for x9 being Point of () st x = x9 holds
( x is_a_cluster_point_of F iff for r being Real
for n being Nat st r > 0 holds
ex m being Nat st
( n <= m & F . m in Ball (x9,r) ) )
proof 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 end;

theorem Th32: :: KURATO_2:32
for A, B, C being SetSequence of the carrier of () st ( for i being Nat holds A . i c= B . i ) & C is subsequence of A holds
ex D being subsequence of B st
for i being Nat holds C . i c= D . i
proof end;

theorem :: KURATO_2:33
for A, B, C being SetSequence of the carrier of () st ( for i being Nat holds A . i c= B . i ) & C is subsequence of B holds
ex D being subsequence of A st
for i being Nat holds D . i c= C . i
proof end;

theorem Th34: :: KURATO_2:34
for A, B being SetSequence of the carrier of () st ( for i being Nat holds A . i c= B . i ) holds
Lim_sup A c= Lim_sup B
proof end;

theorem :: KURATO_2:35
for A, B, C being SetSequence of the carrier of () st ( for i being Nat holds C . i = (A . i) \/ (B . i) ) holds
() \/ () c= Lim_sup C
proof end;

theorem :: KURATO_2:36
for A, B, C being SetSequence of the carrier of () st ( for i being Nat holds C . i = (A . i) /\ (B . i) ) holds
Lim_sup C c= () /\ ()
proof end;

theorem Th37: :: KURATO_2:37
for A, B being SetSequence of the carrier of ()
for C, C1 being SetSequence of the carrier of [:(),():] st ( for i being Nat holds C . i = [:(A . i),(B . i):] ) & C1 is subsequence of C holds
ex A1, B1 being SetSequence of the carrier of () st
( A1 is subsequence of A & B1 is subsequence of B & ( for i being Nat holds C1 . i = [:(A1 . i),(B1 . i):] ) )
proof end;

theorem :: KURATO_2:38
for A, B being SetSequence of the carrier of ()
for C being SetSequence of the carrier of [:(),():] st ( for i being Nat holds C . i = [:(A . i),(B . i):] ) holds
Lim_sup C c= [:(),():]
proof end;

:: 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
proof end;

theorem :: KURATO_2:40
for F being SetSequence of the carrier of ()
for A being Subset of () st ( for i being Nat holds F . i = A ) holds
Lim_sup F = Cl A
proof end;

theorem :: KURATO_2:41
for F, G being SetSequence of the carrier of () st ( for i being Nat holds G . i = Cl (F . i) ) holds
Lim_sup G = Lim_sup F
proof end;