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

theorem :: KURATO_0:1
for F being Function
for i being set st i in dom F holds
meet F c= F . i
proof end;

theorem :: KURATO_0:2
for A, B, C, D being set st A meets B & C meets D holds
[:A,C:] meets [:B,D:]
proof end;

registration
let X be set ;
cluster Function-like V35( NAT , bool X) -> non empty for Element of bool [:NAT,(bool X):];
coherence
for b1 being SetSequence of X holds not b1 is empty
;
end;

registration
let T be non empty set ;
existence
ex b1 being SetSequence of T st b1 is non-empty
proof end;
end;

definition
let X be set ;
let F be SetSequence of X;
:: original: Union
redefine func Union F -> Subset of X;
coherence
Union F is Subset of X
proof end;
:: original: meet
redefine func meet F -> Subset of X;
coherence
meet F is Subset of X
proof end;
end;

definition
let X be set ;
let F be SetSequence of X;
func lim_inf F -> Subset of X means :Def1: :: KURATO_0:def 1
ex f being SetSequence of X st
( it = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) );
existence
ex b1 being Subset of X ex f being SetSequence of X st
( b1 = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) )
proof end;
uniqueness
for b1, b2 being Subset of X st ex f being SetSequence of X st
( b1 = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) ) & ex f being SetSequence of X st
( b2 = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) ) holds
b1 = b2
proof end;
func lim_sup F -> Subset of X means :Def2: :: KURATO_0:def 2
ex f being SetSequence of X st
( it = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) );
existence
ex b1 being Subset of X ex f being SetSequence of X st
( b1 = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) )
proof end;
uniqueness
for b1, b2 being Subset of X st ex f being SetSequence of X st
( b1 = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) ) & ex f being SetSequence of X st
( b2 = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines lim_inf KURATO_0:def 1 :
for X being set
for F being SetSequence of X
for b3 being Subset of X holds
( b3 = lim_inf F iff ex f being SetSequence of X st
( b3 = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) ) );

:: deftheorem Def2 defines lim_sup KURATO_0:def 2 :
for X being set
for F being SetSequence of X
for b3 being Subset of X holds
( b3 = lim_sup F iff ex f being SetSequence of X st
( b3 = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) ) );

theorem Th3: :: KURATO_0:3
for X being set
for F being SetSequence of X
for x being object holds
( x in meet F iff for z being Nat holds x in F . z )
proof end;

theorem Th4: :: KURATO_0:4
for X being set
for F being SetSequence of X
for x being object holds
( x in lim_inf F iff ex n being Nat st
for k being Nat holds x in F . (n + k) )
proof end;

theorem Th5: :: KURATO_0:5
for X being set
for F being SetSequence of X
for x being object holds
( x in lim_sup F iff for n being Nat ex k being Nat st x in F . (n + k) )
proof end;

theorem :: KURATO_0:6
for X being set
for F being SetSequence of X holds lim_inf F c= lim_sup F
proof end;

theorem Th7: :: KURATO_0:7
for X being set
for F being SetSequence of X holds meet F c= lim_inf F
proof end;

theorem Th8: :: KURATO_0:8
for X being set
for F being SetSequence of X holds lim_sup F c= Union F
proof end;

