:: On the {K}uratowski Limit Operators
:: by Adam Grabowski
::
:: Received August 12, 2003
:: Copyright (c) 2003-2021 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 (TOP-REAL 2);
cluster L~ f -> closed ;
coherence
L~ f is closed ;
end;

theorem Th1: :: KURATO_2:1
for n being Nat
for x being Point of (Euclid n)
for r being Real holds Ball (x,r) is open Subset of (TOP-REAL n) by TOPREAL3:8, GOBOARD6:3;

theorem Th2: :: KURATO_2:2
for n being Nat
for p being Point of (Euclid n)
for x, p9 being Point of (TOP-REAL n)
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 (Euclid n)
for x, p9 being Point of (TOP-REAL n)
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 (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 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 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;
cluster TOP-REAL n -> first-countable ;
coherence
TOP-REAL n is first-countable
proof end;
end;

theorem :: KURATO_2:6
for n being 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 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 (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 end;

theorem Th8: :: KURATO_2:8
for n being 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 end;

theorem Th9: :: KURATO_2:9
for n being Nat
for a, b being Real
for x, y being Point of (Euclid n) 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 (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 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 (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 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) = Lim_inf S
proof 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 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
(Lim_inf A) \/ (Lim_inf B) 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= (Lim_inf A) /\ (Lim_inf B)
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 (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 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 (TOP-REAL n)
for P being Subset of (TOP-REAL n) 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 (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st P is bounded & ( for i being Nat holds S . i c= P ) holds
Lim_inf S is compact by Th25, TOPREAL6:79;

theorem Th27: :: KURATO_2:27
for n being 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 Nat holds C . i = [:(A . i),(B . i):] ) holds
[:(Lim_inf A),(Lim_inf B):] = Lim_inf C
proof end;

theorem :: KURATO_2:28
for S being SetSequence of (TOP-REAL 2) 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 (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
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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) st ( for i being Nat holds C . i = (A . i) \/ (B . i) ) holds
(Lim_sup A) \/ (Lim_sup B) c= Lim_sup C
proof end;

theorem :: KURATO_2:36
for A, B, C being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Nat holds C . i = (A . i) /\ (B . i) ) holds
Lim_sup C c= (Lim_sup A) /\ (Lim_sup B)
proof 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 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 Nat holds C1 . i = [:(A1 . i),(B1 . i):] ) )
proof 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 Nat holds C . i = [:(A . i),(B . i):] ) holds
Lim_sup C c= [:(Lim_sup A),(Lim_sup B):]
proof end;

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

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