:: On the {K}uratowski Limit Operators I
:: by Adam Grabowski
::
:: Received August 12, 2003
:: 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 b₁ being SetSequence of X holds not b₁ is empty ;

end;

registration

let T be non empty set ;

cluster non empty Relation-like non-empty NAT -defined bool T -valued Function-like V31( NAT ) V35( NAT , bool T) for Element of bool [:NAT,(bool T):];

existence
ex b₁ being SetSequence of T st b₁ 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 b₁ being Subset of X ex f being SetSequence of X st
( b₁ = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) )

proof end;

uniqueness
for b₁, b₂ being Subset of X st ex f being SetSequence of X st
( b₁ = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) ) & ex f being SetSequence of X st
( b₂ = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) ) holds
b₁ = b₂

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 b₁ being Subset of X ex f being SetSequence of X st
( b₁ = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) )

proof end;

uniqueness
for b₁, b₂ being Subset of X st ex f being SetSequence of X st
( b₁ = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) ) & ex f being SetSequence of X st
( b₂ = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines lim_inf KURATO_0:def 1 :
for X being set
for F being SetSequence of X
for b₃ being Subset of X holds
( b₃ = lim_inf F iff ex f being SetSequence of X st
( b₃ = 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 b₃ being Subset of X holds
( b₃ = lim_sup F iff ex f being SetSequence of X st
( b₃ = 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 = (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 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 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 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 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 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 Nat holds B . n = C \+\ (A . n) ) holds
C \+\ (lim_sup A) 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 b₁ being SetSequence of T st b₁ is constant holds
( b₁ is convergent & b₁ is V53() & b₁ is V52() )

proof end;

end;

registration

let T be set ;

cluster non empty Relation-like NAT -defined bool T -valued Function-like constant V31( NAT ) V35( NAT , bool T) for Element of bool [:NAT,(bool T):];

existence
ex b₁ being SetSequence of T st
( b₁ is constant & not b₁ 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;