:: Limit of Sequence of Subsets
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received March 15, 2005
:: Copyright (c) 2005-2026 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;
definitions TARSKI;
equalities SUBSET_1;
expansions TARSKI;
theorems FUNCT_1, FUNCT_2, PROB_1, NAT_1, TARSKI, XBOOLE_0, XBOOLE_1,
XCMPLX_1, SETFAM_1, ZFMISC_1, CARD_3, KURATO_0, PROB_2, XREAL_1,
ORDINAL1, VALUED_0, RELAT_1;
schemes NAT_1, FUNCT_1;
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;
Lm1:
for i,j being Nat holds i <= j implies i = j or i + 1 <= j
proof let i,j be Nat;
assume i<=j;
then i + 1 <= j + 1 by XREAL_1:6;
hence thesis by NAT_1:8,XCMPLX_1:2;
end;
theorem Th1:
for f be sequence of Y
holds f.(n + m) in {f.k: n <= k}
proof
n <= n + m by NAT_1:11;
hence thesis;
end;
theorem Th2:
for f being sequence of Y holds {f.k1: n <= k1} = {f.k2 : n+1
<=k2} \/ {f.n}
proof
let f be sequence of Y;
set Z1 = {f.k1:n <= k1};
set Z2 = {f.k2:(n+1) <= k2};
A1: Z2 \/ {f.n} c= Z1
proof
let x be object;
assume
A2: x in Z2 \/ {f.n};
now
per cases by A2,XBOOLE_0:def 3;
case
x in Z2;
then consider z such that
A3: x = z and
A4: z in Z2;
consider k11 being Nat such that
A5: z=f.k11 and
A6: n+1 <= k11 by A4;
n <= k11 by A6,NAT_1:13;
hence thesis by A3,A5;
end;
case
x in {f.n};
then x = f.n by TARSKI:def 1;
hence thesis;
end;
end;
hence thesis;
end;
{f.k1: n <= k1} c= {f.k2 : n+1 <= k2} \/ {f.n}
proof
let x be object;
assume x in Z1;
then consider z such that
A7: x=z and
A8: z in Z1;
consider k such that
A9: z = f.k & n <= k by A8;
z = f.k & n+1 <= k or z = f.k & n = k by A9,Lm1;
then z in Z2 or z in {f.n} by TARSKI:def 1;
hence thesis by A7,XBOOLE_0:def 3;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th3:
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
proof
let f be sequence of Y;
set Z = {f.k2 : n <= k2};
now
assume
A1: for k1 holds x in f.(n+k1);
now
let Z1 be set;
assume Z1 in Z;
then consider k1 being Nat such that
A2: Z1=f.k1 and
A3: n <= k1;
ex m be Nat st k1 = n + m by A3,NAT_1:10;
then consider k2 being Nat such that
A4: Z1=f.(n + k2) by A2;
thus x in Z1 by A1,A4;
end;
hence for Z1 being set st Z1 in {f.k2 : n <= k2} holds x in Z1;
end;
hence thesis by Th1;
end;
theorem Th4:
for Y being non empty set for f being sequence of Y holds x
in rng f iff ex n st x = f.n
proof
let Y be non empty set;
let f be sequence of Y;
thus x in rng f implies ex n st x = f.n
proof
assume x in rng f;
then consider y being object such that
A1: y in dom f and
A2: x = f.y by FUNCT_1:def 3;
reconsider m=y as Element of NAT by A1;
take m;
thus thesis by A2;
end;
given n such that
A3: x = f.n;
A4: n in NAT by ORDINAL1:def 12;
dom f = NAT by FUNCT_2:def 1;
hence thesis by A3,FUNCT_1:def 3,A4;
end;
theorem Th5:
for Y be non empty set for f being sequence of Y holds rng f
= {f.k : 0 <= k}
proof
let Y be non empty set;
let f be sequence of Y;
set Z = {f.k : 0 <= k};
A1: dom f = NAT by FUNCT_2:def 1;
A2: rng f c= Z
proof
let y be object;
assume y in rng f;
then consider n be object such that
A3: n in NAT and
A4: y = f.n by A1,FUNCT_1:def 3;
reconsider n as Element of NAT by A3;
0 <= n by NAT_1:2;
hence thesis by A4;
end;
Z c= rng f
proof
let x be object;
assume x in Z;
then consider n1 being Nat such that
A5: x=f.n1 & 0 <= n1;
n1 in NAT by ORDINAL1:def 12;
hence thesis by FUNCT_2:4,A5;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Th6:
for Y being non empty set for f being sequence of Y holds rng
(f ^\ k) = {f.n: k <= n}
proof
let Y be non empty set;
let f be sequence of Y;
reconsider f1 = f ^\ k as sequence of Y;
rng f1 = {f.m: k <= m}
proof
set Z = {f.m : k <= m};
A1: dom f1 = NAT by FUNCT_2:def 1;
A2: rng f1 c= Z
proof
let y be object;
assume y in rng f1;
then consider m1 be object such that
A3: m1 in NAT and
A4: y = f1.m1 by A1,FUNCT_1:def 3;
reconsider m1 as Element of NAT by A3;
y = f.(k+m1) by A4,NAT_1:def 3;
hence thesis by Th1;
end;
Z c= rng f1
proof
let x be object;
assume x in Z;
then consider k1 being Nat such that
A5: x = f.k1 and
A6: k <= k1;
consider k2 being Nat such that
A7: k1 = k + k2 by A6,NAT_1:10;
k2 in NAT & x = f1.k2 by A5,A7,NAT_1:def 3,ORDINAL1:def 12;
hence thesis by FUNCT_2:4;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
hence thesis;
end;
theorem Th7:
x in meet rng B iff for n being Nat holds x in B.n
proof
A1: dom B = NAT by FUNCT_2:def 1;
A2: now
let x;
assume
A3: for n being Nat holds x in B.n;
now
let Y;
assume Y in rng B;
then consider n be object such that
A4: n in NAT and
A5: Y = B.n by A1,FUNCT_1:def 3;
thus x in Y by A3,A4,A5;
end;
hence x in meet rng B by SETFAM_1:def 1;
end;
now
let x;
assume
A6: x in meet rng B;
now
let k be Nat;
k in NAT by ORDINAL1:def 12;
then B.k in rng B by FUNCT_2:4;
hence x in B.k by A6,SETFAM_1:def 1;
end;
hence for n being Nat holds x in B.n;
end;
hence thesis by A2;
end;
theorem Th8:
Intersection B = meet rng B
proof
now
let x be object;
assume x in meet rng B;
then for n being Nat holds x in B.n by Th7;
hence x in Intersection B by PROB_1:13;
end;
then
A1: meet rng B c= Intersection B;
Intersection B c= meet rng B
proof
let x be object;
assume x in Intersection B;
then for n being Nat holds x in B.n by PROB_1:13;
hence thesis by Th7;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem
Intersection B c= Union B
proof
meet rng B c= union rng B by SETFAM_1:2;
then Intersection B c= union rng B by Th8;
hence thesis by CARD_3:def 4;
end;
theorem Th10:
(for n holds B.n = A) implies Union B = A
proof
assume
A1: for n holds B.n = A;
now
let x be object;
assume x in rng B;
then ex n st x = B.n by Th4;
hence x = A by A1;
end;
then rng B = {A} by ZFMISC_1:35;
then union rng B = A by ZFMISC_1:25;
hence thesis by CARD_3:def 4;
end;
theorem Th11:
(for n holds B.n = A) implies Intersection B = A
proof
assume
A1: for n holds B.n = A;
now
let x be object;
assume x in rng B;
then ex n st x = B.n by Th4;
hence x = A by A1;
end;
then rng B = {A} by ZFMISC_1:35;
then meet rng B = A by SETFAM_1:10;
hence thesis by Th8;
end;
theorem
B is constant implies Union B = Intersection B
proof
assume B is constant;
then consider A being Subset of X such that
A1: for n being Nat holds B.n = A by VALUED_0:def 18;
Union B = A by Th10,A1;
hence thesis by Th11,A1;
end;
Lm2: B is constant & the_value_of B = A implies for n holds B.n = A & Union B
= A & Intersection B = A
proof
assume that
A1: B is constant and
A2: the_value_of B = A;
consider x being set such that
A3: x in dom B and
A4: A = B.x by A1,A2,FUNCT_1:def 12;
A5: dom B = NAT by FUNCT_2:def 1;
for n holds B.n = A
proof let n;
reconsider n as Element of NAT by ORDINAL1:def 12;
B.n = A by A1,A3,A4,FUNCT_1:def 10,A5;
hence thesis;
end;
hence thesis by Th10,Th11;
end;
theorem Th13:
B is constant & the_value_of B = A implies for n holds union {B.
k: n <= k} = A
proof
assume
A1: B is constant & the_value_of B = A;
let n;
set Y = {B.k : n <= k};
A2: now
let x be object;
assume x in Y;
then ex k st x = B.k & n <= k;
hence x = A by A1,Lm2;
end;
Y <> {} by Th1;
then Y = {A} by A2,ZFMISC_1:35;
hence thesis by ZFMISC_1:25;
end;
theorem Th14:
B is constant & the_value_of B = A implies for n holds meet {B.k
: n <= k} = A
proof
assume
A1: B is constant & the_value_of B = A;
let n;
set Y = {B.k : n <= k};
A2: now
let x be object;
assume x in Y;
then ex k st x = B.k & n <= k;
hence x = A by A1,Lm2;
end;
Y <> {} by Th1;
then Y = {A} by A2,ZFMISC_1:35;
hence thesis by SETFAM_1:10;
end;
theorem Th15:
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
proof
let X, B;
let f be Function such that
A1: dom f = NAT and
A2: for n holds f.n = meet {B.k: n <= k};
rng f c= bool X
proof
let z be object;
assume z in rng f;
then consider x being object such that
A3: x in dom f and
A4: z = f.x by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A1,A3;
set Y = {B.k: n <= k};
set y = meet Y;
A5: y is Subset of X
proof
per cases;
suppose Y<>{};
then consider Z1 being object such that
A6: Z1 in Y by XBOOLE_0:def 1;
reconsider Z1 as set by TARSKI:1;
consider k1 being Nat such that
A7: Z1 = B.k1 & n <= k1 by A6;
reconsider k1 as Element of NAT by ORDINAL1:def 12;
now
let x be object;
assume x in y;
then x in Z1 by A6,SETFAM_1:def 1;
then x in B.k1 by A7;
hence x in X;
end;
hence thesis by TARSKI:def 3;
end;
suppose Y = {};
then y = {} by SETFAM_1:def 1;
hence thesis by XBOOLE_1:2;
end;
end;
z = y by A2,A4;
hence thesis by A5;
end;
hence thesis by A1,FUNCT_2:2;
end;
theorem Th16:
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
proof
let X be set, B be SetSequence of X;
let f be Function such that
A1: dom f = NAT and
A2: for n holds f.n = union {B.k: n <= k};
rng f c= bool X
proof
let z be object;
assume z in rng f;
then consider x being object such that
A3: x in dom f and
A4: z = f.x by FUNCT_1:def 3;
reconsider n = x as Nat by A1,A3;
set Y = {B.k: n <= k};
set y = union Y;
now
let z be object;
assume z in y;
then ex Z st z in Z & Z in Y by TARSKI:def 4;
then consider Z1 be set such that
A5: Z1 in Y and
A6: z in Z1;
consider k1 such that
A7: Z1 = B.k1 & n <= k1 by A5;
reconsider k1 as Element of NAT by ORDINAL1:def 12;
Z1 = B.k1 by A7;
hence z in X by A6;
end;
then
A8: y is Subset of X by TARSKI:def 3;
z = y by A2,A4;
hence thesis by A8;
end;
hence thesis by A1,FUNCT_2:2;
end;
definition
let X,B;
attr B is monotone means
B is non-descending or B is non-ascending;
end;
definition
let B be Function;
func inferior_setsequence B -> Function means
:Def2:
dom it = NAT & for n holds it.n = meet {B.k : n <= k};
existence
proof
deffunc F(Nat) = meet {B.k : $1 <= k};
consider f being Function such that
A1: dom f = NAT & for n being Element of NAT holds
f.n = F(n) from FUNCT_1:sch 4;
take f;
thus dom f = NAT by A1;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let BSeq,CSeq be Function such that
A2: dom BSeq = NAT & for n holds BSeq.n = meet {B.k : n <= k} and
A3: dom CSeq = NAT & for m holds CSeq.m = meet {B.k : m <= k};
for y being object st y in NAT holds BSeq.y = CSeq.y
proof
let y be object;
assume y in NAT;
then reconsider y as Nat;
set Y = {B.k: y <= k};
BSeq.y = meet Y by A2;
hence thesis by A3;
end;
hence thesis by A2,A3,FUNCT_1:2;
end;
end;
definition
let X be set, B be SetSequence of X;
redefine func inferior_setsequence B -> SetSequence of X; :: redefines inferior_setsequence (SETLIM_1, definition)
coherence
proof
A1: for n be Nat holds (inferior_setsequence B).n = meet {B.k :
n <= k} by Def2;
dom inferior_setsequence B = NAT by Def2;
hence thesis by A1,Th15;
end;
end;
definition
let B be Function;
func superior_setsequence B -> Function means
:Def3:
dom it = NAT & for n holds it.n = union {B.k : n <= k};
existence
proof
deffunc F(Nat) = union {B.k : $1 <= k};
consider f being Function such that
A1: dom f = NAT & for n be Element of NAT holds f.
n = F(n) from FUNCT_1:sch 4;
take f;
thus dom f = NAT by A1;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let BSeq,CSeq be Function such that
A2: dom BSeq = NAT & for n holds BSeq.n = union {B.k : n <= k} and
A3: dom CSeq = NAT & for m holds CSeq.m = union {B.k : m <= k};
for y being object st y in NAT holds BSeq.y = CSeq.y
proof
let y be object;
assume y in NAT;
then reconsider y as Nat;
set Y = {B.k: y <= k};
BSeq.y = union Y by A2;
hence thesis by A3;
end;
hence thesis by A2,A3,FUNCT_1:2;
end;
end;
definition
let X be set, B be SetSequence of X;
redefine func superior_setsequence B -> SetSequence of X; :: redefines superior_setsequence (SETLIM_1, definition)
coherence
proof
A1: for n holds (superior_setsequence B).n = union {B.k : n <= k} by Def3;
dom superior_setsequence B = NAT by Def3;
hence thesis by A1,Th16;
end;
end;
theorem Th17:
(inferior_setsequence B).0 = Intersection B
proof
(inferior_setsequence B).0 = meet {B.k : k >= 0} by Def2
.= meet rng B by Th5
.= Intersection B by Th8;
hence thesis;
end;
theorem Th18:
(superior_setsequence B).0 = Union B
proof
(superior_setsequence B).0 = union {B.k : 0 <= k} by Def3
.= union rng B by Th5
.= Union B by CARD_3:def 4;
hence thesis;
end;
theorem Th19:
for n being Nat holds
x in (inferior_setsequence B).n iff
for k being Nat holds x in B.(n+k)
proof let n be Nat;
reconsider nn=n as Nat;
set Y = {B.k : nn <= k};
A1: (inferior_setsequence B).n
= meet {B.k : n <= k} by Def2;
A2: now
assume
A3: x in (inferior_setsequence B).n;
now
let k be Nat;
B.(n + k) in Y by Th1;
hence x in B.(n + k) by A1,A3,SETFAM_1:def 1;
end;
hence for k being Nat holds x in B.(n+k);
end;
A4: Y <> {} by Th1;
now
assume for k holds x in B.(n+k);
then for Z st Z in Y holds x in Z by Th3;
hence x in (inferior_setsequence B).n by A1,A4,SETFAM_1:def 1;
end;
hence thesis by A2;
end;
theorem Th20:
for n being Nat holds
x in (superior_setsequence B).n iff
ex k being Nat st x in B.(n + k)
proof let n be Nat;
set Y = {B.k : n <= k};
A1: (superior_setsequence B).n = union {B.k : n <= k} by Def3;
thus x in (superior_setsequence B).n
implies ex k being Nat st x in B.(n + k)
proof
assume x in (superior_setsequence B).n;
then consider Y1 being set such that
A2: x in Y1 and
A3: Y1 in Y by A1,TARSKI:def 4;
consider k11 being Nat such that
A4: Y1 = B.k11 and
A5: n <= k11 by A3;
ex k be Nat st k11 = n + k by A5,NAT_1:10;
then consider k22 being Nat such that
A6: Y1=B.(n + k22) by A4;
thus thesis by A2,A6;
end;
now
given k1 being Nat such that
A7: x in B.(n + k1);
B.(n+k1) in Y by Th1;
hence x in (superior_setsequence B).n by A1,A7,TARSKI:def 4;
end;
hence thesis;
end;
theorem Th21:
for n being Nat holds
(inferior_setsequence B).n = (inferior_setsequence B).(n+1) /\ B .n
proof
let n be Nat;
A1: (inferior_setsequence B).n = meet {B.k1 : n <= k1} by Def2;
A2: {B.k1: n <= k1} = {B.k2 : n+1 <=k2} \/ {B.n} by Th2;
A3: (inferior_setsequence B).(n+1) = meet {B.k2 : n+1 <= k2} by Def2;
A4: {B.k1 : n <= k1} <> {} by Th1;
A5: now
let x be object;
assume that
A6: x in (inferior_setsequence B).(n+1) and
A7: x in B.n;
for Z st Z in {B.k2 : n <= k2} holds x in Z
proof
let Z;
assume Z in {B.k1 : n <= k1};
then consider Z1 being set such that
A8: Z=Z1 & Z1 in {B.k1 : n <= k1};
consider k11 being Nat such that
A9: Z1=B.k11 & n <= k11 by A8;
now
per cases by A9,Lm1;
suppose
Z1=B.k11 & n = k11;
hence x in Z1 by A7;
end;
suppose
Z1=B.k11 & n+1 <= k11;
then Z1 in {B.k2 : n+1 <= k2};
hence x in Z1 by A3,A6,SETFAM_1:def 1;
end;
end;
hence thesis by A8;
end;
then x in meet {B.k2 : n <= k2} by A4,SETFAM_1:def 1;
hence x in (inferior_setsequence B).n by Def2;
end;
{B.k2 : n+1 <= k2} <> {} by Th1;
then
A10: (inferior_setsequence B).(n) c= (inferior_setsequence B).(n+1) by A1,A3,A2
,SETFAM_1:6,XBOOLE_1:7;
now
let x be object;
A11: B.n in {B.k1 : n <= k1};
assume x in (inferior_setsequence B).n;
hence x in (inferior_setsequence B).(n+1) & x in B.n by A1,A10,A11,
SETFAM_1:def 1;
end;
hence
(inferior_setsequence B).n = (inferior_setsequence B).(n+1) /\ B.n by A5,
XBOOLE_0:def 4;
end;
theorem Th22:
for n being Nat holds
(superior_setsequence B).n = (superior_setsequence B).(n+1) \/ B .n
proof
let n be Nat;
{B.k1: n <= k1} = {B.k2 : n+1 <=k2} \/ {B.n} by Th2;
then union {B.k2 : n+1 <= k2} c= union {B.k1 : n <= k1} by XBOOLE_1:7
,ZFMISC_1:77;
then (superior_setsequence B).(n+1) c= union {B.k1 : n <= k1} by Def3;
then
A1: (superior_setsequence B).(n+1) c= (superior_setsequence B).n by Def3;
A2: now
let x be object;
assume
A3: x in (superior_setsequence B).(n+1) or x in B.n;
thus x in (superior_setsequence B).n
proof
now
per cases by A3;
case
x in (superior_setsequence B).(n+1);
hence thesis by A1;
end;
case
A4: x in B.n;
B.n in {B.k1 : n <= k1};
then x in union {B.k1 : n <= k1} by A4,TARSKI:def 4;
hence thesis by Def3;
end;
end;
hence thesis;
end;
end;
now
let x be object;
assume x in (superior_setsequence B).n;
then x in union {B.k1 : n <= k1} by Def3;
then consider Y1 being set such that
A5: x in Y1 & Y1 in {B.k1 : n <= k1} by TARSKI:def 4;
consider k11 being Nat such that
A6: Y1=B.k11 & n <= k11 by A5;
now
per cases by A6,Lm1;
case
Y1=B.k11 & n = k11;
hence x in B.n by A5;
end;
case
Y1=B.k11 & n+1 <= k11;
then Y1 in {B.k2 : n+1 <= k2};
hence x in union {B.k2 : n+1 <= k2} by A5,TARSKI:def 4;
end;
end;
hence x in B.n or x in (superior_setsequence B).(n+1) by Def3;
end;
then for x being object holds
x in (superior_setsequence B).n iff x in B.n or x in (
superior_setsequence B).(n+1) by A2;
hence
(superior_setsequence B).n = (superior_setsequence B).(n+1) \/ B.n by
XBOOLE_0:def 3;
end;
theorem Th23:
inferior_setsequence B is non-descending
proof
now
let n be Nat;
(inferior_setsequence B).n = (inferior_setsequence B).(n+1) /\ B.n by Th21;
hence (inferior_setsequence B).n c= (inferior_setsequence B).(n+1) by
XBOOLE_1:17;
end;
hence thesis by PROB_2:7;
end;
theorem Th24:
superior_setsequence B is non-ascending
proof
now
let n be Nat;
(superior_setsequence B).n = (superior_setsequence B).(n+1) \/ B.n by Th22;
hence (superior_setsequence B).(n+1) c= (superior_setsequence B).n by
XBOOLE_1:7;
end;
hence thesis by PROB_2:6;
end;
theorem
inferior_setsequence B is monotone & superior_setsequence B is monotone
by Th23,Th24;
registration
let X be set, A be SetSequence of X;
cluster inferior_setsequence A -> non-descending for SetSequence of X;
coherence by Th23;
end;
registration
let X be set, A be SetSequence of X;
cluster superior_setsequence A -> non-ascending for SetSequence of X;
coherence by Th24;
end;
theorem
Intersection B c= (inferior_setsequence B).n
proof
0 <= n by NAT_1:2;
then (inferior_setsequence B).0 c= (inferior_setsequence B).n by PROB_1:def 5
;
hence thesis by Th17;
end;
theorem
(superior_setsequence B).n c= Union B
proof
0 <= n by NAT_1:2;
then (superior_setsequence B).n c= (superior_setsequence B).0 by PROB_1:def 4
;
hence thesis by Th18;
end;
theorem Th28:
for B,n holds {B.k: n <= k} is Subset-Family of X
proof
let B,n;
set Y1 = {B.k: n <= k};
Y1 c= bool X
proof
let x be object;
assume x in Y1;
then consider k such that
A1: x = B.k & n <= k;
reconsider k as Element of NAT by ORDINAL1:def 12;
x = B.k by A1;
hence thesis;
end;
hence thesis;
end;
theorem
Union B = (Intersection Complement B)`
proof
(Intersection Complement B)` = (Union Complement Complement B)`` by
PROB_1:def 3
.= Union B;
hence thesis;
end;
theorem Th30:
for n being Element of NAT holds
(inferior_setsequence B).n = ((superior_setsequence Complement B ).n)`
proof let n be Element of NAT;
set Y1 = {B.k1: n <= k1};
set Y2 = {(Complement B).k2 : n <= k2};
set Y3 = {(B.k)` where k is Element of NAT: n <= k};
A1: Y3 c= Y2
proof
let y be object;
assume y in Y3;
then consider k being Element of NAT such that
A2: y = (B.k)` and
A3: n <= k;
y = (Complement B).k by A2,PROB_1:def 2;
hence thesis by A3;
end;
Y2 c= Y3
proof
let x be object;
assume x in Y2;
then consider k such that
A4: x = (Complement B).k and
A5: n <= k;
reconsider k as Element of NAT by ORDINAL1:def 12;
x = (B.k)` by A4,PROB_1:def 2;
hence thesis by A5;
end;
then
A6: Y2 = Y3 by A1,XBOOLE_0:def 10;
A7: Y1 <> {} by Th1;
reconsider Y1 as Subset-Family of X by Th28;
A8: COMPLEMENT Y1 c= Y3
proof
let y be object;
assume
A9: y in COMPLEMENT Y1;
then reconsider y as Subset of X;
y` in Y1 by A9,SETFAM_1:def 7;
then consider k such that
A10: y` = B.k and
A11: n <= k;
reconsider k as Element of NAT by ORDINAL1:def 12;
y = (B.k)` by A10;
hence thesis by A11;
end;
Y3 c= COMPLEMENT Y1
proof
let x be object;
assume x in Y3;
then consider k being Element of NAT such that
A12: x = (B.k)` and
A13: n <= k;
reconsider z = B.k as Subset of X;
(z`)` in Y1 by A13;
hence thesis by A12,SETFAM_1:def 7;
end;
then Y3 = COMPLEMENT Y1 by A8,XBOOLE_0:def 10;
then
(superior_setsequence(Complement B)).n = union COMPLEMENT Y1 by A6,Def3
.= [#] X \ meet Y1 by A7,SETFAM_1:34
.= (meet Y1)`;
hence thesis by Def2;
end;
theorem
for n being Element of NAT holds
(superior_setsequence B).n = ((inferior_setsequence Complement B).n)`
proof let n be Element of NAT;
reconsider Y = (inferior_setsequence(Complement B)).n as Subset of X;
Y = ((superior_setsequence(Complement Complement B)).n)` by Th30
.= ((superior_setsequence B).n)`;
hence thesis;
end;
theorem Th32:
Complement (inferior_setsequence B) = (superior_setsequence Complement B)
proof
reconsider A2 = inferior_setsequence B as SetSequence of X;
reconsider A3 = superior_setsequence Complement B as SetSequence of X;
now
let n be Element of NAT;
(A2.n)` = ((A3.n)`)` by Th30;
hence (Complement A2).n = A3.n by PROB_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
theorem
Complement superior_setsequence B = inferior_setsequence Complement B
proof
reconsider A2 = inferior_setsequence Complement B as SetSequence of X;
Complement A2 = superior_setsequence Complement Complement B by Th32
.= superior_setsequence B;
hence thesis;
end;
theorem
(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
proof
assume
A1: for n being Nat holds A3.n = A1.n \/ A2.n;
let n be Nat;
set X1 = inferior_setsequence A1, X2 = inferior_setsequence A2, X3 =
inferior_setsequence A3;
now
let x be object;
assume
A2: x in X1.n \/ X2.n;
per cases by A2,XBOOLE_0:def 3;
suppose
A3: x in X1.n;
now
let k be Nat;
x in A1.(n+k) & A3.(n+k) = A1.(n+k) \/ A2.(n+k) by A1,A3,Th19;
hence x in A3.(n+k) by XBOOLE_0:def 3;
end;
hence x in X3.n by Th19;
end;
suppose
A4: x in X2.n;
now
let k be Nat;
x in A2.(n+k) & A3.(n+k) = A1.(n+k) \/ A2.(n+k) by A1,A4,Th19;
hence x in A3.(n+k) by XBOOLE_0:def 3;
end;
hence x in X3.n by Th19;
end;
end;
hence thesis;
end;
theorem
(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
proof
assume
A1: for n being Nat holds A3.n = A1.n /\ A2.n;
let n be Nat;
reconsider X3 = inferior_setsequence A3 as SetSequence of X;
reconsider X2 = inferior_setsequence A2 as SetSequence of X;
set B = A1;
reconsider X1 = inferior_setsequence B as SetSequence of X;
A2: X1.n /\ X2.n c= X3.n
proof
let x be object;
assume x in (X1.n /\ X2.n);
then
A3: x in X1.n & x in X2.n by XBOOLE_0:def 4;
now
let k be Nat;
x in B.(n+k) & x in A2.(n+k) by A3,Th19;
then x in B.(n+k) /\ A2.(n+k) by XBOOLE_0:def 4;
hence x in A3.(n+k) by A1;
end;
hence thesis by Th19;
end;
X3.n c= X1.n /\ X2.n
proof
let x be object;
assume
A4: x in X3.n;
now
let k be Nat;
x in A3.(n+k) by A4,Th19;
then x in (B.(n+k) /\ A2.(n+k)) by A1;
hence x in B.(n+k) & x in A2.(n+k) by XBOOLE_0:def 4;
end;
then x in X1.n & x in X2.n by Th19;
hence thesis by XBOOLE_0:def 4;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem
(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
proof
assume
A1: for n holds A3.n = A1.n \/ A2.n;
let n;
reconsider X3 = superior_setsequence A3 as SetSequence of X;
reconsider X2 = superior_setsequence A2 as SetSequence of X;
set B = A1;
reconsider X1 = superior_setsequence B as SetSequence of X;
A2: X1.n \/ X2.n c= X3.n
proof
let x be object;
assume
A3: x in (X1.n \/ X2.n);
per cases by A3,XBOOLE_0:def 3;
suppose
x in X1.n;
then consider k being Nat such that
A4: x in B.(n+k) by Th20;
A3.(n+k) = B.(n+k) \/ A2.(n+k) by A1;
then x in A3.(n+k) by A4,XBOOLE_0:def 3;
hence thesis by Th20;
end;
suppose
x in X2.n;
then consider k being Nat such that
A5: x in A2.(n+k) by Th20;
A3.(n+k) = B.(n+k) \/ A2.(n+k) by A1;
then x in A3.(n+k) by A5,XBOOLE_0:def 3;
hence thesis by Th20;
end;
end;
X3.n c= X1.n \/ X2.n
proof
let x be object;
assume x in X3.n;
then consider k being Nat such that
A6: x in A3.(n+k) by Th20;
A7: x in (B.(n+k) \/ A2.(n+k)) by A1,A6;
now
per cases by A7,XBOOLE_0:def 3;
case
x in B.(n+k);
hence x in X1.n by Th20;
end;
case
x in A2.(n+k);
hence x in X2.n by Th20;
end;
end;
hence thesis by XBOOLE_0:def 3;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem
(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
proof
assume
A1: for n holds A3.n = A1.n /\ A2.n;
let n;
reconsider X3 = superior_setsequence A3 as SetSequence of X;
reconsider X2 = superior_setsequence A2 as SetSequence of X;
set B = A1;
reconsider X1 = superior_setsequence B as SetSequence of X;
X3.n c= X1.n /\ X2.n
proof
let x be object;
assume x in X3.n;
then consider k being Nat such that
A2: x in A3.(n+k) by Th20;
A3: A3.(n+k) = B.(n+k) /\ A2.(n+k) by A1;
then x in A2.(n+k) by A2,XBOOLE_0:def 4;
then
A4: x in X2.n by Th20;
x in B.(n+k) by A2,A3,XBOOLE_0:def 4;
then x in X1.n by Th20;
hence thesis by A4,XBOOLE_0:def 4;
end;
hence thesis;
end;
theorem Th38:
B is constant & the_value_of B = A implies for n holds (
inferior_setsequence B).n = A
proof
assume
A1: B is constant & the_value_of B = A;
let n;
(inferior_setsequence(B)).n = meet {B.k : n <= k} by Def2;
hence thesis by A1,Th14;
end;
theorem Th39:
B is constant & the_value_of B = A implies for n holds (
superior_setsequence B).n = A
proof
assume
A1: B is constant & the_value_of B = A;
let n;
(superior_setsequence(B)).n = union {B.k : n <= k} by Def3;
hence thesis by A1,Th13;
end;
theorem Th40:
for n being Nat holds
B is non-descending implies B.n c= (superior_setsequence(B)).(n+ 1)
proof let n be Nat;
assume B is non-descending;
then
A1: B.n c= B.(n+1) by PROB_2:7;
B.n c= union {B.k : n+1 <= k}
proof
let x be object;
A2: B.(n+1) in {B.k : n+1 <= k};
assume x in B.n;
hence thesis by A1,A2,TARSKI:def 4;
end;
hence thesis by Def3;
end;
theorem Th41:
for n being Nat holds
B is non-descending implies (superior_setsequence B).n = (
superior_setsequence B).(n+1)
proof let n be Nat;
assume B is non-descending;
then (superior_setsequence B).(n+1) \/ B.n = (superior_setsequence B).(n+1)
by Th40,XBOOLE_1:12;
hence thesis by Th22;
end;
theorem Th42:
for n being Nat holds
B is non-descending implies (superior_setsequence B).n = Union B
proof let n be Nat;
defpred P[Nat] means (superior_setsequence B).$1 = Union B;
assume B is non-descending;
then
A1: for k being Nat st P[k] holds P[k+1] by Th41;
A2: P[0] by Th18;
for k being Nat holds P[k] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem Th43:
B is non-descending implies Intersection superior_setsequence B = Union B
proof
assume
A1: B is non-descending;
now
let x be object;
assume
A2: x in Intersection superior_setsequence B;
now
let n;
(superior_setsequence B).n = Union B by A1,Th42;
hence x in Union B by A2,PROB_1:13;
end;
hence x in Union B;
end;
then
A3: Intersection superior_setsequence(B) c= Union B;
now
let y be object;
assume y in Union B;
then for n being Nat holds y in (superior_setsequence(B)).n by A1,Th42;
hence y in Intersection superior_setsequence(B) by PROB_1:13;
end;
then Union B c= Intersection superior_setsequence(B);
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th44:
B is non-descending implies B.n c= (inferior_setsequence B).(n+1 )
proof
set Y = {B.k : n+1 <= k};
assume
A1: B is non-descending;
let x be object;
assume
A2: x in B.n;
A3: now
let y be set;
assume y in Y;
then consider k1 being Nat such that
A4: y=B.k1 and
A5: n+1 <= k1;
n <= k1 by A5,NAT_1:13;
then B.n c= B.k1 by A1,PROB_1:def 5;
hence x in y by A2,A4;
end;
A6: Y <> {} by Th1;
(inferior_setsequence B).(n+1) = meet {B.k : n+1 <= k} by Def2;
hence thesis by A6,A3,SETFAM_1:def 1;
end;
theorem Th45:
B is non-descending implies (inferior_setsequence B).n = B.n
proof
assume B is non-descending;
then (inferior_setsequence B).(n+1) /\ B.n = B.n by Th44,XBOOLE_1:28;
hence thesis by Th21;
end;
theorem Th46:
B is non-descending implies inferior_setsequence B = B
proof
assume B is non-descending;
then (inferior_setsequence B).n = B.n by Th45;
then for n being Element of NAT holds (inferior_setsequence B).n = B.n;
hence thesis by FUNCT_2:63;
end;
theorem Th47:
B is non-ascending implies (superior_setsequence B).(n+1) c= B.n
proof
assume
A1: B is non-ascending;
let x be object;
assume x in (superior_setsequence(B)).(n+1);
then consider k being Nat such that
A2: x in B.(n +1+k) by Th20;
n+1 <= n+1+k by NAT_1:11;
then n <= n+1+k by NAT_1:13;
then B.(n +1+k) c= B.n by A1,PROB_1:def 4;
hence thesis by A2;
end;
theorem Th48:
B is non-ascending implies (superior_setsequence(B)).n = B.n
proof
assume B is non-ascending;
then (superior_setsequence(B)).(n+1) \/ B.n = B.n by Th47,XBOOLE_1:12;
hence thesis by Th22;
end;
theorem Th49:
B is non-ascending implies superior_setsequence(B) = B
proof
assume B is non-ascending;
then (superior_setsequence(B)).n = B.n by Th48;
then for n being Element of NAT holds (superior_setsequence(B)).n = B.n;
hence thesis by FUNCT_2:63;
end;
theorem Th50:
for n being Nat holds
B is non-ascending implies (inferior_setsequence(B)).(n+1) c= B. n
proof let n be Nat;
set Y = {B.k : n+1 <= k};
assume B is non-ascending;
then
A1: B.(n+1) c= B.n by PROB_2:6;
A2: B.(n+1) in Y;
A3: now
let x be object;
assume x in meet Y;
then x in B.(n+1) by A2,SETFAM_1:def 1;
hence x in B.n by A1;
end;
(inferior_setsequence(B)).(n+1) = meet {B.k : n+1 <= k} by Def2;
hence thesis by A3;
end;
theorem Th51:
for n being Nat holds
B is non-ascending implies (inferior_setsequence(B)).n = (
inferior_setsequence(B)).(n+1)
proof let n be Nat;
assume B is non-ascending;
then
(inferior_setsequence(B)).(n+1) /\ B.n = (inferior_setsequence(B)).(n+1)
by Th50,XBOOLE_1:28;
hence thesis by Th21;
end;
theorem Th52:
for n being Nat holds
B is non-ascending implies (inferior_setsequence(B)).n = Intersection B
proof let n be Nat;
defpred P[Nat] means (inferior_setsequence(B)).$1 = Intersection B;
assume B is non-ascending;
then
A1: for k being Nat st P[k] holds P[k+1] by Th51;
A2: P[0] by Th17;
for k being Nat holds P[k] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem Th53:
B is non-ascending implies Union inferior_setsequence(B) = Intersection B
proof
assume
A1: B is non-ascending;
now
let x be object;
assume x in Union inferior_setsequence(B);
then ex k being Nat st x in (inferior_setsequence(B)).k by PROB_1:12;
hence x in Intersection B by A1,Th52;
end;
then
A2: Union inferior_setsequence(B) c= Intersection B;
now
let y be object;
assume y in Intersection B;
then y in (inferior_setsequence(B)).0 by Th17;
hence y in Union inferior_setsequence(B) by PROB_1:12;
end;
then Intersection B c= Union inferior_setsequence(B);
hence thesis by A2,XBOOLE_0:def 10;
end;
definition
let X be set, B be SetSequence of X;
redefine func lim_inf B equals :: redefines lim_inf (KURATO_0, definition)
Union inferior_setsequence B;
compatibility
proof
let F be Subset of X;
hereby
assume
A1: F = lim_inf B;
for x being object holds x in F iff x in Union inferior_setsequence B
proof
let x be object;
hereby
assume x in F;
then consider n being Nat such that
A2: for k being Nat holds x in B.(n+k) by A1,KURATO_0:4;
x in (inferior_setsequence B).n by A2,Th19;
hence x in Union inferior_setsequence B by PROB_1:12;
end;
assume x in Union inferior_setsequence B;
then consider n being Nat such that
A3: x in (inferior_setsequence B).n by PROB_1:12;
for k being Nat holds x in B.(n + k) by A3,Th19;
hence thesis by A1,KURATO_0:4;
end;
hence F = Union inferior_setsequence B by TARSKI:2;
end;
assume
A4: F = Union inferior_setsequence B;
for x being object holds x in F iff x in lim_inf B
proof
let x be object;
hereby
assume x in F;
then consider n being Nat such that
A5: x in (inferior_setsequence B).n by A4,PROB_1:12;
for k being Nat holds x in B.(n + k) by A5,Th19;
hence x in lim_inf B by KURATO_0:4;
end;
assume x in lim_inf B;
then consider n being Nat such that
A6: for k being Nat holds x in B.(n+k) by KURATO_0:4;
x in (inferior_setsequence B).n by A6,Th19;
hence thesis by A4,PROB_1:12;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let X be set, B be SetSequence of X;
redefine func lim_sup B equals :: redefines lim_sup (KURATO_0, definition)
Intersection superior_setsequence B;
compatibility
proof
let F be Subset of X;
hereby
assume
A1: F = lim_sup B;
for x being object
holds x in F iff x in Intersection superior_setsequence B
proof
let x be object;
hereby
assume
A2: x in F;
for m being Nat holds x in (superior_setsequence B).m
proof
let m be Nat;
ex k being Nat st x in B.(m+k) by A1,A2,KURATO_0:5;
hence thesis by Th20;
end;
hence x in Intersection superior_setsequence B by PROB_1:13;
end;
assume
A3: x in Intersection superior_setsequence B;
now
let m be Nat;
x in (superior_setsequence B).m by A3,PROB_1:13;
hence ex k being Nat st x in B.(m + k) by Th20;
end;
hence thesis by A1,KURATO_0:5;
end;
hence F = Intersection superior_setsequence B by TARSKI:2;
end;
assume
A4: F = Intersection superior_setsequence B;
for x being object holds x in F iff x in lim_sup B
proof
let x be object;
hereby
assume
A5: x in F;
now
let m be Nat;
x in (superior_setsequence B).m by A4,A5,PROB_1:13;
hence ex k being Nat st x in B.(m + k) by Th20;
end;
hence x in lim_sup B by KURATO_0:5;
end;
assume
A6: x in lim_sup B;
for m being Nat holds x in (superior_setsequence B).m
proof
let m be Nat;
ex k being Nat st x in B.(m+k) by A6,KURATO_0:5;
hence thesis by Th20;
end;
hence thesis by A4,PROB_1:13;
end;
hence thesis by TARSKI:2;
end;
end;
notation
let X be set, B be SetSequence of X;
synonym lim↑ B for lim_sup B;
end;
theorem
Intersection B c= lim_inf B
proof
let x be object;
assume x in Intersection B;
then for k being Nat holds x in B.(0+k) by PROB_1:13;
hence thesis by KURATO_0:4;
end;
theorem
lim_inf B = lim inferior_setsequence(B) by Th43;
theorem
lim_sup B = lim superior_setsequence(B) by Th49;
theorem
lim_sup B = (lim_inf Complement B)`
proof
lim_inf Complement B = (lim_sup Complement Complement B)` by KURATO_0:9
.= (lim_sup B)`;
hence thesis;
end;
theorem Th58:
B is constant & the_value_of B = A implies B is convergent & lim
B = A & lim_inf B = A & lim_sup B = A
proof
assume
A1: B is constant & the_value_of B = A;
then for n holds (superior_setsequence(B)).n = A by Th39;
then
A2: lim_sup B = A by Th11;
for n holds (inferior_setsequence(B)).n = A by A1,Th38;
then lim_inf B = A by Th10;
hence thesis by A2,KURATO_0:def 5;
end;
theorem
B is non-descending implies lim_sup B = Union B by Th43;
theorem
B is non-descending implies lim_inf B = Union B by Th46;
theorem
B is non-ascending implies lim_sup B = Intersection B by Th49;
theorem
B is non-ascending implies lim_inf B = Intersection B by Th53;
theorem Th63:
B is non-descending implies B is convergent & lim B = Union B
proof
assume
A1: B is non-descending;
then lim_sup B = Union B & lim_inf B = Union B by Th43,Th46;
hence B is convergent by KURATO_0:def 5;
thus thesis by A1,Th43;
end;
theorem Th64:
B is non-ascending implies B is convergent & lim B = Intersection B
proof
assume
A1: B is non-ascending;
then lim_sup B = Intersection B & lim_inf B = Intersection B by Th49,Th53;
hence B is convergent by KURATO_0:def 5;
thus thesis by A1,Th49;
end;
theorem
B is monotone implies B is convergent
proof
assume
A1: B is monotone;
per cases by A1;
suppose
B is non-ascending;
hence thesis by Th64;
end;
suppose
B is non-descending;
hence thesis by Th63;
end;
end;
definition
let X be set, Si be SigmaField of X, S be SetSequence of Si;
redefine func inferior_setsequence S -> SetSequence of Si; :: redefines inferior_setsequence (SETLIM_1, definition)
coherence
proof
now
let n be Nat;
reconsider DSeq = S ^\ n as SetSequence of X;
reconsider n1=n as Nat;
for m being Nat holds DSeq.m in Si
proof
let m be Nat;
DSeq.m = S.(m+n1) & S.(m+n1) in rng S by NAT_1:51,def 3;
hence thesis;
end;
then rng DSeq c= Si by NAT_1:52;
then
A1: Intersection DSeq in Si by PROB_1:def 6;
Intersection DSeq = meet rng DSeq by Th8;
then Intersection DSeq = meet {S.k: n1 <= k} by Th6;
hence (inferior_setsequence S).n in Si by A1,Def2;
end;
then rng inferior_setsequence S c= Si by NAT_1:52;
hence thesis by RELAT_1:def 19;
end;
end;
definition
let X be set, Si be SigmaField of X, S be SetSequence of Si;
redefine func superior_setsequence S -> SetSequence of Si; :: redefines superior_setsequence (SETLIM_1, definition)
coherence
proof
now
let n be Nat;
reconsider DSeq = S ^\ n as SetSequence of X;
reconsider n1=n as Nat;
A1: Union DSeq in Si by PROB_1:17;
Union DSeq = union rng DSeq by CARD_3:def 4;
then Union DSeq =union {S.k: n1 <= k} by Th6;
hence (superior_setsequence(S)).n in Si by A1,Def3;
end;
then rng superior_setsequence S c= Si by NAT_1:52;
hence thesis by RELAT_1:def 19;
end;
end;
theorem Th66:
x in lim_sup S iff for n being Nat
ex k being Nat st x in S.(n+k)
proof
x in Intersection superior_setsequence B iff
for n being Nat ex k being Nat st x in B.(n+k)
proof
lim_sup B = Intersection superior_setsequence B;
hence thesis by KURATO_0:5;
end;
hence thesis;
end;
theorem Th67:
x in lim_inf S iff ex n being Nat st for k being Nat holds x in S.(n+k)
proof
x in Union inferior_setsequence(B) iff
ex n being Nat st for k being Nat holds x in B.(n+k)
proof
lim_inf B = Union inferior_setsequence(B);
hence thesis by KURATO_0:4;
end;
hence thesis;
end;
theorem
Intersection S c= lim_inf S
proof
let x be object;
assume x in Intersection S;
then for k being Nat holds x in S.(0+k) by PROB_1:13;
hence thesis by Th67;
end;
theorem
lim_sup S c= Union S
proof
let x be object;
assume x in lim_sup S;
then ex k being Nat st x in S.(0+k) by Th66;
hence thesis by PROB_1:12;
end;
theorem
lim_inf S c= lim_sup S
proof
Union inferior_setsequence B c= Intersection superior_setsequence B
proof
lim_inf B = Union inferior_setsequence(B) & lim_sup B = Intersection
superior_setsequence(B);
hence thesis by KURATO_0:6;
end;
hence thesis;
end;
theorem Th71:
lim_inf S = (lim_sup Complement S)`
proof
Union inferior_setsequence(B) = (Intersection superior_setsequence(
Complement B))`
proof
lim_inf B = Union inferior_setsequence(B) & (lim_sup Complement B)` =
( Intersection superior_setsequence(Complement B))`;
hence thesis by KURATO_0:9;
end;
hence thesis;
end;
theorem
lim_sup S = (lim_inf Complement S)`
proof
lim_inf (Complement S qua non empty SetSequence of X)
= (lim_sup Complement Complement S)` by Th71
.= (lim_sup S)`;
hence thesis;
end;
theorem
(for n being Nat holds S3.n = S1.n \/ S2.n)
implies lim_inf S1 \/ lim_inf S2 c=
lim_inf S3
proof
A1: (for n being Nat holds A3.n = B.n \/ A2.n)
implies Union inferior_setsequence(B)
\/ Union inferior_setsequence(A2) c= Union inferior_setsequence(A3)
proof
A2: lim_inf B = Union inferior_setsequence(B) & lim_inf A2 = Union
inferior_setsequence(A2);
A3: lim_inf A3 = Union inferior_setsequence(A3);
assume for n being Nat holds A3.n = B.n \/ A2.n;
hence thesis by A2,A3,KURATO_0:12;
end;
assume for n being Nat holds S3.n = S1.n \/ S2.n;
hence thesis by A1;
end;
theorem
(for n being Nat holds S3.n = S1.n /\ S2.n)
implies lim_inf S3 = lim_inf S1 /\
lim_inf S2
proof
A1: (for n being Nat holds A3.n = B.n /\ A2.n)
implies Union inferior_setsequence(B)
/\ Union inferior_setsequence(A2) = Union inferior_setsequence(A3)
proof
A2: lim_inf B = Union inferior_setsequence(B) & lim_inf A2 = Union
inferior_setsequence(A2);
A3: lim_inf A3 = Union inferior_setsequence(A3);
assume for n being Nat holds A3.n = B.n /\ A2.n;
hence thesis by A2,A3,KURATO_0:10;
end;
assume for n being Nat holds S3.n = S1.n /\ S2.n;
hence thesis by A1;
end;
theorem
(for n being Nat holds S3.n = S1.n \/ S2.n)
implies lim_sup S3 = lim_sup S1 \/
lim_sup S2
proof
A1: (for n being Nat holds A3.n = B.n \/ A2.n)
implies Intersection
superior_setsequence(B) \/ Intersection superior_setsequence(A2) = Intersection
superior_setsequence(A3)
proof
A2: lim_sup B = Intersection superior_setsequence(B) & lim_sup A2 =
Intersection superior_setsequence(A2);
A3: lim_sup A3 = Intersection superior_setsequence(A3);
assume for n being Nat holds A3.n = B.n \/ A2.n;
hence thesis by A2,A3,KURATO_0:11;
end;
assume for n being Nat holds S3.n = S1.n \/ S2.n;
hence thesis by A1;
end;
theorem
(for n being Nat holds S3.n = S1.n /\ S2.n)
implies lim_sup S3 c= lim_sup S1 /\ lim_sup S2
proof
A1: (for n being Nat holds A3.n = B.n /\ A2.n) implies Intersection
superior_setsequence(A3) c= Intersection superior_setsequence(B) /\
Intersection superior_setsequence(A2)
proof
A2: lim_sup B = Intersection superior_setsequence(B) & lim_sup A2 =
Intersection superior_setsequence(A2);
A3: lim_sup A3 = Intersection superior_setsequence(A3);
assume for n being Nat holds A3.n = B.n /\ A2.n;
hence thesis by A2,A3,KURATO_0:13;
end;
assume for n being Nat holds S3.n = S1.n /\ S2.n;
hence thesis by A1;
end;
theorem
S is constant & the_value_of S = A implies S is convergent & lim S = A
& lim_inf S = A & lim_sup S = A
proof
A1: B is constant & the_value_of B = A implies Union inferior_setsequence(B)
= A & Intersection superior_setsequence(B) = A
proof
A2: lim_inf B = Union inferior_setsequence(B) & lim_sup B = Intersection
superior_setsequence(B);
assume B is constant & the_value_of B = A;
hence thesis by A2,Th58;
end;
assume S is constant & the_value_of S = A;
then lim_inf S = A & lim_sup S = A by A1;
hence thesis by KURATO_0:def 5;
end;
theorem Th78:
S is non-descending implies lim_sup S = Union S by Th43;
theorem Th79:
S is non-descending implies lim_inf S = Union S by Th46;
theorem Th80:
S is non-descending implies S is convergent & lim S = Union S
proof
assume
A1: S is non-descending;
then lim_sup S = Union S & lim_inf S = Union S by Th78,Th79;
hence S is convergent by KURATO_0:def 5;
thus thesis by A1,Th78;
end;
theorem Th81:
S is non-ascending implies lim_sup S = Intersection S by Th49;
theorem Th82:
S is non-ascending implies lim_inf S = Intersection S by Th53;
theorem Th83:
S is non-ascending implies S is convergent & lim S = Intersection S
proof
assume
A1: S is non-ascending;
then lim_sup S = Intersection S & lim_inf S = Intersection S by Th81,Th82;
hence S is convergent by KURATO_0:def 5;
thus thesis by A1,Th81;
end;
theorem
S is monotone implies S is convergent
proof
assume
A1: S is monotone;
per cases by A1;
suppose
S is non-ascending;
hence thesis by Th83;
end;
suppose
S is non-descending;
hence thesis by Th80;
end;
end;