:: Limit of Sequence of Subsets
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received March 15, 2005
:: Copyright (c) 2005-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, NUMBERS, PROB_1, XXREAL_0, ARYTM_3, FUNCT_1, XBOOLE_0,
TARSKI, NAT_1, RELAT_1, CARD_1, SETFAM_1, EQREL_1, CARD_3, ZFMISC_1,
SEQM_3, ORDINAL2, SEQ_2, SETLIM_1;
notations ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1,
TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELSET_1, SETFAM_1, PROB_1,
FUNCT_2, KURATO_0;
constructors SETFAM_1, NAT_1, KURATO_0, XREAL_0, RELSET_1, FINSUB_1, PROB_2;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, FUNCT_2, RELAT_1, PROB_1,
RELSET_1, NAT_1;
requirements NUMERALS, BOOLE, SUBSET;
begin
reserve n,m,k,k1,k2,i,j for Nat;
reserve x,y,z for object,X,Y,Z for set;
reserve A for Subset of X;
reserve B,A1,A2,A3 for SetSequence of X;
reserve Si for SigmaField of X;
reserve S,S1,S2,S3 for SetSequence of Si;
theorem :: SETLIM_1:1
for f be sequence of Y
holds f.(n + m) in {f.k: n <= k};
theorem :: SETLIM_1:2
for f being sequence of Y holds {f.k1: n <= k1} = {f.k2 : n+1
<=k2} \/ {f.n};
theorem :: SETLIM_1:3
for f be sequence of Y holds (for k1 holds x in f.(n+k1)) iff
for Z st Z in {f.k2 : n <= k2} holds x in Z;
theorem :: SETLIM_1:4
for Y being non empty set for f being sequence of Y holds x
in rng f iff ex n st x = f.n;
theorem :: SETLIM_1:5
for Y be non empty set for f being sequence of Y holds rng f
= {f.k : 0 <= k};
theorem :: SETLIM_1:6
for Y being non empty set for f being sequence of Y holds rng
(f ^\ k) = {f.n: k <= n};
theorem :: SETLIM_1:7
x in meet rng B iff for n being Nat holds x in B.n;
theorem :: SETLIM_1:8
Intersection B = meet rng B;
theorem :: SETLIM_1:9
Intersection B c= Union B;
theorem :: SETLIM_1:10
(for n holds B.n = A) implies Union B = A;
theorem :: SETLIM_1:11
(for n holds B.n = A) implies Intersection B = A;
theorem :: SETLIM_1:12
B is constant implies Union B = Intersection B;
theorem :: SETLIM_1:13
B is constant & the_value_of B = A implies for n holds union {B.
k: n <= k} = A;
theorem :: SETLIM_1:14
B is constant & the_value_of B = A implies for n holds meet {B.k
: n <= k} = A;
theorem :: SETLIM_1:15
for X, B for f being Function st dom f = NAT & for n holds f.n =
meet {B.k: n <= k} holds f is SetSequence of X;
theorem :: SETLIM_1:16
for X being set, B being SetSequence of X for f being Function
st dom f = NAT & for n holds f.n = union {B.k: n <= k} holds
f is sequence of bool X;
definition
let X,B;
attr B is monotone means
:: SETLIM_1:def 1
B is non-descending or B is non-ascending;
end;
definition
let B be Function;
func inferior_setsequence B -> Function means
:: SETLIM_1:def 2
dom it = NAT & for n holds it.n = meet {B.k : n <= k};
end;
definition
let X be set, B be SetSequence of X;
redefine func inferior_setsequence B -> SetSequence of X;
end;
definition
let B be Function;
func superior_setsequence B -> Function means
:: SETLIM_1:def 3
dom it = NAT & for n holds it.n = union {B.k : n <= k};
end;
definition
let X be set, B be SetSequence of X;
redefine func superior_setsequence B -> SetSequence of X;
end;
theorem :: SETLIM_1:17
(inferior_setsequence B).0 = Intersection B;
theorem :: SETLIM_1:18
(superior_setsequence B).0 = Union B;
theorem :: SETLIM_1:19
for n being Nat holds
x in (inferior_setsequence B).n iff
for k being Nat holds x in B.(n+k);
theorem :: SETLIM_1:20
for n being Nat holds
x in (superior_setsequence B).n iff
ex k being Nat st x in B.(n + k);
theorem :: SETLIM_1:21
for n being Nat holds
(inferior_setsequence B).n = (inferior_setsequence B).(n+1) /\ B .n;
theorem :: SETLIM_1:22
for n being Nat holds
(superior_setsequence B).n = (superior_setsequence B).(n+1) \/ B .n;
theorem :: SETLIM_1:23
inferior_setsequence B is non-descending;
theorem :: SETLIM_1:24
superior_setsequence B is non-ascending;
theorem :: SETLIM_1:25
inferior_setsequence B is monotone & superior_setsequence B is monotone;
registration
let X be set, A be SetSequence of X;
cluster inferior_setsequence A -> non-descending for SetSequence of X;
end;
registration
let X be set, A be SetSequence of X;
cluster superior_setsequence A -> non-ascending for SetSequence of X;
end;
theorem :: SETLIM_1:26
Intersection B c= (inferior_setsequence B).n;
theorem :: SETLIM_1:27
(superior_setsequence B).n c= Union B;
theorem :: SETLIM_1:28
for B,n holds {B.k: n <= k} is Subset-Family of X;
theorem :: SETLIM_1:29
Union B = (Intersection Complement B)`;
theorem :: SETLIM_1:30
for n being Element of NAT holds
(inferior_setsequence B).n = ((superior_setsequence Complement B ).n)`;
theorem :: SETLIM_1:31
for n being Element of NAT holds
(superior_setsequence B).n = ((inferior_setsequence Complement B).n)`;
theorem :: SETLIM_1:32
Complement (inferior_setsequence B) = (superior_setsequence Complement B);
theorem :: SETLIM_1:33
Complement superior_setsequence B = inferior_setsequence Complement B;
theorem :: SETLIM_1:34
(for n being Nat holds A3.n = A1.n \/ A2.n) implies
for n being Nat holds (
inferior_setsequence A1).n \/ (inferior_setsequence(A2)).n c= (
inferior_setsequence(A3)).n;
theorem :: SETLIM_1:35
(for n being Nat holds A3.n = A1.n /\ A2.n) implies
for n being Nat holds (
inferior_setsequence A3).n = (inferior_setsequence A1).n /\ (
inferior_setsequence A2).n;
theorem :: SETLIM_1:36
(for n holds A3.n = A1.n \/ A2.n) implies for n holds (
superior_setsequence(A3)).n = (superior_setsequence(A1)).n \/ (
superior_setsequence(A2)).n;
theorem :: SETLIM_1:37
(for n holds A3.n = A1.n /\ A2.n) implies for n holds (
superior_setsequence A3).n c= (superior_setsequence A1).n /\ (
superior_setsequence A2).n;
theorem :: SETLIM_1:38
B is constant & the_value_of B = A implies for n holds (
inferior_setsequence B).n = A;
theorem :: SETLIM_1:39
B is constant & the_value_of B = A implies for n holds (
superior_setsequence B).n = A;
theorem :: SETLIM_1:40
for n being Nat holds
B is non-descending implies B.n c= (superior_setsequence(B)).(n+ 1);
theorem :: SETLIM_1:41
for n being Nat holds
B is non-descending implies (superior_setsequence B).n = (
superior_setsequence B).(n+1);
theorem :: SETLIM_1:42
for n being Nat holds
B is non-descending implies (superior_setsequence B).n = Union B;
theorem :: SETLIM_1:43
B is non-descending implies Intersection superior_setsequence B = Union B;
theorem :: SETLIM_1:44
B is non-descending implies B.n c= (inferior_setsequence B).(n+1 );
theorem :: SETLIM_1:45
B is non-descending implies (inferior_setsequence B).n = B.n;
theorem :: SETLIM_1:46
B is non-descending implies inferior_setsequence B = B;
theorem :: SETLIM_1:47
B is non-ascending implies (superior_setsequence B).(n+1) c= B.n;
theorem :: SETLIM_1:48
B is non-ascending implies (superior_setsequence(B)).n = B.n;
theorem :: SETLIM_1:49
B is non-ascending implies superior_setsequence(B) = B;
theorem :: SETLIM_1:50
for n being Nat holds
B is non-ascending implies (inferior_setsequence(B)).(n+1) c= B. n;
theorem :: SETLIM_1:51
for n being Nat holds
B is non-ascending implies (inferior_setsequence(B)).n = (
inferior_setsequence(B)).(n+1);
theorem :: SETLIM_1:52
for n being Nat holds
B is non-ascending implies (inferior_setsequence(B)).n = Intersection B;
theorem :: SETLIM_1:53
B is non-ascending implies Union inferior_setsequence(B) = Intersection B;
definition
let X be set, B be SetSequence of X;
redefine func lim_inf B equals
:: SETLIM_1:def 4
Union inferior_setsequence B;
end;
definition
let X be set, B be SetSequence of X;
redefine func lim_sup B equals
:: SETLIM_1:def 5
Intersection superior_setsequence B;
end;
notation
let X be set, B be SetSequence of X;
synonym lim B for lim_sup B;
end;
theorem :: SETLIM_1:54
Intersection B c= lim_inf B;
theorem :: SETLIM_1:55
lim_inf B = lim inferior_setsequence(B);
theorem :: SETLIM_1:56
lim_sup B = lim superior_setsequence(B);
theorem :: SETLIM_1:57
lim_sup B = (lim_inf Complement B)`;
theorem :: SETLIM_1:58
B is constant & the_value_of B = A implies B is convergent & lim
B = A & lim_inf B = A & lim_sup B = A;
theorem :: SETLIM_1:59
B is non-descending implies lim_sup B = Union B;
theorem :: SETLIM_1:60
B is non-descending implies lim_inf B = Union B;
theorem :: SETLIM_1:61
B is non-ascending implies lim_sup B = Intersection B;
theorem :: SETLIM_1:62
B is non-ascending implies lim_inf B = Intersection B;
theorem :: SETLIM_1:63
B is non-descending implies B is convergent & lim B = Union B;
theorem :: SETLIM_1:64
B is non-ascending implies B is convergent & lim B = Intersection B;
theorem :: SETLIM_1:65
B is monotone implies B is convergent;
definition
let X be set, Si be SigmaField of X, S be SetSequence of Si;
redefine func inferior_setsequence S -> SetSequence of Si;
end;
definition
let X be set, Si be SigmaField of X, S be SetSequence of Si;
redefine func superior_setsequence S -> SetSequence of Si;
end;
theorem :: SETLIM_1:66
x in lim_sup S iff for n being Nat
ex k being Nat st x in S.(n+k);
theorem :: SETLIM_1:67
x in lim_inf S iff ex n being Nat st for k being Nat holds x in S.(n+k);
theorem :: SETLIM_1:68
Intersection S c= lim_inf S;
theorem :: SETLIM_1:69
lim_sup S c= Union S;
theorem :: SETLIM_1:70
lim_inf S c= lim_sup S;
theorem :: SETLIM_1:71
lim_inf S = (lim_sup Complement S)`;
theorem :: SETLIM_1:72
lim_sup S = (lim_inf Complement S)`;
theorem :: SETLIM_1:73
(for n being Nat holds S3.n = S1.n \/ S2.n)
implies lim_inf S1 \/ lim_inf S2 c=
lim_inf S3;
theorem :: SETLIM_1:74
(for n being Nat holds S3.n = S1.n /\ S2.n)
implies lim_inf S3 = lim_inf S1 /\
lim_inf S2;
theorem :: SETLIM_1:75
(for n being Nat holds S3.n = S1.n \/ S2.n)
implies lim_sup S3 = lim_sup S1 \/
lim_sup S2;
theorem :: SETLIM_1:76
(for n being Nat holds S3.n = S1.n /\ S2.n)
implies lim_sup S3 c= lim_sup S1 /\ lim_sup S2;
theorem :: SETLIM_1:77
S is constant & the_value_of S = A implies S is convergent & lim S = A
& lim_inf S = A & lim_sup S = A;
theorem :: SETLIM_1:78
S is non-descending implies lim_sup S = Union S;
theorem :: SETLIM_1:79
S is non-descending implies lim_inf S = Union S;
theorem :: SETLIM_1:80
S is non-descending implies S is convergent & lim S = Union S;
theorem :: SETLIM_1:81
S is non-ascending implies lim_sup S = Intersection S;
theorem :: SETLIM_1:82
S is non-ascending implies lim_inf S = Intersection S;
theorem :: SETLIM_1:83
S is non-ascending implies S is convergent & lim S = Intersection S;
theorem :: SETLIM_1:84
S is monotone implies S is convergent;