:: by Adam Grabowski

::

:: Received August 12, 2003

:: Copyright (c) 2003-2021 Association of Mizar Users

registration
end;

registration

let T be non empty set ;

ex b_{1} being SetSequence of T st b_{1} is non-empty

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

proof 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

redefine func meet F -> Subset of X;

coherence

meet F is Subset of X

end;
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: meetredefine func meet F -> Subset of X;

coherence

meet F is Subset of X

proof end;

definition

let X be set ;

let F be SetSequence of X;

ex b_{1} being Subset of X ex f being SetSequence of X st

( b_{1} = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) )

for b_{1}, b_{2} being Subset of X st ex f being SetSequence of X st

( b_{1} = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) ) & ex f being SetSequence of X st

( b_{2} = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) ) holds

b_{1} = b_{2}

ex b_{1} being Subset of X ex f being SetSequence of X st

( b_{1} = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) )

for b_{1}, b_{2} being Subset of X st ex f being SetSequence of X st

( b_{1} = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) ) & ex f being SetSequence of X st

( b_{2} = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) ) holds

b_{1} = b_{2}

end;
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 f being SetSequence of X st

( it = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) );

ex b

( b

proof end;

uniqueness for b

( b

( 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 f being SetSequence of X st

( it = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def1 defines lim_inf KURATO_0:def 1 :

for X being set

for F being SetSequence of X

for b_{3} being Subset of X holds

( b_{3} = lim_inf F iff ex f being SetSequence of X st

( b_{3} = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) ) );

for X being set

for F being SetSequence of X

for b

( b

( b

:: deftheorem Def2 defines lim_sup KURATO_0:def 2 :

for X being set

for F being SetSequence of X

for b_{3} being Subset of X holds

( b_{3} = lim_sup F iff ex f being SetSequence of X st

( b_{3} = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) ) );

for X being set

for F being SetSequence of X

for b

( b

( b

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 )

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) )

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) )

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: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)

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)

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

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)

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

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

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

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

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

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;

( S is non-ascending iff for i being Nat holds S . (i + 1) c= S . i )

( S is non-descending iff for i being Nat holds S . i c= S . (i + 1) )

end;
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 redefine attr S is non-ascending means :: KURATO_0:def 3

for i being Nat holds S . (i + 1) c= S . i;

( 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 redefine attr S is non-descending means :: KURATO_0:def 4

for i being Nat holds S . i c= S . (i + 1);

( S is non-descending iff for i being Nat holds S . i c= S . (i + 1) )

proof 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 );

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) );

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

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;

:: 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 );

for T being set

for S being SetSequence of T holds

( S is convergent iff lim_sup S = lim_inf S );

registration

let T be set ;

for b_{1} being SetSequence of T st b_{1} is constant holds

( b_{1} is convergent & b_{1} is V53() & b_{1} is V52() )

end;
cluster Function-like constant V35( NAT , bool T) -> V52() V53() convergent for Element of bool [:NAT,(bool T):];

coherence for b

( b

proof end;

registration

let T be set ;

ex b_{1} being SetSequence of T st

( b_{1} is constant & not b_{1} is empty )

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

( b

proof 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) )

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;