:: Set Sequences and Monotone Class
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received August 12, 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 NUMBERS, NAT_1, XREAL_0, PROB_1, FINSEQ_1, ZFMISC_1, XBOOLE_0,
CARD_1, ARYTM_3, XXREAL_0, ARYTM_1, RELAT_1, SEQ_1, FUNCT_1, SEQ_2,
ORDINAL2, SUBSET_1, COMPLEX1, RPR_1, TARSKI, VALUED_0, EQREL_1, CARD_3,
PROB_2, SERIES_1, XXREAL_2, FINSEQ_2, SETFAM_1, BINOP_2, SETWISEO,
FINSOP_1, SEQM_3, SETLIM_2, PROB_3, SEQ_4, REAL_1;
notations FINSEQ_1, ORDINAL1, CARD_3, REAL_1, RELAT_1, TARSKI, XBOOLE_0,
RVSUM_1, FINSOP_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, SETFAM_1,
VALUED_0,
BINOP_1, SETWOP_2, BINOP_2, SETWISEO, NAT_1, FINSEQ_2, COMPLEX1, SEQ_1,
COMSEQ_2, SEQ_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, PROB_1, PROB_2,
KURATO_0, SETLIM_2, SEQM_3, SETLIM_1, RINFSUP1, SERIES_1, XXREAL_0;
constructors SETFAM_1, PARTFUN1, SETWISEO, XXREAL_0, REAL_1, NAT_1, BINOP_2,
COMPLEX1, SEQ_2, SEQM_3, PROB_2, FINSOP_1, RVSUM_1, SERIES_1, BINOP_1,
KURATO_0, SETLIM_1, RINFSUP1, SETLIM_2, PROB_1, RELSET_1, SETWOP_2,
COMSEQ_2;
registrations SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, PROB_1,
VALUED_0, SEQ_2, FUNCT_2, FINSEQ_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, RELAT_1, FINSEQ_1;
equalities XBOOLE_0, FINSEQ_2;
expansions TARSKI, XBOOLE_0, RELAT_1, FUNCT_2;
theorems FUNCT_1, FUNCT_2, SEQ_1, ABSVALUE, SEQ_2, SUBSET_1, NAT_1, TARSKI,
XBOOLE_0, XBOOLE_1, PROB_2, SETLIM_2, RINFSUP1, RELAT_1, SETFAM_1,
ZFMISC_1, SEQM_3, CARD_3, SETLIM_1, PROB_1, FINSUB_1, SERIES_1, FINSEQ_1,
FINSEQ_2, FINSEQ_3, RVSUM_1, FINSOP_1, SETWISEO, BINOP_2, XREAL_1,
XXREAL_0, ORDINAL1, VALUED_0, FUNCOP_1, XREAL_0;
schemes CLASSES1, NAT_1, RECDEF_1, FINSEQ_2, PARTFUN1;
begin
reserve n,m,k,i for Nat,
g,s,t,p for Real,
x,y,z for object, X,Y,Z for set,
A1 for SetSequence of X,
F1 for FinSequence of bool X,
RFin for real-valued FinSequence,
Si for SigmaField of X,
XSeq,YSeq for SetSequence of Si,
Omega for non empty set,
Sigma for SigmaField of Omega,
ASeq,BSeq for SetSequence of Sigma,
P for Probability of Sigma;
Lm1: for s st 0 < s & t <= p holds t < p+s & t-s < p
proof
let s;
assume 0<s & t <= p;
then t+0 < p+s by XREAL_1:8;
hence thesis by XREAL_1:19;
end;
theorem Th1:
for f being FinSequence holds not 0 in dom f
proof
let f be FinSequence;
assume 0 in dom f;
then 0 in Seg len f by FINSEQ_1:def 3;
hence contradiction by FINSEQ_1:1;
end;
theorem Th2:
for f being FinSequence holds n in dom f iff n<>0 & n <= len f
proof
let f be FinSequence;
n in dom f iff n>=1 & n <= len f by FINSEQ_3:25;
hence thesis by NAT_1:14;
end;
theorem Th3:
for f being Real_Sequence st (ex k st for n st k<=n holds f.n=g)
holds f is convergent & lim f = g
proof
let f be Real_Sequence;
given k such that
A1: for n st k<=n holds f.n=g;
A2: now
let p such that
A3: 0 < p;
take k;
let m be Nat;
assume k<=m;
then f.m = g by A1;
hence |.f.m-g.|<p by A3,ABSVALUE:2;
end;
hence f is convergent by SEQ_2:def 6;
hence thesis by A2,SEQ_2:def 7;
end;
theorem Th4:
(P * ASeq).n >= 0
proof
A1: n in NAT by ORDINAL1:def 12;
dom (P * ASeq) = NAT by SEQ_1:1;
then (P * ASeq).n = P.(ASeq.n) by A1,FUNCT_1:12;
hence thesis by PROB_1:def 8;
end;
theorem Th5:
ASeq.n c= BSeq.n implies (P * ASeq).n <= (P * BSeq).n
proof
A1: n in NAT by ORDINAL1:def 12;
assume ASeq.n c= BSeq.n;
then P.(ASeq.n) <= P.(BSeq.n) by PROB_1:34;
then (P * ASeq).n <= P.(BSeq.n) by A1,FUNCT_2:15;
hence thesis by A1,FUNCT_2:15;
end;
theorem Th6:
ASeq is non-descending implies P * ASeq is non-decreasing
proof
A1: dom (P * ASeq) = NAT by SEQ_1:1;
assume
A2: ASeq is non-descending;
now
let n,m be Nat;
assume n <= m;
then
A3: ASeq.n c= ASeq.m by A2,PROB_1:def 5;
reconsider nn=n, mm=m as Element of NAT by ORDINAL1:def 12;
(P * ASeq).nn = P.(ASeq.nn) & (P * ASeq).mm = P.(ASeq.mm)
by A1,FUNCT_1:12;
hence (P * ASeq).n <= (P * ASeq).m by A3,PROB_1:34;
end;
hence thesis by SEQM_3:6;
end;
theorem Th7:
ASeq is non-ascending implies P * ASeq is non-increasing
proof
A1: dom (P * ASeq) = NAT by SEQ_1:1;
assume
A2: ASeq is non-ascending;
now
let n,m be Nat;
assume n <= m;
then
A3: ASeq.m c= ASeq.n by A2,PROB_1:def 4;
reconsider nn=n, mm=m as Element of NAT by ORDINAL1:def 12;
(P * ASeq).nn = P.(ASeq.nn) & (P * ASeq).mm = P.(ASeq.mm)
by A1,FUNCT_1:12;
hence (P * ASeq).m <= (P * ASeq).n by A3,PROB_1:34;
end;
hence thesis by SEQM_3:8;
end;
definition
let X be set, A1 be SetSequence of X;
func Partial_Intersection A1 -> SetSequence of X means
:Def1:
it.0 = A1.0 & for n being Nat holds it.(n+1) = it.n /\ A1.(n+1);
existence
proof
defpred P[set,set,set] means for x,y being Subset of X,s being Nat holds s =
$1 & x = $2 & y = $3 implies y = x /\ A1.(s+1);
A1: for n being Nat for x being Subset of X ex y being Subset of
X st P[n,x,y]
proof
let n be Nat;
let x be Subset of X;
take x /\ A1.(n+1);
thus thesis;
end;
consider F being SetSequence of X such that
A2: F.0 = A1.0 and
A3: for n being Nat holds P[n,F.n,F.(n+1)] from RECDEF_1:sch
2(A1 );
take F;
thus F.0 = A1.0 by A2;
let n be Nat;
reconsider n as Element of NAT by ORDINAL1:def 12;
P[n,F.n,F.(n+1)] by A3;
hence thesis;
end;
uniqueness
proof
let S1,S2 be SetSequence of X such that
A4: S1.0 = A1.0 and
A5: for n being Nat holds S1.(n+1) = S1.n /\ A1.(n+1) and
A6: S2.0 = A1.0 and
A7: for n being Nat holds S2.(n+1) = S2.n /\ A1.(n+1);
defpred P[object] means S1.$1 = S2.$1;
for n being object holds n in NAT implies P[n]
proof
let n be object;
assume n in NAT;
then reconsider n as Element of NAT;
A8: for k st P[k] holds P[k+1]
proof
let k;
assume S1.k = S2.k;
hence S1.(k+1) = S2.k /\ A1.(k+1) by A5
.= S2.(k+1) by A7;
end;
A9: P[0] by A4,A6;
for k being Nat holds P[k] from NAT_1:sch 2(A9,A8);
then S1.n = S2.n;
hence thesis;
end;
hence thesis;
end;
end;
definition
let X be set, A1 be SetSequence of X;
func Partial_Union A1 -> SetSequence of X means
:Def2:
it.0 = A1.0 & for n being Nat holds it.(n+1) = it.n \/ A1.(n+1);
existence
proof
defpred P[set,set,set] means for x,y being Subset of X,s being Nat holds (s
= $1 & x = $2 & y = $3 implies y = x \/ A1.(s+1));
A1: for n being Nat for x being Subset of X ex y being Subset of
X st P[n,x,y]
proof
let n be Nat;
let x be Subset of X;
take x \/ A1.(n+1);
thus thesis;
end;
consider F being SetSequence of X such that
A2: F.0 = A1.0 and
A3: for n being Nat holds P[n,F.n,F.(n+1)] from RECDEF_1:sch
2(A1 );
take F;
thus F.0 = A1.0 by A2;
let n be Nat;
reconsider n as Element of NAT by ORDINAL1:def 12;
P[n,F.n,F.(n+1)] by A3;
hence thesis;
end;
uniqueness
proof
let S1,S2 be SetSequence of X such that
A4: S1.0 = A1.0 and
A5: for n being Nat holds S1.(n+1) = S1.n \/ A1.(n+1) and
A6: S2.0 = A1.0 and
A7: for n being Nat holds S2.(n+1) = S2.n \/ A1.(n+1);
defpred P[object] means S1.$1 = S2.$1;
for n being object holds n in NAT implies P[n]
proof
let n be object;
assume n in NAT;
then reconsider n as Element of NAT;
A8: for k st P[k] holds P[k+1]
proof
let k;
assume S1.k = S2.k;
hence S1.(k+1) = S2.k \/ A1.(k+1) by A5
.= S2.(k+1) by A7;
end;
A9: P[0] by A4,A6;
for k being Nat holds P[k] from NAT_1:sch 2(A9,A8);
then S1.n = S2.n;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th8:
(Partial_Intersection A1).n c= A1.n
proof
per cases by NAT_1:6;
suppose
n = 0;
hence thesis by Def1;
end;
suppose
ex k being Nat st n = k+1;
then consider k such that
A1: n = k+1;
(Partial_Intersection A1).(k+1) = (Partial_Intersection A1).k /\ A1.(k
+1) by Def1;
hence thesis by A1,XBOOLE_1:17;
end;
end;
theorem Th9:
A1.n c= (Partial_Union A1).n
proof
per cases by NAT_1:6;
suppose
n = 0;
hence thesis by Def2;
end;
suppose
ex k being Nat st n = k+1;
then consider k such that
A1: n = k+1;
(Partial_Union A1).(k+1) = (Partial_Union A1).k \/ A1.(k+1) by Def2;
hence thesis by A1,XBOOLE_1:7;
end;
end;
theorem Th10:
Partial_Intersection A1 is non-ascending
proof
now
let n be Nat;
(Partial_Intersection A1).(n+1) = (Partial_Intersection A1).n /\ A1.(n
+1) by Def1;
hence (Partial_Intersection A1).(n+1) c= (Partial_Intersection A1).n by
XBOOLE_1:17;
end;
hence thesis by PROB_2:6;
end;
theorem Th11:
Partial_Union A1 is non-descending
proof
now
let n be Nat;
(Partial_Union A1).(n+1) = (Partial_Union A1).n \/ A1.(n+1) by Def2;
hence (Partial_Union A1).n c= (Partial_Union A1).(n+1) by XBOOLE_1:7;
end;
hence thesis by PROB_2:7;
end;
theorem Th12:
for x being object holds
x in (Partial_Intersection A1).n iff for k st k <= n holds x in A1.k
proof let x be object;
defpred P[Nat] means (for k st k <= $1 holds x in A1.k) implies x in (
Partial_Intersection A1).$1;
A1: for i st P[i] holds P[i+1]
proof
let i such that
A2: (for k st k <= i holds x in A1.k) implies x in (
Partial_Intersection A1).i;
assume for k st k <= i+1 holds x in A1.k;
then
A3: ( for k st k <= i holds x in A1.k)& x in A1.(i+1) by NAT_1:12;
(Partial_Intersection A1).(i+1) = (Partial_Intersection A1).i /\ A1.(
i+1) by Def1;
hence thesis by A2,A3,XBOOLE_0:def 4;
end;
thus x in (Partial_Intersection A1).n implies for k st k <= n holds x in A1.
k
proof
assume
A4: x in (Partial_Intersection A1).n;
for k st k <= n holds x in A1.k
proof
A5: Partial_Intersection A1 is non-ascending by Th10;
let k such that
A6: k <= n;
A7: (Partial_Intersection A1).k c= A1.k by Th8;
(Partial_Intersection A1).n c= (Partial_Intersection A1).k by A6,A5,
PROB_1:def 4;
then (Partial_Intersection A1).n c= A1.k by A7;
hence thesis by A4;
end;
hence thesis;
end;
A8: P[0]
proof
assume for k st k <= 0 holds x in A1.k;
then x in A1.0;
hence thesis by Def1;
end;
for n holds P[n] from NAT_1:sch 2(A8,A1);
hence thesis;
end;
theorem Th13:
x in (Partial_Union A1).n iff ex k st k <= n & x in A1.k
proof
defpred P[Nat] means (x in (Partial_Union A1).$1 implies ex k st k <= $1 & x
in A1.k);
A1: for i st P[i] holds P[i+1]
proof
let i such that
A2: x in (Partial_Union A1).i implies ex k st k <= i & x in A1.k;
assume
A3: x in (Partial_Union A1).(i+1);
A4: (Partial_Union A1).(i+1) = (Partial_Union A1).i \/ A1.(i+1) by Def2;
now
per cases by A3,A4,XBOOLE_0:def 3;
case
x in (Partial_Union A1).i;
then consider k such that
A5: k <= i & x in A1.k by A2;
take k;
thus thesis by A5,NAT_1:12;
end;
case
x in A1.(i+1);
hence thesis;
end;
end;
hence thesis;
end;
A6: P[0]
proof
assume
A7: x in (Partial_Union A1).0;
take 0;
thus thesis by A7,Def2;
end;
for n holds P[n] from NAT_1:sch 2(A6,A1);
hence x in (Partial_Union A1).n implies ex k st k <= n & x in A1.k;
given i such that
A8: i <= n and
A9: x in A1.i;
A1.i c= (Partial_Union A1).i by Th9;
then
A10: x in (Partial_Union A1).i by A9;
A11: Partial_Union A1 is non-descending by Th11;
(Partial_Union A1).i c= (Partial_Union A1).n by A8,A11,PROB_1:def 5;
hence thesis by A10;
end;
theorem Th14:
Intersection Partial_Intersection A1 = Intersection A1
proof
thus Intersection Partial_Intersection A1 c= Intersection A1
proof
let x be object;
assume
A1: x in Intersection Partial_Intersection A1;
for n be Nat holds x in A1.n
proof
let n be Nat;
x in (Partial_Intersection A1).n by A1,PROB_1:13;
hence thesis by Th12;
end;
hence thesis by PROB_1:13;
end;
let x be object;
assume
A2: x in Intersection A1;
for n be Nat holds x in (Partial_Intersection A1).n
proof
let n be Nat;
for k st k <= n holds x in A1.k
by A2,PROB_1:13;
hence thesis by Th12;
end;
hence thesis by PROB_1:13;
end;
theorem Th15:
Union Partial_Union A1 = Union A1
proof
thus Union Partial_Union A1 c= Union A1
proof
let x be object;
assume x in Union Partial_Union A1;
then consider n being Nat such that
A1: x in (Partial_Union A1).n by PROB_1:12;
consider k such that
k <= n and
A2: x in A1.k by A1,Th13;
thus thesis by A2,PROB_1:12;
end;
let x be object;
assume x in Union A1;
then consider n being Nat such that
A3: x in A1.n by PROB_1:12;
x in (Partial_Union A1).n by A3,Th13;
hence thesis by PROB_1:12;
end;
definition
let X be set, A1 be SetSequence of X;
func Partial_Diff_Union A1 -> SetSequence of X means
:Def3:
it.0 = A1.0 &
for n being Nat holds it.(n+1) = A1.(n+1) \ (Partial_Union A1).n;
existence
proof
defpred P[set,set,set] means for x,y being Subset of X,s being Nat holds (s
= $1 & x = $2 & y = $3 implies y = A1.(s+1) \ (Partial_Union A1).s);
set A = A1.0;
A1: for n being Nat for x being Subset of X ex y being Subset of
X st P[n,x,y]
proof
let n be Nat;
let x be Subset of X;
take A1.(n+1) \ (Partial_Union A1).n;
thus thesis;
end;
consider F being SetSequence of X such that
A2: F.0 = A & for n being Nat holds P[n,F.n,F.(n+1)] from
RECDEF_1:sch 2(A1);
for n holds F.(n+1) = A1.(n+1) \ (Partial_Union A1).n
proof
let n;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
for x,y being Subset of X,s being Nat holds s = n1 & x = F.n1 & y = F.
(n1+1) implies y = A1.(s+1) \ (Partial_Union A1).s by A2;
hence thesis;
end;
hence thesis by A2;
end;
uniqueness
proof
let S1,S2 be SetSequence of X such that
A3: S1.0 = A1.0 and
A4: for n being Nat holds S1.(n+1) = A1.(n+1) \ (Partial_Union A1).n and
A5: S2.0 = A1.0 and
A6: for n being Nat holds S2.(n+1) = A1.(n+1) \ (Partial_Union A1).n;
defpred P[object] means S1.$1 = S2.$1;
for n being object holds n in NAT implies P[n]
proof
let n be object;
assume n in NAT;
then reconsider n as Element of NAT;
A7: for k st P[k] holds P[k+1]
proof
let k;
assume S1.k = S2.k;
thus S1.(k+1) = A1.(k+1) \ (Partial_Union A1).k by A4
.= S2.(k+1) by A6;
end;
A8: P[0] by A3,A5;
for k being Nat holds P[k] from NAT_1:sch 2(A8,A7);
then S1.n = S2.n;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th16:
x in (Partial_Diff_Union A1).n iff x in A1.n & for k st k < n
holds not x in A1.k
proof
thus x in (Partial_Diff_Union A1).n implies x in A1.n & for k st k < n holds
not x in A1.k
proof
assume
A1: x in (Partial_Diff_Union A1).n;
now
per cases by NAT_1:6;
case
n = 0;
hence thesis by A1,Def3;
end;
case
ex n1 being Nat st n = n1 + 1;
then consider n1 being Nat such that
A2: n = n1+1;
A3: x in A1.(n1+1) \ (Partial_Union A1).n1 by A1,A2,Def3;
then
A4: not x in (Partial_Union A1).n1 by XBOOLE_0:def 5;
for k st k < n holds not x in A1.k
proof
let k;
assume k < n;
then k <= n1 by A2,NAT_1:13;
hence thesis by A4,Th13;
end;
hence thesis by A2,A3,XBOOLE_0:def 5;
end;
end;
hence thesis;
end;
assume that
A5: x in A1.n and
A6: for k st k < n holds not x in A1.k;
now
per cases by NAT_1:6;
case
n = 0;
hence thesis by A5,Def3;
end;
case
ex n1 being Nat st n = n1 + 1;
then consider n1 being Nat such that
A7: n = n1+1;
for k st k <= n1 holds not x in A1.k
proof
let k;
assume k <= n1;
then k < n1+1 by NAT_1:13;
hence thesis by A6,A7;
end;
then not x in (Partial_Union A1).n1 by Th13;
then x in A1.(n1+1) \ (Partial_Union A1).n1 by A5,A7,XBOOLE_0:def 5;
hence thesis by A7,Def3;
end;
end;
hence thesis;
end;
theorem Th17:
(Partial_Diff_Union A1).n c= A1.n
by Th16;
theorem Th18:
(Partial_Diff_Union A1).n c= (Partial_Union A1).n
proof
(Partial_Diff_Union A1).n c= A1.n & A1.n c= (Partial_Union A1).n by Th9,Th17;
hence thesis;
end;
theorem Th19:
Partial_Union (Partial_Diff_Union A1) = Partial_Union A1
proof
for n being Nat holds (Partial_Union (Partial_Diff_Union A1))
.n = (Partial_Union A1).n
proof
set A2 = Partial_Diff_Union A1;
defpred P[set] means (Partial_Union A2).$1 = (Partial_Union A1).$1;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A2: (Partial_Union A2).k = (Partial_Union A1).k;
thus (Partial_Union A2).(k+1) = A2.(k+1) \/ (Partial_Union A2).k by Def2
.= (A1.(k+1) \ (Partial_Union A1).k) \/ (Partial_Union A1).k by A2,Def3
.= A1.(k+1) \/ (Partial_Union A1).k by XBOOLE_1:39
.= (Partial_Union A1).(k+1) by Def2;
end;
(Partial_Union (Partial_Diff_Union A1)).0 = A2.0 by Def2
.= A1.0 by Def3
.= (Partial_Union A1).0 by Def2;
then
A3: P[0];
thus for k being Nat holds P[k] from NAT_1:sch 2(A3,A1 );
end;
hence thesis;
end;
theorem Th20:
Union Partial_Diff_Union A1 = Union A1
proof
thus Union Partial_Diff_Union A1 = Union Partial_Union (Partial_Diff_Union
A1) by Th15
.= Union Partial_Union A1 by Th19
.= Union A1 by Th15;
end;
definition
let X,A1;
redefine attr A1 is disjoint_valued means :: redefines disjoint_valued (PROB_2, definition)
for m,n st m <> n holds A1. m misses A1.n;
compatibility
proof
thus A1 is disjoint_valued implies for m,n st m <> n holds A1.m misses A1.
n by PROB_2:def 2;
assume
A1: for m,n st m <> n holds A1.m misses A1.n;
now
let x,y be object;
assume
A2: x <> y;
per cases;
suppose
x in dom A1 & y in dom A1;
hence A1.x misses A1.y by A1,A2;
end;
suppose
not (x in dom A1 & y in dom A1);
then A1.x = {} or A1.y = {} by FUNCT_1:def 2;
hence A1.x misses A1.y;
end;
end;
hence thesis by PROB_2:def 2;
end;
end;
registration let X,A1;
cluster Partial_Diff_Union A1 -> disjoint_valued;
coherence
proof
for m,n st m <> n holds (Partial_Diff_Union A1).n misses (
Partial_Diff_Union A1).m
proof
let m,n such that
A1: m <> n;
assume (Partial_Diff_Union A1).n meets (Partial_Diff_Union A1).m;
then consider x being object such that
A2: x in (Partial_Diff_Union A1).n and
A3: x in (Partial_Diff_Union A1).m by XBOOLE_0:3;
per cases by A1,XXREAL_0:1;
suppose
m < n;
then not x in A1.m by A2,Th16;
hence contradiction by A3,Th16;
end;
suppose
n < m;
then not x in A1.n by A3,Th16;
hence contradiction by A2,Th16;
end;
end;
hence thesis;
end;
end;
registration
let X be set, Si be SigmaField of X, XSeq be SetSequence of Si;
cluster Partial_Intersection XSeq -> Si-valued;
coherence
proof
defpred P[set] means (Partial_Intersection XSeq).$1 in Si;
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A2: (Partial_Intersection XSeq).k in Si;
(Partial_Intersection XSeq).k /\ XSeq.(k+1) is Event of Si by A2,
PROB_1:19;
then (Partial_Intersection XSeq).k /\ XSeq.(k+1) in Si;
hence thesis by Def1;
end;
XSeq.0 in rng XSeq & (Partial_Intersection XSeq).0 = XSeq.0 by Def1,
NAT_1:51;
then
A3: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A3,A1);
then rng Partial_Intersection XSeq c= Si by NAT_1:52;
hence thesis;
end;
end;
registration
let X be set, Si be SigmaField of X, XSeq be SetSequence of Si;
cluster Partial_Union XSeq -> Si-valued;
coherence
proof
defpred P[set] means (Partial_Union XSeq).$1 in Si;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A2: (Partial_Union XSeq).k in Si;
(Partial_Union XSeq).k \/ XSeq.(k+1) is Event of Si by A2,PROB_1:21;
then (Partial_Union XSeq).k \/ XSeq.(k+1) in Si;
hence thesis by Def2;
end;
XSeq.0 in rng XSeq & (Partial_Union XSeq).0 = XSeq.0 by Def2,NAT_1:51;
then
A3: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A3,A1);
then rng Partial_Union XSeq c= Si by NAT_1:52;
hence thesis;
end;
end;
registration
let X be set, Si be SigmaField of X, XSeq be SetSequence of Si;
cluster Partial_Diff_Union XSeq -> Si-valued;
coherence
proof
A1: XSeq.0 in rng XSeq & (Partial_Diff_Union XSeq).0 = XSeq.0 by Def3,NAT_1:51;
for m being Nat holds (Partial_Diff_Union XSeq).m in Si
proof
let m be Nat;
now
per cases by NAT_1:6;
case
m = 0;
hence thesis by A1;
end;
case
ex k being Nat st m = k+1;
then consider k being Nat such that
A2: m = k+1;
reconsider k as Element of NAT by ORDINAL1:def 12;
XSeq.(k+1) \ (Partial_Union XSeq).k in Si;
hence thesis by A2,Def3;
end;
end;
hence thesis;
end;
then rng Partial_Diff_Union XSeq c= Si by NAT_1:52;
hence thesis;
end;
end;
theorem
YSeq = Partial_Intersection XSeq implies YSeq.0 = XSeq.0 & for n
holds YSeq.(n+1) = YSeq.n /\ XSeq.(n+1) by Def1;
theorem
YSeq = Partial_Union XSeq implies YSeq.0 = XSeq.0 & for n holds YSeq.
(n+1) = YSeq.n \/ XSeq.(n+1) by Def2;
theorem
(Partial_Intersection XSeq).n c= XSeq.n by Th8;
theorem
XSeq.n c= (Partial_Union XSeq).n by Th9;
theorem
for x being object holds
x in (Partial_Intersection XSeq).n iff
for k st k <= n holds x in XSeq.k
proof reconsider XSeq as SetSequence of X;
let x be object;
x in (Partial_Intersection XSeq).n iff
for k st k <= n holds x in XSeq.k by Th12;
hence thesis;
end;
theorem
x in (Partial_Union XSeq).n iff ex k st k <= n & x in XSeq.k
proof reconsider XSeq as SetSequence of X;
x in (Partial_Union XSeq).n iff ex k st k <= n & x in XSeq.k by Th13;
hence thesis;
end;
theorem
Partial_Intersection XSeq is non-ascending by Th10;
theorem
Partial_Union XSeq is non-descending by Th11;
theorem
Intersection Partial_Intersection XSeq = Intersection XSeq by Th14;
theorem
Union Partial_Union XSeq = Union XSeq by Th15;
theorem
YSeq = Partial_Diff_Union XSeq implies YSeq.0 = XSeq.0 & for n holds
YSeq.(n+1) = XSeq.(n+1) \ (Partial_Union XSeq).n by Def3;
theorem
x in (Partial_Diff_Union XSeq).n iff x in XSeq.n & for k st k < n
holds not x in XSeq.k
proof reconsider XSeq as SetSequence of X;
x in (Partial_Diff_Union XSeq).n iff x in XSeq.n & for k st k < n
holds not x in XSeq.k by Th16;
hence thesis;
end;
theorem
(Partial_Diff_Union XSeq).n c= XSeq.n by Th17;
theorem
(Partial_Diff_Union XSeq).n c= (Partial_Union XSeq).n by Th18;
theorem
Partial_Union (Partial_Diff_Union XSeq) = Partial_Union XSeq by Th19;
theorem
Union Partial_Diff_Union XSeq = Union XSeq by Th20;
theorem Th37:
(P * Partial_Union ASeq) is non-decreasing
proof
Partial_Union ASeq is non-descending by Th11;
hence thesis by Th6;
end;
theorem
(P * Partial_Intersection ASeq) is non-increasing
proof
Partial_Intersection ASeq is non-ascending by Th10;
hence thesis by Th7;
end;
theorem
Partial_Sums(P * ASeq) is non-decreasing
proof
for n being Nat holds (P * ASeq).n >= 0 by Th4;
hence thesis by SERIES_1:16;
end;
theorem Th40:
(P * Partial_Union ASeq).0 = Partial_Sums(P * ASeq).0
proof
A1: dom (P * ASeq) = NAT by SEQ_1:1;
dom (P * Partial_Union ASeq) = NAT by SEQ_1:1;
then
A2: (P * Partial_Union ASeq).0 = P.((Partial_Union ASeq).0) by FUNCT_1:12
.= P.(ASeq.0) by Def2;
Partial_Sums(P * ASeq).0 = (P * ASeq).0 by SERIES_1:def 1
.= P.(ASeq.0) by A1,FUNCT_1:12;
hence thesis by A2;
end;
theorem Th41:
P * Partial_Union ASeq is convergent & lim (P * Partial_Union
ASeq) = upper_bound (P * Partial_Union ASeq) & lim (P * Partial_Union ASeq)
= P.Union
ASeq
proof
A1: P * Partial_Union ASeq is non-decreasing by Th37;
A2: Partial_Union ASeq is non-descending by Th11;
then P * Partial_Union ASeq is convergent by PROB_2:10;
then
A3: P * Partial_Union ASeq is bounded;
lim (P * Partial_Union ASeq) = P.Union (Partial_Union ASeq) by A2,PROB_2:10
.= P.Union ASeq by Th15;
hence thesis by A2,A3,A1,PROB_2:10,RINFSUP1:24;
end;
theorem Th42:
ASeq is disjoint_valued implies for n,m st n < m holds (
Partial_Union ASeq).n misses ASeq.m
proof
assume
A1: ASeq is disjoint_valued;
let n,m such that
A2: n < m;
assume (Partial_Union ASeq).n meets ASeq.m;
then consider x being object such that
A3: x in (Partial_Union ASeq).n and
A4: x in ASeq.m by XBOOLE_0:3;
reconsider ASeq as SetSequence of Omega;
consider k being Nat such that
A5: k <= n and
A6: x in ASeq.k by A3,Th13;
ASeq.k misses ASeq.m by A1,A2,A5;
then ASeq.k /\ ASeq.m = {};
hence contradiction by A4,A6,XBOOLE_0:def 4;
end;
theorem Th43:
ASeq is disjoint_valued implies (P * Partial_Union ASeq).n =
Partial_Sums(P * ASeq).n
proof
A1: dom (P * ASeq) = NAT by SEQ_1:1;
defpred P[Nat] means (P * Partial_Union ASeq).$1 = Partial_Sums(P * ASeq).
$1;
A2: dom (P * Partial_Union ASeq) = NAT by SEQ_1:1;
assume
A3: ASeq is disjoint_valued;
A4: for k st P[k] holds P[k+1]
proof
let k such that
A5: (P * Partial_Union ASeq).k = Partial_Sums(P * ASeq).k;
k < k+1 by NAT_1:13;
then
A6: (Partial_Union ASeq).k misses ASeq.(k+1) by A3,Th42;
reconsider k as Element of NAT by ORDINAL1:def 12;
A7: Partial_Sums(P * ASeq).(k+1) =Partial_Sums(P * ASeq).k + (P * ASeq).(
k+1) by SERIES_1:def 1
.=Partial_Sums(P * ASeq).k + P.(ASeq.(k+1)) by A1,FUNCT_1:12;
(P * Partial_Union ASeq).(k+1) = P.((Partial_Union ASeq).(k+1)) by A2,
FUNCT_1:12
.= P.((Partial_Union ASeq).k \/ ASeq.(k+1)) by Def2
.= P.((Partial_Union ASeq).k) + P.(ASeq.(k+1)) by A6,PROB_1:def 8
.= (P * Partial_Union ASeq).k + P.(ASeq.(k+1)) by A2,FUNCT_1:12;
hence thesis by A5,A7;
end;
A8: P[0] by Th40;
for k holds P[k] from NAT_1:sch 2(A8,A4);
hence thesis;
end;
theorem Th44:
ASeq is disjoint_valued implies (P * Partial_Union ASeq) =
Partial_Sums(P * ASeq)
by Th43;
theorem Th45:
ASeq is disjoint_valued implies Partial_Sums(P * ASeq) is
convergent & lim Partial_Sums(P * ASeq) = upper_bound Partial_Sums(P * ASeq)
& lim
Partial_Sums(P * ASeq) = P.Union ASeq
proof
assume ASeq is disjoint_valued;
then (P * Partial_Union ASeq) = Partial_Sums(P * ASeq) by Th44;
hence thesis by Th41;
end;
theorem Th46:
ASeq is disjoint_valued implies P.(Union ASeq) = Sum(P * ASeq)
proof
assume ASeq is disjoint_valued;
then lim Partial_Sums(P * ASeq) = P.Union ASeq by Th45;
hence thesis by SERIES_1:def 3;
end;
definition
let X,F1,n;
redefine func F1.n -> Subset of X; :: redefines . (FUNCT_1, definition)
coherence
proof
per cases;
suppose
n in dom F1;
hence thesis by FINSEQ_2:11;
end;
suppose
not n in dom F1;
then F1.n = {} by FUNCT_1:def 2;
hence thesis by SUBSET_1:1;
end;
end;
end;
theorem
ex F1 being FinSequence of bool X st for k st k in dom F1 holds F1.k = X
proof
now
let n be Element of NAT;
set F1 = n |-> X;
A1: dom F1 = Seg n by FUNCOP_1:13;
rng F1 c= bool X
proof
let x be object;
assume x in rng F1;
then ex i be Nat st i in dom F1 & F1.i = x by FINSEQ_2:10;
then x = X by A1,FINSEQ_2:57;
hence thesis by ZFMISC_1:def 1;
end;
then
A2: F1 is FinSequence of bool X by FINSEQ_1:def 4;
for k being Nat st k in dom F1 holds F1.k = X by A1,FINSEQ_2:57;
hence thesis by A2;
end;
hence thesis;
end;
theorem
for F1 being FinSequence of bool X holds union rng F1 is Subset of X;
definition
let X be set, F1 be FinSequence of bool X;
redefine func Union F1 -> Subset of X; :: redefines Union (CARD_3, definition)
coherence
proof
Union F1 = union rng F1 by CARD_3:def 4;
hence thesis;
end;
end;
theorem Th49:
x in Union F1 iff ex k st k in dom F1 & x in F1.k
proof
set Y = union rng F1;
A1: for x holds x in Y iff ex k st k in dom F1 & x in F1.k
proof
let x;
thus x in Y implies ex k st k in dom F1 & x in F1.k
proof
assume x in Y;
then consider Z such that
A2: x in Z and
A3: Z in rng F1 by TARSKI:def 4;
ex i being Nat st i in dom F1 & Z = F1.i by A3,FINSEQ_2:10;
hence thesis by A2;
end;
thus (ex k st k in dom F1 & x in F1.k) implies x in Y
proof
given i such that
A4: i in dom F1 and
A5: x in F1.i;
F1.i in rng F1 by A4,FUNCT_1:def 3;
hence thesis by A5,TARSKI:def 4;
end;
end;
Y = Union F1 by CARD_3:def 4;
hence thesis by A1;
end;
definition
let X, F1;
func Complement F1 -> FinSequence of bool X means
:Def5:
len it = len F1 & for n st n in dom it holds it.n = (F1.n)`;
existence
proof
deffunc F(Nat) = (F1.$1)`;
consider f being FinSequence of bool X such that
A1: len f = len F1 & for n being Nat st n in dom f holds f.n = F(n)
from FINSEQ_2:sch 1;
take f;
thus thesis by A1;
end;
uniqueness
proof
let F2,F3 be FinSequence of bool X such that
A2: len F2 = len F1 and
A3: for n st n in dom F2 holds F2.n = (F1.n)` and
A4: len F3 = len F1 and
A5: for n st n in dom F3 holds F3.n = (F1.n)`;
dom F2 = dom F3 & for k being Nat st k in dom F2 holds F2.k = F3.k
proof
thus
A6: dom F2 = Seg len F3 by A2,A4,FINSEQ_1:def 3
.= dom F3 by FINSEQ_1:def 3;
let k be Nat;
assume
A7: k in dom F2;
hence F2.k = (F1.k)` by A3
.= F3.k by A5,A6,A7;
end;
hence thesis by FINSEQ_1:13;
end;
end;
definition
let X, F1;
func Intersection F1 -> Subset of X equals
:Def6:
(Union Complement F1)` if
F1 <> {} otherwise {};
coherence by SUBSET_1:1;
consistency;
end;
theorem Th50:
dom Complement F1 = dom F1
proof
thus dom Complement F1 = Seg len Complement F1 by FINSEQ_1:def 3
.= Seg len F1 by Def5
.= dom F1 by FINSEQ_1:def 3;
end;
theorem Th51:
for x being object holds
F1 <> {} implies (x in Intersection F1 iff for k st k in dom F1
holds x in F1.k )
proof let x be object;
A1: for n st n in dom F1 holds X \ (Complement F1).n = F1.n
proof
let n;
assume n in dom F1;
then
A2: n in dom Complement F1 by Th50;
X \ (Complement F1).n = ((Complement F1).n)` by SUBSET_1:def 4
.= ((F1.n)`)` by A2,Def5
.= F1.n;
hence thesis;
end;
assume
A3: F1 <> {};
then
A4: dom F1 <> {} by RELAT_1:41;
A5: x in X & (for n st n in dom F1 holds not x in (Complement F1).n) iff
for n st n in dom F1 holds x in F1.n
proof
hereby
assume that
A6: x in X and
A7: for n st n in dom F1 holds not x in (Complement F1).n;
let n such that
A8: n in dom F1;
not x in (Complement F1).n by A7,A8;
then x in X \ (Complement F1).n by A6,XBOOLE_0:def 5;
hence x in F1.n by A1,A8;
end;
assume
A9: for n st n in dom F1 holds x in F1.n;
A10: now
let n be Element of NAT such that
A11: n in dom F1;
x in F1.n by A9,A11;
then x in X \ (Complement F1).n by A1,A11;
hence x in X & not x in (Complement F1).n by XBOOLE_0:def 5;
end;
ex a being object st a in dom F1 by A4,XBOOLE_0:def 1;
hence thesis by A10;
end;
dom Complement F1 = dom F1 by Th50;
then
A12: x in X & (not x in Union (Complement F1)) iff x in X & for n st n in
dom F1 holds not x in (Complement F1).n by Th49;
x in (Union Complement F1)` iff x in X \ Union Complement F1 by
SUBSET_1:def 4;
hence thesis by A3,A12,A5,Def6,XBOOLE_0:def 5;
end;
theorem Th52:
F1 <> {} implies (x in meet rng F1 iff for n st n in dom F1 holds x in F1.n)
proof
assume F1 <> {};
then
A1: rng F1 <> {} by RELAT_1:41;
A2: now
let x;
assume
A3: for n st n in dom F1 holds x in F1.n;
now
let Y;
assume Y in rng F1;
then consider n be object such that
A4: n in dom F1 and
A5: Y = F1.n by FUNCT_1:def 3;
thus x in Y by A3,A4,A5;
end;
hence x in meet rng F1 by A1,SETFAM_1:def 1;
end;
now
let x;
assume
A6: x in meet rng F1;
now
let k;
assume k in dom F1;
then F1.k in rng F1 by FUNCT_1:3;
hence x in F1.k by A6,SETFAM_1:def 1;
end;
hence for n st n in dom F1 holds x in F1.n;
end;
hence thesis by A2;
end;
theorem
Intersection F1 = meet rng F1
proof
per cases;
suppose
A1: F1 <> {};
now
let x be object;
x in Intersection F1 iff for n st n in dom F1 holds x in F1.n by A1,Th51;
hence x in Intersection F1 iff x in meet rng F1 by A1,Th52;
end;
hence thesis by TARSKI:2;
end;
suppose
F1 = {};
hence thesis by Def6,RELAT_1:38,SETFAM_1:1;
end;
end;
theorem Th54:
for F1 being FinSequence of bool X holds ex A1 being SetSequence
of X st (for k st k in dom F1 holds A1.k = F1.k) & for k st not k in dom F1
holds A1.k = {}
proof
deffunc G(object) = {};
let F1 be FinSequence of bool X;
defpred P[object] means $1 in dom F1;
deffunc F(object) = F1.$1;
ex f being Function st dom f = NAT &
for k being object st k in NAT holds (
P[k] implies f.k=F(k)) & (not P[k] implies f.k=G(k)) from PARTFUN1:sch 1;
then consider f being Function such that
A1: dom f = NAT and
A2: for x being object st x in NAT
holds (x in dom F1 implies f.x = F1.x) & (not x in
dom F1 implies f.x = {});
A3: for x st x in dom F1 holds F1.x in bool X
proof
let x;
assume x in dom F1;
then F1.x in rng F1 by FUNCT_1:3;
hence thesis;
end;
for x st x in NAT holds f.x in bool X
proof
let x;
assume
A4: x in NAT;
per cases;
suppose
not x in dom F1;
then f.x = {} by A2,A4;
then f.x c= X;
hence thesis;
end;
suppose
A5: x in dom F1;
then f.x = F1.x by A2;
hence thesis by A3,A5;
end;
end;
then reconsider f as SetSequence of X by A1,FUNCT_2:3;
take f;
thus for k st k in dom F1 holds f.k = F1.k by A2;
let k;
k in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
theorem Th55:
for F1 being FinSequence of bool X for A1 being SetSequence of X
st (for k st k in dom F1 holds A1.k = F1.k) &
(for k st not k in dom F1 holds A1.k = {})
holds A1.0={} & Union A1 = Union F1
proof
let F1 be FinSequence of bool X;
let A1 be SetSequence of X such that
A1: for k st k in dom F1 holds A1.k = F1.k and
A2: for k st not k in dom F1 holds A1.k = {};
thus A1.0 = {} by A2,Th1;
thus Union A1 = Union F1
proof
thus Union A1 c= Union F1
proof
let x be object;
assume x in Union A1;
then consider n being Nat such that
A3: x in A1.n by PROB_1:12;
n in dom F1 & x in F1.n by A1,A2,A3;
hence thesis by Th49;
end;
let x be object;
assume x in Union F1;
then consider n such that
A4: n in dom F1 & x in F1.n by Th49;
n in NAT & x in A1.n by A1,A4;
hence thesis by PROB_1:12;
end;
end;
definition :: czy wystarczy rejestracja?
let X be set, Si be SigmaField of X;
redefine mode FinSequence of Si -> FinSequence of bool X; :: redefines FinSequence (FINSEQ_1, definition)
coherence
proof let f be FinSequence of Si;
thus rng f c= bool X by XBOOLE_1:1;
end;
end;
definition
let X be set, Si be SigmaField of X, FSi be FinSequence of Si,n;
redefine func FSi.n -> Event of Si; :: redefines . (FUNCT_1, definition)
coherence
proof
per cases;
suppose
n in dom FSi;
hence thesis by FINSEQ_2:11;
end;
suppose
not n in dom FSi;
then FSi.n = {} by FUNCT_1:def 2;
hence thesis by PROB_1:22;
end;
end;
end;
theorem Th56:
for FSi being FinSequence of Si holds ex ASeq being SetSequence
of Si st (for k st k in dom FSi holds ASeq.k = FSi.k) & for k st not k in dom
FSi holds ASeq.k = {}
proof
let FSi be FinSequence of Si;
consider A1 being SetSequence of X such that
A1: for k st k in dom FSi holds A1.k = FSi.k and
A2: for k st not k in dom FSi holds A1.k = {} by Th54;
for n being Nat holds A1.n in Si
proof
let n be Nat;
per cases;
suppose
not n in dom FSi;
then A1.n = {} by A2;
hence thesis by PROB_1:4;
end;
suppose
n in dom FSi;
then A1.n = FSi.n by A1;
hence thesis;
end;
end;
then rng A1 c= Si by NAT_1:52;
then reconsider A1 as SetSequence of Si by RELAT_1:def 19;
take A1;
thus thesis by A1,A2;
end;
theorem Th57:
for FSi being FinSequence of Si holds Union FSi in Si
proof
let FSi be FinSequence of Si;
consider ASeq being SetSequence of Si such that
A1: ( for k st k in dom FSi holds ASeq.k = FSi.k)&
for k st not k in dom FSi holds ASeq.k = {} by Th56;
reconsider ASeq as SetSequence of X;
( for k st k in dom FSi holds ASeq.k = FSi.k)&
for k st not k in dom FSi holds ASeq.k = {} by A1;
then Union ASeq = Union FSi by Th55;
hence thesis by PROB_1:17;
end;
registration
let X be set, S be SigmaField of X, F being FinSequence of S;
cluster Complement F -> S-valued;
coherence
proof set G = Complement F;
let x be object;
assume x in rng G;
then consider y being object such that
A1: y in dom G and
A2: x = G.y by FUNCT_1:def 3;
reconsider y as Nat by A1;
G.y = (F.y)` by A1,Def5;
then G.y is Event of S by PROB_1:20;
hence x in S by A2;
end;
end;
theorem
for FSi being FinSequence of Si holds Intersection FSi in Si
proof
let FSi be FinSequence of Si;
per cases;
suppose
FSi = {};
then Intersection FSi = {} by Def6;
hence thesis by PROB_1:4;
end;
suppose
A1: FSi <> {};
rng Complement FSi c= Si;
then reconsider C = Complement FSi as FinSequence of Si by FINSEQ_1:def 4;
A2: Union C in Si by Th57;
Intersection FSi = (Union Complement FSi)` by A1,Def6;
hence thesis by A2,PROB_1:def 1;
end;
end;
reserve FSeq for FinSequence of Sigma;
theorem Th59:
dom(P * FSeq) = dom FSeq
proof
for x being object holds x in dom (P * FSeq) iff x in dom FSeq
proof
let x be object;
thus x in dom (P * FSeq) implies x in dom FSeq by FUNCT_1:11;
assume
A1: x in dom FSeq;
then reconsider k=x as Element of NAT;
FSeq.k in Sigma;
then FSeq.k in dom P by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:11;
end;
hence thesis by TARSKI:2;
end;
theorem Th60:
P * FSeq is FinSequence of REAL
proof
dom (P * FSeq) = dom FSeq by Th59;
then ex n being Nat st dom (P * FSeq) = Seg n by FINSEQ_1:def 2;
then reconsider RSeq = P * FSeq as FinSequence by FINSEQ_1:def 2;
rng (P * FSeq) c= REAL;
then rng RSeq c= REAL;
hence thesis by FINSEQ_1:def 4;
end;
definition
let Omega,Sigma,FSeq,P;
redefine func P * FSeq -> FinSequence of REAL; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence by Th60;
end;
theorem Th61:
len (P * FSeq) = len FSeq
proof
dom(P * FSeq) = dom FSeq by Th59;
then Seg len (P * FSeq) = dom FSeq by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th62:
len RFin = 0 implies Sum RFin = 0
proof
assume
A1: len RFin=0;
0 in REAL by XREAL_0:def 1;
then
A2: addreal is having_a_unity by RVSUM_1:1,SETWISEO:def 2;
reconsider RFin as FinSequence of REAL by FINSEQ_1:106;
Sum(RFin) = addreal $$ RFin by RVSUM_1:def 12
.= 0 by A1,A2,BINOP_2:2,FINSOP_1:def 1;
hence thesis;
end;
theorem Th63:
len RFin >= 1 implies ex f being Real_Sequence st f.1 = RFin.1 &
(for n st 0 <> n & n < len RFin holds f.(n+1) = f.n+RFin.(n+1)) &
Sum(RFin) = f.(len RFin)
proof
assume
A0: len RFin >= 1;
reconsider RFin as FinSequence of REAL by FINSEQ_1:106;
consider f be sequence of REAL such that
A1: f.1 = RFin.1 and
A2: for n being Nat st 0 <> n & n < len RFin holds f.(n+1) =
addreal.(f.n,RFin.(n+1)) and
A3: addreal "**" RFin = f.(len RFin) by A0,FINSOP_1:1;
take f;
for n st 0 <> n & n < len RFin holds f.(n+1) = f.n+ RFin.(n+1)
proof
let n;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
assume that
A4: 0 <> n and
A5: n < len RFin;
thus f.(n+1) = addreal.(f.n1,RFin.(n1+1)) by A2,A4,A5
.= f.n+ RFin.(n+1) by BINOP_2:def 9;
end;
hence thesis by A1,A3,RVSUM_1:def 12;
end;
theorem Th64:
for FSeq being FinSequence of Sigma, ASeq being SetSequence of
Sigma st (for k st k in dom FSeq holds ASeq.k = FSeq.k) & (for k st not k in
dom FSeq holds ASeq.k = {}) holds Partial_Sums(P * ASeq) is convergent & Sum(P
* ASeq) = Partial_Sums(P * ASeq).(len FSeq) & P.(Union ASeq) <= Sum(P * ASeq) &
Sum(P * FSeq) = Sum(P * ASeq)
proof
let FSeq be FinSequence of Sigma, ASeq be SetSequence of Sigma such that
A1: for k st k in dom FSeq holds ASeq.k = FSeq.k and
A2: for k st not k in dom FSeq holds ASeq.k = {};
reconsider XSeq = ASeq as SetSequence of Omega;
(for k st k in dom FSeq holds XSeq.k = FSeq.k) &
for k st not k in dom FSeq holds XSeq.k = {} by A1,A2;
then
A3: ASeq.0 ={} by Th55;
A4: (P * ASeq).0 = P.(ASeq.0) by FUNCT_2:15
.= 0 by A3,VALUED_0:def 19;
A5: for k st k in dom FSeq holds (P * ASeq).k = (P * FSeq).k
proof
let k such that
A6: k in dom FSeq;
k in NAT by ORDINAL1:def 12;
hence (P * ASeq).k = P.(ASeq.k) by FUNCT_2:15
.= P.(FSeq.k) by A1,A6
.= (P * FSeq).k by A6,FUNCT_1:13;
end;
1 = 0+1;
then
A7: Partial_Sums(P * ASeq).1 = Partial_Sums(P * ASeq).0 + (P*ASeq).1 by
SERIES_1:def 1
.= (P*ASeq).0 + (P*ASeq).1 by SERIES_1:def 1
.= (P * ASeq).1 by A4;
A8: len FSeq >= 1 implies Partial_Sums(P * ASeq).1=(P * FSeq).1 & for m st
m <> 0 & m < len FSeq holds Partial_Sums(P*ASeq).(m+1)=Partial_Sums(P*ASeq).m+(
P*FSeq).(m+1)
proof
assume len FSeq >= 1;
then 1 in dom FSeq by Th2;
hence Partial_Sums(P * ASeq).1 = (P * FSeq).1 by A5,A7;
thus for m st m <> 0 & m < len FSeq holds Partial_Sums(P*ASeq).(m+1)=
Partial_Sums(P*ASeq).m+(P*FSeq).(m+1)
proof
let m;
assume that
m <> 0 and
A9: m < len FSeq;
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
m+1 in Seg len FSeq by A9,FINSEQ_3:11;
then
A10: m+1 in dom FSeq by FINSEQ_1:def 3;
thus Partial_Sums(P*ASeq).(m+1) = Partial_Sums(P*ASeq).m1+(P*ASeq).(m1+1
) by SERIES_1:def 1
.= Partial_Sums(P*ASeq).m+(P*FSeq).(m+1) by A5,A10;
end;
end;
defpred P[Nat] means Partial_Sums(P * ASeq).((len FSeq + 1) + $1) =
Partial_Sums(P * ASeq).(len FSeq);
A11: for m being Nat holds (P * ASeq).((len FSeq + 1) + m)=0
proof
set k=len FSeq + 1;
let m be Nat;
reconsider m1=m as Element of NAT by ORDINAL1:def 12;
k + m >= k by NAT_1:11;
then len FSeq + 1 + m > len FSeq by Lm1;
then not len FSeq + 1 + m in dom FSeq by FINSEQ_3:25;
then
A12: ASeq.((len FSeq + 1) + m) = {} by A2;
thus (P * ASeq).((len FSeq + 1) + m) = P.(ASeq.((len FSeq + 1) + m1)) by
FUNCT_2:15
.= 0 by A12,VALUED_0:def 19;
end;
A13: for k st P[k] holds P[k+1]
proof
let k such that
A14: Partial_Sums(P * ASeq).((len FSeq + 1) + k) = Partial_Sums(P *
ASeq).(len FSeq);
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
Partial_Sums(P * ASeq).((len FSeq + 1 + k)+1) = Partial_Sums(P * ASeq
).(len FSeq + 1 + k1) + (P * ASeq).((len FSeq + 1) + (k1+1)) by SERIES_1:def 1
.= Partial_Sums(P * ASeq).(len FSeq + 1 + k) + 0 by A11;
hence thesis by A14;
end;
now
let n be Nat;
(Partial_Diff_Union ASeq).n c= ASeq.n by Th17;
hence (P * Partial_Diff_Union ASeq).n <= (P * ASeq).n by Th5;
end;
then
A15: for n being Nat holds (Partial_Sums(P * Partial_Diff_Union
ASeq)).n <= (Partial_Sums(P * ASeq)).n by SERIES_1:14;
A16: Partial_Sums(P * Partial_Diff_Union ASeq) is convergent by Th45;
Partial_Sums(P * ASeq).((len FSeq + 1) + 0) = Partial_Sums(P * ASeq).(
len FSeq) + (P * ASeq).((len FSeq + 1) + 0) by SERIES_1:def 1
.= Partial_Sums(P * ASeq).(len FSeq) + 0 by A11;
then
A17: P[0];
A18: for k holds P[k] from NAT_1:sch 2(A17,A13);
A19: for m st len FSeq + 1 <= m holds Partial_Sums(P * ASeq).m =
Partial_Sums(P * ASeq).(len FSeq)
proof
let m;
assume len FSeq + 1 <= m;
then ex k being Nat st m = (len FSeq + 1) + k by NAT_1:10;
hence thesis by A18;
end;
then
A20: lim Partial_Sums(P * ASeq) = Partial_Sums(P * ASeq).(len FSeq) by Th3;
then
A21: Sum(P * ASeq) = Partial_Sums(P * ASeq).(len FSeq) by SERIES_1:def 3;
A22: Sum(P * FSeq) = Sum(P * ASeq)
proof
now
per cases;
suppose
len FSeq = 0;
then len (P * FSeq) = 0 & Sum(P * ASeq) = 0 by A4,A21,Th61,
SERIES_1:def 1;
hence thesis by Th62;
end;
suppose
A23: len FSeq <> 0;
then 1 <= len FSeq by NAT_1:14;
then
A24: 1 <= len (P * FSeq) by Th61;
then consider seq1 being Real_Sequence such that
A25: seq1.1 = (P * FSeq).1 and
A26: for n st 0 <> n & n < len (P * FSeq) holds seq1.(n+1) = seq1.
n+(P * FSeq).(n+1) and
A27: Sum(P * FSeq) = seq1.(len (P * FSeq)) by Th63;
defpred P[object,object] means
ex n st (n=$1 & (n = 0 implies $2=0) & (n <>
0 & n <= len (P * FSeq) implies $2=seq1.n) & (n <> 0 & n > len (P * FSeq)
implies $2=Partial_Sums(P*ASeq).(len(P * FSeq))));
ex seq being Real_Sequence st for n holds (n=0 implies seq.n=0) &
(n<>0 & n <= len (P * FSeq) implies seq.n=seq1.n) & (n<>0 & n > len (P * FSeq)
implies seq.n=Partial_Sums(P*ASeq).(len (P * FSeq)))
proof
A28: for x being object st x in NAT ex y being object st P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider n=x as Element of NAT;
now
per cases;
case
n=0;
hence P[x,0];
end;
case
n <> 0 & n <= len (P * FSeq);
hence P[x,(seq1.n)];
end;
case
n <> 0 & not n <= len (P * FSeq);
hence P[x,Partial_Sums(P*ASeq).(len(P * FSeq))];
end;
end;
hence thesis;
end;
consider f being Function such that
A29: dom f=NAT & for x being object st x in NAT holds P[x,f.x]
from CLASSES1:
sch 1(A28);
now
let x;
assume x in NAT;
then
ex n st n=x & (n = 0 implies f.x=0) & (n <> 0 & n <= len (P *
FSeq) implies f.x=seq1.n) & (n <> 0 & n > len (P * FSeq) implies f.x=
Partial_Sums(P*ASeq).(len(P * FSeq))) by A29;
hence f.x is real;
end;
then reconsider f as Real_Sequence by A29,SEQ_1:1;
take seq=f;
let n;
n in NAT by ORDINAL1:def 12;
then ex k st k=n & (k=0 implies seq.n=0) & (k<>0 & k <= len (P *
FSeq) implies seq.n=seq1.k) & (k<>0 & k > len (P * FSeq) implies seq.n=
Partial_Sums(P*ASeq).(len (P * FSeq))) by A29;
hence thesis;
end;
then consider seq2 being Real_Sequence such that
A30: for n holds (n=0 implies seq2.n=0) & (n<>0 & n <= len (P *
FSeq) implies seq2.n=seq1.n) & (n<>0 & n > len (P * FSeq) implies seq2.n=
Partial_Sums(P*ASeq).(len (P * FSeq)));
defpred P[Nat] means seq2.$1 = Partial_Sums(P * ASeq).$1;
A31: for k st P[k] holds P[k+1]
proof
let k such that
A32: P[k];
now
per cases;
case
k = 0;
thus seq2.1 = Partial_Sums(P * ASeq).1 by A8,A23,A24,A25,A30,
NAT_1:14;
end;
case
A33: k <> 0 & k <= len (P * FSeq) -1;
then
A34: k + 0 < (len (P * FSeq) - 1) + 1 by XREAL_1:8;
then
A35: k < len FSeq by Th61;
k+1 <= len (P * FSeq) -1 +1 by A33,XREAL_1:7;
hence seq2.(k+1) = seq1.(k+1) by A30
.= seq1.k + (P * FSeq).(k+1) by A26,A33,A34
.= Partial_Sums(P * ASeq).k + (P * FSeq).(k+1) by A30,A32,A33
,A34
.= Partial_Sums(P * ASeq).(k+1) by A8,A33,A35,NAT_1:14;
end;
case
k <> 0 & not k <= len (P * FSeq) - 1;
then
A36: k+1 > len (P * FSeq) - 1 + 1 by XREAL_1:8;
then k+1 >= len (P * FSeq) + 1 by NAT_1:13;
then consider i being Nat such that
A37: k+1 = len (P * FSeq) + 1 + i by NAT_1:10;
thus seq2.(k+1) = Partial_Sums(P * ASeq).(len (P * FSeq)) by A30
,A36
.= Partial_Sums(P * ASeq).(len FSeq) by Th61
.= Partial_Sums(P * ASeq).((len FSeq + 1) + i) by A18
.= Partial_Sums(P * ASeq).(k+1) by A37,Th61;
end;
end;
hence thesis;
end;
seq2.0 = (P * ASeq).0 by A4,A30
.= Partial_Sums(P * ASeq).0 by SERIES_1:def 1;
then
A38: P[0];
A39: for k holds P[k] from NAT_1:sch 2(A38,A31);
len (P * FSeq) <> 0 by A23,Th61;
then seq2.(len (P * FSeq)) = Sum(P * FSeq) by A27,A30;
hence Sum(P * FSeq) = Partial_Sums(P * ASeq).(len (P * FSeq)) by A39
.= Sum(P * ASeq) by A21,Th61;
end;
end;
hence thesis;
end;
Partial_Sums(P * ASeq) is convergent by A19,Th3;
then lim Partial_Sums(P * Partial_Diff_Union ASeq) <= lim Partial_Sums(P *
ASeq) by A16,A15,SEQ_2:18;
then Sum (P * Partial_Diff_Union ASeq) <= lim Partial_Sums(P * ASeq) by
SERIES_1:def 3;
then Sum (P * Partial_Diff_Union ASeq) <= Sum(P * ASeq) by SERIES_1:def 3;
then P.(Union Partial_Diff_Union ASeq) <= Sum(P * ASeq) by Th46;
hence thesis by A19,A20,A22,Th3,Th20,SERIES_1:def 3;
end;
theorem
P.(Union FSeq) <= Sum(P * FSeq) & (FSeq is disjoint_valued implies P.(
Union FSeq) = Sum(P * FSeq))
proof
consider ASeq being SetSequence of Sigma such that
A1: for k st k in dom FSeq holds ASeq.k = FSeq.k and
A2: for k st not k in dom FSeq holds ASeq.k = {} by Th56;
reconsider XSeq = ASeq as SetSequence of Omega;
A3: (for k st k in dom FSeq holds XSeq.k = FSeq.k) &
for k st not k in dom FSeq holds XSeq.k = {} by A1,A2;
then P.(Union ASeq) = P.(Union FSeq) by Th55;
then P.(Union FSeq) <= Sum(P * ASeq) by A1,A2,Th64;
hence P.(Union FSeq) <= Sum(P * FSeq) by A1,A2,Th64;
assume
A4: FSeq is disjoint_valued;
A5: FSeq is disjoint_valued implies ASeq is disjoint_valued
proof
assume
A6: FSeq is disjoint_valued;
for m,n being Nat st m <> n holds ASeq.m misses ASeq.n
proof
let m,n be Nat such that
A7: m <> n;
per cases;
suppose
A8: m in dom FSeq & n in dom FSeq;
FSeq.m misses FSeq.n by A6,A7,PROB_2:def 2;
then ASeq.m misses FSeq.n by A1,A8;
hence thesis by A1,A8;
end;
suppose
not (m in dom FSeq & n in dom FSeq);
then ASeq.m = {} or ASeq.n = {} by A2;
hence thesis;
end;
end;
hence thesis;
end;
thus P.(Union FSeq) = P.(Union ASeq) by Th55,A3
.= Sum(P * ASeq) by A5,A4,Th46
.= Sum(P * FSeq) by A1,A2,Th64;
end;
definition
::$CD 2
let X;
let IT be Subset-Family of X;
attr IT is non-decreasing-closed means
:Def7:
for A1 being SetSequence of X
st A1 is non-descending & rng A1 c= IT holds Union A1 in IT;
attr IT is non-increasing-closed means
:Def8:
for A1 being SetSequence of X
st A1 is non-ascending & rng A1 c= IT holds Intersection A1 in IT;
end;
theorem Th66:
for IT be Subset-Family of X holds IT is non-decreasing-closed
iff for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds
lim A1 in IT
proof
let IT be Subset-Family of X;
thus IT is non-decreasing-closed implies for A1 being SetSequence of X st A1
is non-descending & rng A1 c= IT holds lim A1 in IT
proof
assume
A1: IT is non-decreasing-closed;
now
let A1 be SetSequence of X;
assume that
A2: A1 is non-descending and
A3: rng A1 c= IT;
Union A1 in IT by A1,A2,A3;
hence lim A1 in IT by A2,SETLIM_1:63;
end;
hence thesis;
end;
assume
A4: for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT
holds lim A1 in IT;
for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT
holds Union A1 in IT
proof
let A1 be SetSequence of X;
assume that
A5: A1 is non-descending and
A6: rng A1 c= IT;
lim A1 in IT by A4,A5,A6;
hence thesis by A5,SETLIM_1:63;
end;
hence thesis;
end;
theorem Th67:
for IT be Subset-Family of X holds IT is non-increasing-closed
iff for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= IT holds
lim A1 in IT
proof
let IT be Subset-Family of X;
thus IT is non-increasing-closed implies for A1 being SetSequence of X st A1
is non-ascending & rng A1 c= IT holds lim A1 in IT
proof
assume
A1: IT is non-increasing-closed;
now
let A1 be SetSequence of X;
assume that
A2: A1 is non-ascending and
A3: rng A1 c= IT;
Intersection A1 in IT by A1,A2,A3;
hence lim A1 in IT by A2,SETLIM_1:64;
end;
hence thesis;
end;
assume
A4: for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= IT
holds lim A1 in IT;
for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= IT
holds Intersection A1 in IT
proof
let A1 be SetSequence of X;
assume that
A5: A1 is non-ascending and
A6: rng A1 c= IT;
lim A1 in IT by A4,A5,A6;
hence thesis by A5,SETLIM_1:64;
end;
hence thesis;
end;
theorem Th68:
bool X is non-decreasing-closed & bool X is non-increasing-closed;
registration
let X;
cluster non-decreasing-closed non-increasing-closed for Subset-Family of X;
existence
proof
take bool X;
thus thesis;
end;
end;
definition
let X;
mode MonotoneClass of X is non-decreasing-closed non-increasing-closed
Subset-Family of X;
end;
theorem Th69:
Z is MonotoneClass of X iff Z c= bool X & for A1 being
SetSequence of X st A1 is monotone & rng A1 c= Z holds lim A1 in Z
proof
thus Z is MonotoneClass of X implies Z c= bool X & for A1 being SetSequence
of X st A1 is monotone & rng A1 c= Z holds lim A1 in Z
proof
assume
A1: Z is MonotoneClass of X;
then reconsider Z as Subset-Family of X;
for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z
proof
let A1 be SetSequence of X;
assume that
A2: A1 is monotone and
A3: rng A1 c= Z;
per cases by A2,SETLIM_1:def 1;
suppose
A1 is non-descending;
hence thesis by A1,A3,Th66;
end;
suppose
A1 is non-ascending;
hence thesis by A1,A3,Th67;
end;
end;
hence thesis;
end;
assume that
A4: Z c= bool X and
A5: for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z;
reconsider Z as Subset-Family of X by A4;
A6: for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= Z
holds lim A1 in Z
proof
let A1 be SetSequence of X;
assume
A7: A1 is non-ascending & rng A1 c= Z;
A1 is monotone & rng A1 c= Z implies lim A1 in Z by A5;
hence thesis by A7,SETLIM_1:def 1;
end;
for A1 being SetSequence of X st A1 is non-descending & rng A1 c= Z
holds lim A1 in Z
proof
let A1 be SetSequence of X;
assume
A8: A1 is non-descending & rng A1 c= Z;
A1 is monotone & rng A1 c= Z implies lim A1 in Z by A5;
hence thesis by A8,SETLIM_1:def 1;
end;
hence thesis by A6,Th66,Th67;
end;
theorem Th70:
for F being Field_Subset of X holds F is SigmaField of X iff F
is MonotoneClass of X
proof
let F be Field_Subset of X;
thus F is SigmaField of X implies F is MonotoneClass of X
proof
assume F is SigmaField of X;
then reconsider F as SigmaField of X;
A1: for A1 being SetSequence of X st A1 is non-descending & rng A1 c= F
holds Union A1 in F
proof
let A1 be SetSequence of X;
assume that
A1 is non-descending and
A2: rng A1 c= F;
reconsider A2=A1 as SetSequence of F by A2,RELAT_1:def 19;
Union A2 in F by PROB_1:17;
hence thesis;
end;
F is non-increasing-closed
by PROB_1:def 6;
hence thesis by A1,Def7;
end;
assume
A3: F is MonotoneClass of X;
for A1 being SetSequence of X st rng A1 c= F holds Intersection A1 in F
proof
let A1 such that
A4: rng A1 c= F;
set A2 = Partial_Intersection A1;
defpred P[Nat] means A2.$1 in F;
A5: for k st P[k] holds P[k+1]
proof
let k;
assume
A6: A2.k in F;
A1.(k+1) in rng A1 & A2.(k+1) = A2.k /\ A1.(k+1) by Def1,NAT_1:51;
hence A2.(k+1) in F by A4,A6,FINSUB_1:def 2;
end;
A1.0 in rng A1 & A2.0 = A1.0 by Def1,NAT_1:51;
then
A7: P[0] by A4;
for k holds P[k] from NAT_1:sch 2(A7,A5);
then
A8: rng A2 c= F by NAT_1:52;
A2 is non-ascending by Th10;
then Intersection A2 in F by A3,A8,Def8;
hence thesis by Th14;
end;
hence thesis by PROB_1:def 6;
end;
theorem
bool Omega is MonotoneClass of Omega by Th68;
definition
let Omega;
let X be Subset-Family of Omega;
func monotoneclass(X) -> MonotoneClass of Omega means
:Def9:
X c= it & for Z st X c= Z & Z is MonotoneClass of Omega holds it c= Z;
existence
proof
set V = { M where M is Subset-Family of Omega : X c= M & M is MonotoneClass
of Omega};
set Y = meet V;
A1: for Z st Z in V holds X c= Z
proof
let Z;
assume Z in V;
then ex M being Subset-Family of Omega st Z = M & X c= M & M is
MonotoneClass of Omega;
hence thesis;
end;
bool Omega is MonotoneClass of Omega by Th68;
then
A2: bool Omega in V;
for MSeq being SetSequence of Omega st MSeq is monotone & rng MSeq c= Y
holds lim MSeq in Y
proof
let MSeq be SetSequence of Omega such that
A3: MSeq is monotone and
A4: rng MSeq c= Y;
now
let Z;
assume
A5: Z in V;
now
let n be Nat;
MSeq.n in rng MSeq by NAT_1:51;
hence MSeq.n in Z by A4,A5,SETFAM_1:def 1;
end;
then
A6: rng MSeq c= Z by NAT_1:52;
ex M being Subset-Family of Omega st Z = M & X c= M & M is
MonotoneClass of Omega by A5;
hence lim MSeq in Z by A3,A6,Th69;
end;
hence thesis by A2,SETFAM_1:def 1;
end;
then reconsider Y as MonotoneClass of Omega by A2,Th69,SETFAM_1:3;
take Y;
for Z st X c= Z & Z is MonotoneClass of Omega holds Y c= Z
proof
let Z;
assume X c= Z & Z is MonotoneClass of Omega;
then Z in V;
hence thesis by SETFAM_1:3;
end;
hence thesis by A2,A1,SETFAM_1:5;
end;
uniqueness;
end;
theorem Th72:
for Z being Field_Subset of Omega holds monotoneclass(Z) is
Field_Subset of Omega
proof
let Z be Field_Subset of Omega;
A1: Z c= monotoneclass(Z) by Def9;
then reconsider Z1=monotoneclass(Z) as non empty Subset-Family of Omega;
A2: for y,Y being set
st Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 &
x /\ y in Z1}
for z being set st z in Y holds z in Z1 & y \ z in Z1 & z \ y in Z1 &
z /\ y in Z1
proof
let y,Y be set;
assume
A3: Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\ y in Z1};
thus for z being set st z in Y
holds z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in
Z1
proof
let z be set;
assume z in Y;
then ex z1 be Element of Z1 st z = z1 & y \ z1 in Z1 & z1 \ y in Z1 & z1
/\ y in Z1 by A3;
hence thesis;
end;
end;
A4: for y being Element of Z1,Y st Y = {x where x is Element of Z1: y \ x in
Z1 & x \ y in Z1 & x /\ y in Z1} holds Y is MonotoneClass of Omega
proof
let y be Element of Z1,Y;
assume
A5: Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\ y in Z1};
A6: for A1 being SetSequence of Omega st A1 is monotone & rng A1 c= Y
holds lim A1 in Y
proof
let A1 be SetSequence of Omega such that
A7: A1 is monotone and
A8: rng A1 c= Y;
A9: A1 is convergent by A7,SETLIM_1:65;
for n holds A1.n in Z1
proof
let n;
A1.n in rng A1 by NAT_1:51;
hence thesis by A2,A5,A8;
end;
then rng A1 c= Z1 by NAT_1:52;
then
A10: lim A1 is Element of Z1 by A7,Th69;
for n holds (A1 (\) y).n in Z1
proof
let n be Nat;
A1.n in rng A1 by NAT_1:51;
then n in NAT & A1.n \ y in Z1 by A2,A5,A8,ORDINAL1:def 12;
hence thesis by SETLIM_2:def 8;
end;
then
A11: rng(A1 (\) y) c= Z1 by NAT_1:52;
for n holds (y (/\) A1).n in Z1
proof
let n;
A1.n in rng A1 by NAT_1:51;
then n in NAT & y /\ A1.n in Z1 by A2,A5,A8,ORDINAL1:def 12;
hence thesis by SETLIM_2:def 5;
end;
then
A12: rng (y (/\) A1) c= Z1 by NAT_1:52;
y (/\) A1 is monotone by A7,SETLIM_2:23;
then lim (y (/\) A1) in Z1 by A12,Th69;
then
A13: y /\ lim A1 in Z1 by A9,SETLIM_2:92;
for n holds (y (\) A1).n in Z1
proof
let n;
A1.n in rng A1 by NAT_1:51;
then n in NAT & y \ A1.n in Z1 by A2,A5,A8,ORDINAL1:def 12;
hence thesis by SETLIM_2:def 7;
end;
then
A14: rng(y (\) A1) c= Z1 by NAT_1:52;
y (\) A1 is monotone by A7,SETLIM_2:29;
then lim (y (\) A1) in Z1 by A14,Th69;
then
A15: y \ lim A1 in Z1 by A9,SETLIM_2:94;
A1 (\) y is monotone by A7,SETLIM_2:32;
then lim (A1 (\) y) in Z1 by A11,Th69;
then lim A1 \ y in Z1 by A9,SETLIM_2:95;
hence thesis by A5,A10,A15,A13;
end;
for z being object holds z in Y implies z in Z1 by A2,A5;
then Y c= Z1;
hence thesis by A6,Th69,XBOOLE_1:1;
end;
A16: for y being Element of Z,Y st Y = {x where x is Element of Z1: y \ x in
Z1 & x \ y in Z1 & x /\ y in Z1} holds Z1 c= Y
proof
let y be Element of Z,Y;
assume
A17: Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\
y in Z1};
A18: Z c= Y
proof
let z be object;
reconsider zz=z as set by TARSKI:1;
assume
A19: z in Z;
then
A20: zz /\ y in Z by FINSUB_1:def 2;
zz \ y in Z & y \ zz in Z by A19,PROB_1:6;
hence thesis by A1,A17,A19,A20;
end;
y in Z;
then Y is MonotoneClass of Omega by A1,A4,A17;
hence thesis by A18,Def9;
end;
A21: for y being Element of Z1,Y st Y = {x where x is Element of Z1: y \ x
in Z1 & x \ y in Z1 & x /\ y in Z1} holds Z1 c= Y
proof
let y be Element of Z1,Y;
assume
A22: Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\
y in Z1};
A23: Z c= Y
proof
let z be object;
reconsider zz=z as set by TARSKI:1;
set Y1 =
{x where x is Element of Z1: zz \ x in Z1 & x \ zz in Z1 & x /\ zz
in Z1};
assume
A24: z in Z;
then
A25: Z1 c= Y1 by A16;
A26: y in Z1;
then
A27: zz /\ y in Z1 by A2,A25;
zz \ y in Z1 & y \ zz in Z1 by A2,A25,A26;
hence thesis by A1,A22,A24,A27;
end;
Y is MonotoneClass of Omega by A4,A22;
hence thesis by A23,Def9;
end;
A28: for y being Subset of Omega st y in Z1 holds y` in Z1
proof
Omega in Z by PROB_1:5;
then
A29: Omega in Z1 by A1;
let y be Subset of Omega such that
A30: y in Z1;
set Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\ y in
Z1};
Z1 c= Y by A21,A30;
then Omega \ y in Z1 by A2,A29;
hence thesis by SUBSET_1:def 4;
end;
now
let y,z be set;
assume that
A31: y in Z1 and
A32: z in Z1;
set Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\ y in
Z1};
Z1 c= Y by A21,A31;
hence y /\ z in Z1 by A2,A32;
end;
hence thesis by A28,FINSUB_1:def 2,PROB_1:def 1;
end;
theorem
for Z being Field_Subset of Omega holds sigma Z = monotoneclass Z
proof
let Z be Field_Subset of Omega;
monotoneclass Z is Field_Subset of Omega by Th72;
then
A1: monotoneclass Z is SigmaField of Omega by Th70;
Z c= monotoneclass Z by Def9;
hence sigma Z c= monotoneclass Z by A1,PROB_1:def 9;
sigma Z is MonotoneClass of Omega & Z c= sigma Z by Th70,PROB_1:def 9;
hence thesis by Def9;
end;