theorem :: KURATO_0:9
for X being set
for F being SetSequence of X holds lim_inf F = () `
proof end;

theorem :: KURATO_0:10
for X being set
for A, B, C being SetSequence of X st ( for n being Nat holds C . n = (A . n) /\ (B . n) ) holds
lim_inf C = () /\ ()
proof end;

theorem :: KURATO_0:11
for X being set
for A, B, C being SetSequence of X st ( for n being Nat holds C . n = (A . n) \/ (B . n) ) holds
lim_sup C = () \/ ()
proof end;

theorem :: KURATO_0:12
for X being set
for A, B, C being SetSequence of X st ( for n being Nat holds C . n = (A . n) \/ (B . n) ) holds
() \/ () c= lim_inf C
proof end;

theorem :: KURATO_0:13
for X being set
for A, B, C being SetSequence of X st ( for n being Nat holds C . n = (A . n) /\ (B . n) ) holds
lim_sup C c= () /\ ()
proof end;

theorem Th14: :: KURATO_0:14
for X being set
for A being SetSequence of X
for B being Subset of X st ( for n being Nat holds A . n = B ) holds
lim_sup A = B
proof end;

theorem Th15: :: KURATO_0:15
for X being set
for A being SetSequence of X
for B being Subset of X st ( for n being Nat holds A . n = B ) holds
lim_inf A = B
proof end;

theorem :: KURATO_0:16
for X being set
for A, B being SetSequence of X
for C being Subset of X st ( for n being Nat holds B . n = C \+\ (A . n) ) holds
C \+\ () c= lim_sup B
proof end;

theorem :: KURATO_0:17
for X being set
for A, B being SetSequence of X
for C being Subset of X st ( for n being Nat holds B . n = C \+\ (A . n) ) holds
C \+\ () c= lim_sup B
proof end;

theorem Th18: :: KURATO_0:18
for f being Function st ( for i being Nat holds f . (i + 1) c= f . i ) holds
for i, j being Nat st i <= j holds
f . j c= f . i
proof end;

definition
let T be set ;
let S be SetSequence of T;
:: original: non-ascending
redefine attr S is non-ascending means :: KURATO_0:def 3
for i being Nat holds S . (i + 1) c= S . i;
compatibility
( S is non-ascending iff for i being Nat holds S . (i + 1) c= S . i )
proof end;
:: original: non-descending
redefine attr S is non-descending means :: KURATO_0:def 4
for i being Nat holds S . i c= S . (i + 1);
compatibility
( S is non-descending iff for i being Nat holds S . i c= S . (i + 1) )
proof end;
end;

:: deftheorem defines non-ascending KURATO_0:def 3 :
for T being set
for S being SetSequence of T holds
( S is non-ascending iff for i being Nat holds S . (i + 1) c= S . i );

:: deftheorem defines non-descending KURATO_0:def 4 :
for T being set
for S being SetSequence of T holds
( S is non-descending iff for i being Nat holds S . i c= S . (i + 1) );

theorem Th19: :: KURATO_0:19
for T being set
for F being SetSequence of T
for x being object st F is V52() & ex k being Nat st
for n being Nat st n > k holds
x in F . n holds
x in meet F
proof end;

theorem :: KURATO_0:20
for T being set
for F being SetSequence of T st F is V52() holds
lim_inf F = meet F
proof end;

theorem :: KURATO_0:21
for T being set
for F being SetSequence of T st F is V53() holds
lim_sup F = Union F
proof end;

definition
let T be set ;
let S be SetSequence of T;
attr S is convergent means :Def5: :: KURATO_0:def 5
lim_sup S = lim_inf S;
end;

:: deftheorem Def5 defines convergent KURATO_0:def 5 :
for T being set
for S being SetSequence of T holds
( S is convergent iff lim_sup S = lim_inf S );

theorem :: KURATO_0:22
for T being set
for S being SetSequence of T st S is constant holds
the_value_of S is Subset of T
proof end;

registration
let T be set ;
cluster Function-like constant V35( NAT , bool T) -> V52() V53() convergent for Element of bool [:NAT,(bool T):];
coherence
for b1 being SetSequence of T st b1 is constant holds
( b1 is convergent & b1 is V53() & b1 is V52() )
proof end;
end;

registration
let T be set ;
existence
ex b1 being SetSequence of T st
( b1 is constant & not b1 is empty )
proof end;
end;

notation
let T be set ;
let S be convergent SetSequence of T;
synonym Lim_K S for lim_sup S;
end;

theorem :: KURATO_0:23
for X being set
for F being convergent SetSequence of X
for x being set holds
( x in Lim_K F iff ex n being Nat st
for k being Nat holds x in F . (n + k) )
proof end;