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


begin

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 V33( 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 ;
cluster non empty Relation-like non-empty NAT -defined bool T -valued Function-like V29( NAT ) V33( NAT , bool T) for Element of bool [:NAT,(bool T):];
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;

begin

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 Element of 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 Element of 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 Element of NAT holds f . n = meet (F ^\ n) ) ) & ex f being SetSequence of X st
( b2 = Union f & ( for n being Element of 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 Element of 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 Element of 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 Element of NAT holds f . n = Union (F ^\ n) ) ) & ex f being SetSequence of X st
( b2 = meet f & ( for n being Element of 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 Element of 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 Element of 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 set holds
( x in meet F iff for z being Element of 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 set holds
( x in lim_inf F iff ex n being Element of NAT st
for k being Element of 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 set holds
( x in lim_sup F iff for n being Element of NAT ex k being Element of 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 = (lim_sup (Complement F)) `
proof end;

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

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

theorem :: KURATO_0:12
for X being set
for A, B, C being SetSequence of X st ( for n being Element of NAT holds C . n = (A . n) \/ (B . n) ) holds
(lim_inf A) \/ (lim_inf B) 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 Element of NAT holds C . n = (A . n) /\ (B . n) ) holds
lim_sup C c= (lim_sup A) /\ (lim_sup B)
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 Element of NAT holds B . n = C \+\ (A . n) ) holds
C \+\ (lim_inf A) 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 Element of NAT holds B . n = C \+\ (A . n) ) holds
C \+\ (lim_sup A) c= lim_sup B
proof end;

begin

theorem Th18: :: KURATO_0:18
for f being Function st ( for i being Element of NAT holds f . (i + 1) c= f . i ) holds
for i, j being Element of 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 :Def3: :: KURATO_0:def 3
for i being Element of NAT holds S . (i + 1) c= S . i;
compatibility
( S is non-ascending iff for i being Element of NAT holds S . (i + 1) c= S . i )
proof end;
:: original: non-descending
redefine attr S is non-descending means :Def4: :: KURATO_0:def 4
for i being Element of NAT holds S . i c= S . (i + 1);
compatibility
( S is non-descending iff for i being Element of NAT holds S . i c= S . (i + 1) )
proof end;
end;

:: deftheorem Def3 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 Element of NAT holds S . (i + 1) c= S . i );

:: deftheorem Def4 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 Element of 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 set st F is V50() & ex k being Element of NAT st
for n being Element of 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 V50() 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 V51() holds
lim_sup F = Union F
proof end;

begin

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 V33( NAT , bool T) -> V50() V51() 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 V51() & b1 is V50() )
proof end;
end;

registration
let T be set ;
cluster non empty Relation-like NAT -defined bool T -valued Function-like constant V29( NAT ) V33( NAT , bool T) for Element of bool [:NAT,(bool T):];
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 Element of NAT st
for k being Element of NAT holds x in F . (n + k) )
proof end;