:: PROB_1 semantic presentation begin theorem Th1: :: PROB_1:1 for r being real number for seq being Real_Sequence st ex n being Element of NAT st for m being Element of NAT st n <= m holds seq . m = r holds ( seq is convergent & lim seq = r ) proof let r be real number ; ::_thesis: for seq being Real_Sequence st ex n being Element of NAT st for m being Element of NAT st n <= m holds seq . m = r holds ( seq is convergent & lim seq = r ) let seq be Real_Sequence; ::_thesis: ( ex n being Element of NAT st for m being Element of NAT st n <= m holds seq . m = r implies ( seq is convergent & lim seq = r ) ) assume A1: ex n being Element of NAT st for m being Element of NAT st n <= m holds seq . m = r ; ::_thesis: ( seq is convergent & lim seq = r ) A2: for r1 being real number st 0 < r1 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq . m) - r) < r1 proof consider n being Element of NAT such that A3: for m being Element of NAT st n <= m holds seq . m = r by A1; let r1 be real number ; ::_thesis: ( 0 < r1 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq . m) - r) < r1 ) assume A4: 0 < r1 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq . m) - r) < r1 take n ; ::_thesis: for m being Element of NAT st n <= m holds abs ((seq . m) - r) < r1 let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq . m) - r) < r1 ) assume n <= m ; ::_thesis: abs ((seq . m) - r) < r1 then seq . m = r by A3; hence abs ((seq . m) - r) < r1 by A4, ABSVALUE:2; ::_thesis: verum end; then seq is convergent by SEQ_2:def_6; hence ( seq is convergent & lim seq = r ) by A2, SEQ_2:def_7; ::_thesis: verum end; definition let X be set ; let IT be Subset-Family of X; attrIT is compl-closed means :Def1: :: PROB_1:def 1 for A being Subset of X st A in IT holds A ` in IT; end; :: deftheorem Def1 defines compl-closed PROB_1:def_1_:_ for X being set for IT being Subset-Family of X holds ( IT is compl-closed iff for A being Subset of X st A in IT holds A ` in IT ); registration let X be set ; cluster bool X -> cap-closed ; coherence bool X is cap-closed proof let A, B be set ; :: according to FINSUB_1:def_2 ::_thesis: ( not A in bool X or not B in bool X or A /\ B in bool X ) assume that A1: A in bool X and B in bool X ; ::_thesis: A /\ B in bool X A /\ B c= X by A1, XBOOLE_1:108; hence A /\ B in bool X ; ::_thesis: verum end; end; registration let X be set ; cluster bool X -> compl-closed for Subset-Family of X; coherence for b1 being Subset-Family of X st b1 = bool X holds b1 is compl-closed proof bool X is compl-closed proof let A be Subset of X; :: according to PROB_1:def_1 ::_thesis: ( A in bool X implies A ` in bool X ) thus ( A in bool X implies A ` in bool X ) ; ::_thesis: verum end; hence for b1 being Subset-Family of X st b1 = bool X holds b1 is compl-closed ; ::_thesis: verum end; end; registration let X be set ; cluster non empty cap-closed compl-closed for Event of ; existence ex b1 being Subset-Family of X st ( not b1 is empty & b1 is compl-closed & b1 is cap-closed ) proof take bool X ; ::_thesis: ( not bool X is empty & bool X is compl-closed & bool X is cap-closed ) thus ( not bool X is empty & bool X is compl-closed & bool X is cap-closed ) ; ::_thesis: verum end; end; definition let X be set ; mode Field_Subset of X is non empty cap-closed compl-closed Subset-Family of X; end; theorem Th2: :: PROB_1:2 for X being set for A, B being Subset of X holds {A,B} is Subset-Family of X proof let X be set ; ::_thesis: for A, B being Subset of X holds {A,B} is Subset-Family of X let A, B be Subset of X; ::_thesis: {A,B} is Subset-Family of X set C = {A,B}; {A,B} c= bool X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {A,B} or x in bool X ) assume x in {A,B} ; ::_thesis: x in bool X then ( x = A or x = B ) by TARSKI:def_2; hence x in bool X ; ::_thesis: verum end; hence {A,B} is Subset-Family of X ; ::_thesis: verum end; theorem Th3: :: PROB_1:3 for X being set for F being Field_Subset of X for A, B being set st A in F & B in F holds A \/ B in F proof let X be set ; ::_thesis: for F being Field_Subset of X for A, B being set st A in F & B in F holds A \/ B in F let F be Field_Subset of X; ::_thesis: for A, B being set st A in F & B in F holds A \/ B in F let A, B be set ; ::_thesis: ( A in F & B in F implies A \/ B in F ) assume A1: ( A in F & B in F ) ; ::_thesis: A \/ B in F then reconsider A1 = A, B1 = B as Subset of X ; ( A1 ` in F & B1 ` in F ) by A1, Def1; then (A1 `) /\ (B1 `) in F by FINSUB_1:def_2; then (A1 \/ B1) ` in F by XBOOLE_1:53; then ((A1 \/ B1) `) ` in F by Def1; hence A \/ B in F ; ::_thesis: verum end; theorem Th4: :: PROB_1:4 for X being set for F being Field_Subset of X holds {} in F proof let X be set ; ::_thesis: for F being Field_Subset of X holds {} in F let F be Field_Subset of X; ::_thesis: {} in F consider A being Subset of X such that A1: A in F by SUBSET_1:4; A misses A ` by XBOOLE_1:79; then A2: A /\ (A `) = {} by XBOOLE_0:def_7; A ` in F by A1, Def1; hence {} in F by A1, A2, FINSUB_1:def_2; ::_thesis: verum end; theorem Th5: :: PROB_1:5 for X being set for F being Field_Subset of X holds X in F proof let X be set ; ::_thesis: for F being Field_Subset of X holds X in F let F be Field_Subset of X; ::_thesis: X in F consider A being Subset of X such that A1: A in F by SUBSET_1:4; A2: A \/ (A `) = [#] X by SUBSET_1:10 .= X ; A ` in F by A1, Def1; hence X in F by A1, A2, Th3; ::_thesis: verum end; theorem Th6: :: PROB_1:6 for X being set for F being Field_Subset of X for A, B being Subset of X st A in F & B in F holds A \ B in F proof let X be set ; ::_thesis: for F being Field_Subset of X for A, B being Subset of X st A in F & B in F holds A \ B in F let F be Field_Subset of X; ::_thesis: for A, B being Subset of X st A in F & B in F holds A \ B in F let A, B be Subset of X; ::_thesis: ( A in F & B in F implies A \ B in F ) assume A1: A in F ; ::_thesis: ( not B in F or A \ B in F ) assume B in F ; ::_thesis: A \ B in F then B ` in F by Def1; then A /\ (B `) in F by A1, FINSUB_1:def_2; hence A \ B in F by SUBSET_1:13; ::_thesis: verum end; theorem :: PROB_1:7 for X being set for F being Field_Subset of X for A, B being set st A in F & B in F holds (A \ B) \/ B in F proof let X be set ; ::_thesis: for F being Field_Subset of X for A, B being set st A in F & B in F holds (A \ B) \/ B in F let F be Field_Subset of X; ::_thesis: for A, B being set st A in F & B in F holds (A \ B) \/ B in F let A, B be set ; ::_thesis: ( A in F & B in F implies (A \ B) \/ B in F ) A \/ B = (A \ B) \/ B by XBOOLE_1:39; hence ( A in F & B in F implies (A \ B) \/ B in F ) by Th3; ::_thesis: verum end; registration let X be set ; cluster{{},X} -> cap-closed ; coherence {{},X} is cap-closed proof let A, B be set ; :: according to FINSUB_1:def_2 ::_thesis: ( not A in {{},X} or not B in {{},X} or A /\ B in {{},X} ) A1: ( ( A = {} or B = {} ) implies A /\ B = {} ) ; ( A = X & B = X implies A /\ B = X ) ; hence ( not A in {{},X} or not B in {{},X} or A /\ B in {{},X} ) by A1, TARSKI:def_2; ::_thesis: verum end; end; theorem :: PROB_1:8 for X being set holds {{},X} is Field_Subset of X proof let X be set ; ::_thesis: {{},X} is Field_Subset of X ( {} c= X & X in bool X ) by XBOOLE_1:2, ZFMISC_1:def_1; then reconsider EX = {{},X} as Subset-Family of X by Th2; now__::_thesis:_for_A_being_Subset_of_X_st_A_in_EX_holds_ A_`_in_EX let A be Subset of X; ::_thesis: ( A in EX implies A ` in EX ) A1: ( A = {} implies A ` = X ) ; ( A = X implies A ` = {} X ) by XBOOLE_1:37; hence ( A in EX implies A ` in EX ) by A1, TARSKI:def_2; ::_thesis: verum end; hence {{},X} is Field_Subset of X by Def1; ::_thesis: verum end; theorem :: PROB_1:9 for X being set holds bool X is Field_Subset of X ; theorem :: PROB_1:10 for X being set for F being Field_Subset of X holds ( {{},X} c= F & F c= bool X ) proof let X be set ; ::_thesis: for F being Field_Subset of X holds ( {{},X} c= F & F c= bool X ) let F be Field_Subset of X; ::_thesis: ( {{},X} c= F & F c= bool X ) ( {} in F & X in F ) by Th4, Th5; then for x being set st x in {{},X} holds x in F by TARSKI:def_2; hence ( {{},X} c= F & F c= bool X ) by TARSKI:def_3; ::_thesis: verum end; definition let X be set ; mode SetSequence of X is sequence of (bool X); end; theorem Th11: :: PROB_1:11 for X being set for A1 being SetSequence of X holds union (rng A1) is Subset of X proof let X be set ; ::_thesis: for A1 being SetSequence of X holds union (rng A1) is Subset of X let A1 be SetSequence of X; ::_thesis: union (rng A1) is Subset of X for Y being set st Y in rng A1 holds Y c= X proof let Y be set ; ::_thesis: ( Y in rng A1 implies Y c= X ) assume Y in rng A1 ; ::_thesis: Y c= X then consider y being set such that A1: y in dom A1 and A2: Y = A1 . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A1, FUNCT_2:def_1; Y = A1 . y by A2; hence Y c= X ; ::_thesis: verum end; hence union (rng A1) is Subset of X by ZFMISC_1:76; ::_thesis: verum end; definition let X be set ; let A1 be SetSequence of X; :: original: Union redefine func Union A1 -> Subset of X; coherence Union A1 is Subset of X by Th11; end; theorem Th12: :: PROB_1:12 for X, x being set for A1 being SetSequence of X holds ( x in Union A1 iff ex n being Element of NAT st x in A1 . n ) proof let X, x be set ; ::_thesis: for A1 being SetSequence of X holds ( x in Union A1 iff ex n being Element of NAT st x in A1 . n ) let A1 be SetSequence of X; ::_thesis: ( x in Union A1 iff ex n being Element of NAT st x in A1 . n ) set DX = union (rng A1); for x being set holds ( x in union (rng A1) iff ex n being Element of NAT st x in A1 . n ) proof let x be set ; ::_thesis: ( x in union (rng A1) iff ex n being Element of NAT st x in A1 . n ) thus ( x in union (rng A1) implies ex n being Element of NAT st x in A1 . n ) ::_thesis: ( ex n being Element of NAT st x in A1 . n implies x in union (rng A1) ) proof assume x in union (rng A1) ; ::_thesis: ex n being Element of NAT st x in A1 . n then consider Y being set such that A1: x in Y and A2: Y in rng A1 by TARSKI:def_4; consider p being set such that A3: p in dom A1 and A4: Y = A1 . p by A2, FUNCT_1:def_3; p in NAT by A3, FUNCT_2:def_1; hence ex n being Element of NAT st x in A1 . n by A1, A4; ::_thesis: verum end; thus ( ex n being Element of NAT st x in A1 . n implies x in union (rng A1) ) ::_thesis: verum proof given n being Element of NAT such that A5: x in A1 . n ; ::_thesis: x in union (rng A1) n in NAT ; then n in dom A1 by FUNCT_2:def_1; then A1 . n in rng A1 by FUNCT_1:def_3; hence x in union (rng A1) by A5, TARSKI:def_4; ::_thesis: verum end; end; hence ( x in Union A1 iff ex n being Element of NAT st x in A1 . n ) ; ::_thesis: verum end; definition let X be set ; let A1 be SetSequence of X; func Complement A1 -> SetSequence of X means :Def2: :: PROB_1:def 2 for n being Element of NAT holds it . n = (A1 . n) ` ; existence ex b1 being SetSequence of X st for n being Element of NAT holds b1 . n = (A1 . n) ` proof deffunc H1( Element of NAT ) -> Event of = (A1 . \$1) ` ; ex f being Function of NAT,(bool X) st for x being Element of NAT holds f . x = H1(x) from FUNCT_2:sch_4(); then consider f being Function of NAT,(bool X) such that A1: for x being Element of NAT holds f . x = (A1 . x) ` ; take f ; ::_thesis: for n being Element of NAT holds f . n = (A1 . n) ` thus for n being Element of NAT holds f . n = (A1 . n) ` by A1; ::_thesis: verum end; uniqueness for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) ` ) & ( for n being Element of NAT holds b2 . n = (A1 . n) ` ) holds b1 = b2 proof let BSeq, CSeq be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds BSeq . n = (A1 . n) ` ) & ( for n being Element of NAT holds CSeq . n = (A1 . n) ` ) implies BSeq = CSeq ) assume that A2: for n being Element of NAT holds BSeq . n = (A1 . n) ` and A3: for m being Element of NAT holds CSeq . m = (A1 . m) ` ; ::_thesis: BSeq = CSeq A4: for x being set st x in NAT holds BSeq . x = CSeq . x proof let x be set ; ::_thesis: ( x in NAT implies BSeq . x = CSeq . x ) assume x in NAT ; ::_thesis: BSeq . x = CSeq . x then reconsider x = x as Element of NAT ; BSeq . x = (A1 . x) ` by A2 .= CSeq . x by A3 ; hence BSeq . x = CSeq . x ; ::_thesis: verum end; ( NAT = dom BSeq & NAT = dom CSeq ) by FUNCT_2:def_1; hence BSeq = CSeq by A4, FUNCT_1:2; ::_thesis: verum end; involutiveness for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (b2 . n) ` ) holds for n being Element of NAT holds b2 . n = (b1 . n) ` proof let IT, A1 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds IT . n = (A1 . n) ` ) implies for n being Element of NAT holds A1 . n = (IT . n) ` ) assume A5: for n being Element of NAT holds IT . n = (A1 . n) ` ; ::_thesis: for n being Element of NAT holds A1 . n = (IT . n) ` let n be Element of NAT ; ::_thesis: A1 . n = (IT . n) ` thus A1 . n = ((A1 . n) `) ` .= (IT . n) ` by A5 ; ::_thesis: verum end; end; :: deftheorem Def2 defines Complement PROB_1:def_2_:_ for X being set for A1, b3 being SetSequence of X holds ( b3 = Complement A1 iff for n being Element of NAT holds b3 . n = (A1 . n) ` ); definition let X be set ; let A1 be SetSequence of X; func Intersection A1 -> Subset of X equals :: PROB_1:def 3 (Union (Complement A1)) ` ; correctness coherence (Union (Complement A1)) ` is Subset of X; ; end; :: deftheorem defines Intersection PROB_1:def_3_:_ for X being set for A1 being SetSequence of X holds Intersection A1 = (Union (Complement A1)) ` ; theorem Th13: :: PROB_1:13 for X, x being set for A1 being SetSequence of X holds ( x in Intersection A1 iff for n being Element of NAT holds x in A1 . n ) proof let X, x be set ; ::_thesis: for A1 being SetSequence of X holds ( x in Intersection A1 iff for n being Element of NAT holds x in A1 . n ) let A1 be SetSequence of X; ::_thesis: ( x in Intersection A1 iff for n being Element of NAT holds x in A1 . n ) A1: for n being Element of NAT holds X \ ((Complement A1) . n) = A1 . n proof let n be Element of NAT ; ::_thesis: X \ ((Complement A1) . n) = A1 . n X \ ((Complement A1) . n) = ((A1 . n) `) ` by Def2 .= A1 . n ; hence X \ ((Complement A1) . n) = A1 . n ; ::_thesis: verum end; A2: ( ( for n being Element of NAT holds ( x in X & not x in (Complement A1) . n ) ) iff for n being Element of NAT holds x in A1 . n ) proof thus ( ( for n being Element of NAT holds ( x in X & not x in (Complement A1) . n ) ) implies for n being Element of NAT holds x in A1 . n ) ::_thesis: ( ( for n being Element of NAT holds x in A1 . n ) implies for n being Element of NAT holds ( x in X & not x in (Complement A1) . n ) ) proof assume A3: for n being Element of NAT holds ( x in X & not x in (Complement A1) . n ) ; ::_thesis: for n being Element of NAT holds x in A1 . n let n be Element of NAT ; ::_thesis: x in A1 . n not x in (Complement A1) . n by A3; then x in X \ ((Complement A1) . n) by A3, XBOOLE_0:def_5; hence x in A1 . n by A1; ::_thesis: verum end; assume A4: for n being Element of NAT holds x in A1 . n ; ::_thesis: for n being Element of NAT holds ( x in X & not x in (Complement A1) . n ) let n be Element of NAT ; ::_thesis: ( x in X & not x in (Complement A1) . n ) x in A1 . n by A4; then x in X \ ((Complement A1) . n) by A1; hence ( x in X & not x in (Complement A1) . n ) by XBOOLE_0:def_5; ::_thesis: verum end; ( x in X & not x in Union (Complement A1) iff ( x in X & ( for n being Element of NAT holds not x in (Complement A1) . n ) ) ) by Th12; hence ( x in Intersection A1 iff for n being Element of NAT holds x in A1 . n ) by A2, XBOOLE_0:def_5; ::_thesis: verum end; Lm1: for X being set for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `) proof let X be set ; ::_thesis: for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `) let A, B be Subset of X; ::_thesis: Complement (A followed_by B) = (A `) followed_by (B `) let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (Complement (A followed_by B)) . n = ((A `) followed_by (B `)) . n percases ( n = 0 or n > 0 ) by NAT_1:3; supposeA1: n = 0 ; ::_thesis: (Complement (A followed_by B)) . n = ((A `) followed_by (B `)) . n thus (Complement (A followed_by B)) . n = ((A followed_by B) . n) ` by Def2 .= A ` by A1, FUNCT_7:119 .= ((A `) followed_by (B `)) . n by A1, FUNCT_7:119 ; ::_thesis: verum end; supposeA2: n > 0 ; ::_thesis: (Complement (A followed_by B)) . n = ((A `) followed_by (B `)) . n thus (Complement (A followed_by B)) . n = ((A followed_by B) . n) ` by Def2 .= B ` by A2, FUNCT_7:120 .= ((A `) followed_by (B `)) . n by A2, FUNCT_7:120 ; ::_thesis: verum end; end; end; theorem Th14: :: PROB_1:14 for X being set for A, B being Subset of X holds Intersection (A followed_by B) = A /\ B proof let X be set ; ::_thesis: for A, B being Subset of X holds Intersection (A followed_by B) = A /\ B let A, B be Subset of X; ::_thesis: Intersection (A followed_by B) = A /\ B set A1 = A followed_by B; Complement (A followed_by B) = (A `) followed_by (B `) by Lm1; then rng (Complement (A followed_by B)) = {(A `),(B `)} by FUNCT_7:126; then Union (Complement (A followed_by B)) = (A `) \/ (B `) by ZFMISC_1:75; then (Union (Complement (A followed_by B))) ` = ((A `) `) /\ ((B `) `) by XBOOLE_1:53; hence Intersection (A followed_by B) = A /\ B ; ::_thesis: verum end; definition let f be Function; attrf is non-ascending means :Def4: :: PROB_1:def 4 for n, m being Element of NAT st n <= m holds f . m c= f . n; attrf is non-descending means :: PROB_1:def 5 for n, m being Element of NAT st n <= m holds f . n c= f . m; end; :: deftheorem Def4 defines non-ascending PROB_1:def_4_:_ for f being Function holds ( f is non-ascending iff for n, m being Element of NAT st n <= m holds f . m c= f . n ); :: deftheorem defines non-descending PROB_1:def_5_:_ for f being Function holds ( f is non-descending iff for n, m being Element of NAT st n <= m holds f . n c= f . m ); definition let X be set ; let F be Subset-Family of X; attrF is sigma-multiplicative means :Def6: :: PROB_1:def 6 for A1 being SetSequence of X st rng A1 c= F holds Intersection A1 in F; end; :: deftheorem Def6 defines sigma-multiplicative PROB_1:def_6_:_ for X being set for F being Subset-Family of X holds ( F is sigma-multiplicative iff for A1 being SetSequence of X st rng A1 c= F holds Intersection A1 in F ); registration let X be set ; cluster bool X -> sigma-multiplicative for Subset-Family of X; coherence for b1 being Subset-Family of X st b1 = bool X holds b1 is sigma-multiplicative proof for BSeq being SetSequence of X st rng BSeq c= bool X holds Intersection BSeq in bool X ; hence for b1 being Subset-Family of X st b1 = bool X holds b1 is sigma-multiplicative by Def6; ::_thesis: verum end; end; registration let X be set ; cluster non empty compl-closed sigma-multiplicative for Event of ; existence ex b1 being Subset-Family of X st ( b1 is compl-closed & b1 is sigma-multiplicative & not b1 is empty ) proof take bool X ; ::_thesis: ( bool X is compl-closed & bool X is sigma-multiplicative & not bool X is empty ) thus ( bool X is compl-closed & bool X is sigma-multiplicative & not bool X is empty ) ; ::_thesis: verum end; end; definition let X be set ; mode SigmaField of X is non empty compl-closed sigma-multiplicative Subset-Family of X; end; theorem :: PROB_1:15 for X being set for S being non empty set holds ( S is SigmaField of X iff ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds Intersection A1 in S ) & ( for A being Subset of X st A in S holds A ` in S ) ) ) by Def1, Def6; theorem Th16: :: PROB_1:16 for Y, X being set st Y is SigmaField of X holds Y is Field_Subset of X proof let Y, X be set ; ::_thesis: ( Y is SigmaField of X implies Y is Field_Subset of X ) assume A1: Y is SigmaField of X ; ::_thesis: Y is Field_Subset of X Y is cap-closed proof let A, B be set ; :: according to FINSUB_1:def_2 ::_thesis: ( not A in Y or not B in Y or A /\ B in Y ) assume A2: ( A in Y & B in Y ) ; ::_thesis: A /\ B in Y then reconsider A9 = A, B9 = B as Subset of X by A1; set A1 = A9 followed_by B9; rng (A9 followed_by B9) = {A9,B9} by FUNCT_7:126; then A3: rng (A9 followed_by B9) c= Y by A2, ZFMISC_1:32; Intersection (A9 followed_by B9) = A /\ B by Th14; hence A /\ B in Y by A1, A3, Def6; ::_thesis: verum end; hence Y is Field_Subset of X by A1; ::_thesis: verum end; registration let X be set ; cluster non empty compl-closed sigma-multiplicative -> cap-closed for Event of ; coherence for b1 being SigmaField of X holds ( b1 is cap-closed & b1 is compl-closed ) by Th16; end; registration let X be set ; let F be non empty Subset-Family of X; cluster Relation-like NAT -defined F -valued bool X -valued Function-like V37( NAT , bool X) for Event of ; existence ex b1 being SetSequence of X st b1 is F -valued proof set A1 = NAT --> the Element of F; reconsider A1 = NAT --> the Element of F as SetSequence of X by FUNCOP_1:45; take A1 ; ::_thesis: A1 is F -valued thus A1 is F -valued ; ::_thesis: verum end; end; definition let X be set ; let F be non empty Subset-Family of X; mode SetSequence of F is F -valued SetSequence of X; end; theorem Th17: :: PROB_1:17 for X being set for Si being SigmaField of X for ASeq being SetSequence of Si holds Union ASeq in Si proof let X be set ; ::_thesis: for Si being SigmaField of X for ASeq being SetSequence of Si holds Union ASeq in Si let Si be SigmaField of X; ::_thesis: for ASeq being SetSequence of Si holds Union ASeq in Si let ASeq be SetSequence of Si; ::_thesis: Union ASeq in Si A1: for A1 being SetSequence of X st rng A1 c= Si holds for n being Nat holds (Complement A1) . n in Si proof let A1 be SetSequence of X; ::_thesis: ( rng A1 c= Si implies for n being Nat holds (Complement A1) . n in Si ) assume A2: rng A1 c= Si ; ::_thesis: for n being Nat holds (Complement A1) . n in Si let n be Nat; ::_thesis: (Complement A1) . n in Si A1 . n in rng A1 by NAT_1:51; then ( n in NAT & (A1 . n) ` in Si ) by A2, Def1, ORDINAL1:def_12; hence (Complement A1) . n in Si by Def2; ::_thesis: verum end; A3: for A1 being SetSequence of X st rng A1 c= Si holds Union (Complement (Complement A1)) in Si proof let A1 be SetSequence of X; ::_thesis: ( rng A1 c= Si implies Union (Complement (Complement A1)) in Si ) assume rng A1 c= Si ; ::_thesis: Union (Complement (Complement A1)) in Si then for n being Nat holds (Complement A1) . n in Si by A1; then rng (Complement A1) c= Si by NAT_1:52; then Intersection (Complement A1) in Si by Def6; then ((Union (Complement (Complement A1))) `) ` in Si by Def1; hence Union (Complement (Complement A1)) in Si ; ::_thesis: verum end; A4: for A1 being SetSequence of X st rng A1 c= Si holds Union A1 in Si proof let A1 be SetSequence of X; ::_thesis: ( rng A1 c= Si implies Union A1 in Si ) assume rng A1 c= Si ; ::_thesis: Union A1 in Si then Union (Complement (Complement A1)) in Si by A3; hence Union A1 in Si ; ::_thesis: verum end; rng ASeq c= Si by RELAT_1:def_19; hence Union ASeq in Si by A4; ::_thesis: verum end; notation let X be set ; let F be SigmaField of X; synonym Event of F for Element of X; end; definition let X be set ; let F be SigmaField of X; :: original: Event redefine mode Event of F -> Subset of X; coherence for b1 being Event of holds b1 is Subset of X proof let E be Event of ; ::_thesis: E is Subset of X E in F ; hence E is Subset of X ; ::_thesis: verum end; end; theorem :: PROB_1:18 for X, x being set for Si being SigmaField of X st x in Si holds x is Event of Si ; theorem :: PROB_1:19 for X being set for Si being SigmaField of X for A, B being Event of Si holds A /\ B is Event of Si by FINSUB_1:def_2; theorem :: PROB_1:20 for X being set for Si being SigmaField of X for A being Event of Si holds A ` is Event of Si by Def1; theorem :: PROB_1:21 for X being set for Si being SigmaField of X for A, B being Event of Si holds A \/ B is Event of Si by Th3; theorem :: PROB_1:22 for X being set for Si being SigmaField of X holds {} is Event of Si by Th4; theorem :: PROB_1:23 for X being set for Si being SigmaField of X holds X is Event of Si by Th5; theorem :: PROB_1:24 for X being set for Si being SigmaField of X for A, B being Event of Si holds A \ B is Event of Si by Th6; registration let X be set ; let Si be SigmaField of X; cluster empty for Event of ; existence ex b1 being Event of Si st b1 is empty proof {} is Event of Si by Th4; hence ex b1 being Event of Si st b1 is empty ; ::_thesis: verum end; end; definition let X be set ; let Si be SigmaField of X; func [#] Si -> Event of Si equals :: PROB_1:def 7 X; coherence X is Event of Si by Th5; end; :: deftheorem defines [#] PROB_1:def_7_:_ for X being set for Si being SigmaField of X holds [#] Si = X; definition let X be set ; let Si be SigmaField of X; let A, B be Event of Si; :: original: /\ redefine funcA /\ B -> Event of Si; coherence A /\ B is Event of Si by FINSUB_1:def_2; :: original: \/ redefine funcA \/ B -> Event of Si; coherence A \/ B is Event of Si by Th3; :: original: \ redefine funcA \ B -> Event of Si; coherence A \ B is Event of Si by Th6; end; theorem :: PROB_1:25 for X being set for A1 being SetSequence of X for Si being SigmaField of X holds ( A1 is SetSequence of Si iff for n being Element of NAT holds A1 . n is Event of Si ) proof let X be set ; ::_thesis: for A1 being SetSequence of X for Si being SigmaField of X holds ( A1 is SetSequence of Si iff for n being Element of NAT holds A1 . n is Event of Si ) let A1 be SetSequence of X; ::_thesis: for Si being SigmaField of X holds ( A1 is SetSequence of Si iff for n being Element of NAT holds A1 . n is Event of Si ) let Si be SigmaField of X; ::_thesis: ( A1 is SetSequence of Si iff for n being Element of NAT holds A1 . n is Event of Si ) thus ( A1 is SetSequence of Si implies for n being Element of NAT holds A1 . n is Event of Si ) ::_thesis: ( ( for n being Element of NAT holds A1 . n is Event of Si ) implies A1 is SetSequence of Si ) proof assume A1 is SetSequence of Si ; ::_thesis: for n being Element of NAT holds A1 . n is Event of Si then A1: rng A1 c= Si by RELAT_1:def_19; for n being Element of NAT holds A1 . n is Event of Si proof let n be Element of NAT ; ::_thesis: A1 . n is Event of Si A1 . n in rng A1 by NAT_1:51; hence A1 . n is Event of Si by A1; ::_thesis: verum end; hence for n being Element of NAT holds A1 . n is Event of Si ; ::_thesis: verum end; assume A2: for n being Element of NAT holds A1 . n is Event of Si ; ::_thesis: A1 is SetSequence of Si for n being Nat holds A1 . n in Si proof let n be Nat; ::_thesis: A1 . n in Si n in NAT by ORDINAL1:def_12; then A1 . n is Event of Si by A2; hence A1 . n in Si ; ::_thesis: verum end; then rng A1 c= Si by NAT_1:52; hence A1 is SetSequence of Si by RELAT_1:def_19; ::_thesis: verum end; theorem :: PROB_1:26 for Omega being set for ASeq being SetSequence of Omega for Sigma being SigmaField of Omega st ASeq is SetSequence of Sigma holds Union ASeq is Event of Sigma by Th17; theorem Th27: :: PROB_1:27 for Omega, p being set for Sigma being SigmaField of Omega ex f being Function st ( dom f = Sigma & ( for D being Subset of Omega st D in Sigma holds ( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) ) ) proof let Omega, p be set ; ::_thesis: for Sigma being SigmaField of Omega ex f being Function st ( dom f = Sigma & ( for D being Subset of Omega st D in Sigma holds ( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) ) ) let Sigma be SigmaField of Omega; ::_thesis: ex f being Function st ( dom f = Sigma & ( for D being Subset of Omega st D in Sigma holds ( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) ) ) deffunc H1( set ) -> Element of NAT = 0 ; deffunc H2( set ) -> Element of NAT = 1; defpred S1[ set ] means p in \$1; ex f being Function st ( dom f = Sigma & ( for x being set st x in Sigma holds ( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) ) ) from PARTFUN1:sch_1(); then consider f being Function such that A1: dom f = Sigma and A2: for x being set st x in Sigma holds ( ( S1[x] implies f . x = 1 ) & ( not S1[x] implies f . x = 0 ) ) ; take f ; ::_thesis: ( dom f = Sigma & ( for D being Subset of Omega st D in Sigma holds ( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) ) ) thus dom f = Sigma by A1; ::_thesis: for D being Subset of Omega st D in Sigma holds ( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) let D be Subset of Omega; ::_thesis: ( D in Sigma implies ( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) ) assume A3: D in Sigma ; ::_thesis: ( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) hence ( p in D implies f . D = 1 ) by A2; ::_thesis: ( not p in D implies f . D = 0 ) assume not p in D ; ::_thesis: f . D = 0 hence f . D = 0 by A2, A3; ::_thesis: verum end; theorem Th28: :: PROB_1:28 for Omega, p being set for Sigma being SigmaField of Omega ex P being Function of Sigma,REAL st for D being Subset of Omega st D in Sigma holds ( ( p in D implies P . D = 1 ) & ( not p in D implies P . D = 0 ) ) proof let Omega, p be set ; ::_thesis: for Sigma being SigmaField of Omega ex P being Function of Sigma,REAL st for D being Subset of Omega st D in Sigma holds ( ( p in D implies P . D = 1 ) & ( not p in D implies P . D = 0 ) ) let Sigma be SigmaField of Omega; ::_thesis: ex P being Function of Sigma,REAL st for D being Subset of Omega st D in Sigma holds ( ( p in D implies P . D = 1 ) & ( not p in D implies P . D = 0 ) ) consider f being Function such that A1: dom f = Sigma and A2: for D being Subset of Omega st D in Sigma holds ( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) by Th27; rng f c= REAL proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in REAL ) assume y in rng f ; ::_thesis: y in REAL then consider x being set such that A3: x in dom f and A4: y = f . x by FUNCT_1:def_3; reconsider x = x as Subset of Omega by A1, A3; A5: ( not p in x implies y = 0 ) by A1, A2, A3, A4; ( p in x implies y = 1 ) by A1, A2, A3, A4; hence y in REAL by A5; ::_thesis: verum end; then reconsider f = f as Function of Sigma,REAL by A1, FUNCT_2:def_1, RELSET_1:4; take f ; ::_thesis: for D being Subset of Omega st D in Sigma holds ( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) thus for D being Subset of Omega st D in Sigma holds ( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) by A2; ::_thesis: verum end; theorem Th29: :: PROB_1:29 for Omega being set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Function of Sigma,REAL holds P * ASeq is Real_Sequence proof let Omega be set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Function of Sigma,REAL holds P * ASeq is Real_Sequence let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma for P being Function of Sigma,REAL holds P * ASeq is Real_Sequence let ASeq be SetSequence of Sigma; ::_thesis: for P being Function of Sigma,REAL holds P * ASeq is Real_Sequence let P be Function of Sigma,REAL; ::_thesis: P * ASeq is Real_Sequence rng ASeq c= Sigma by RELAT_1:def_19; then rng ASeq c= dom P by FUNCT_2:def_1; then A1: dom (P * ASeq) = dom ASeq by RELAT_1:27 .= NAT by FUNCT_2:def_1 ; rng (P * ASeq) c= REAL by RELAT_1:def_19; hence P * ASeq is Real_Sequence by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; definition let Omega be set ; let Sigma be SigmaField of Omega; let ASeq be SetSequence of Sigma; let P be Function of Sigma,REAL; :: original: * redefine funcP * ASeq -> Real_Sequence; coherence ASeq * P is Real_Sequence by Th29; end; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; mode Probability of Sigma -> Function of Sigma,REAL means :Def8: :: PROB_1:def 8 ( ( for A being Event of Sigma holds 0 <= it . A ) & it . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds it . (A \/ B) = (it . A) + (it . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds ( it * ASeq is convergent & lim (it * ASeq) = it . (Intersection ASeq) ) ) ); existence ex b1 being Function of Sigma,REAL st ( ( for A being Event of Sigma holds 0 <= b1 . A ) & b1 . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds b1 . (A \/ B) = (b1 . A) + (b1 . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds ( b1 * ASeq is convergent & lim (b1 * ASeq) = b1 . (Intersection ASeq) ) ) ) proof set p = the Element of Omega; consider P being Function of Sigma,REAL such that A1: for D being Subset of Omega st D in Sigma holds ( ( the Element of Omega in D implies P . D = 1 ) & ( not the Element of Omega in D implies P . D = 0 ) ) by Th28; take P ; ::_thesis: ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ) ) thus for A being Event of Sigma holds 0 <= P . A by A1; ::_thesis: ( P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ) ) [#] Sigma in Sigma ; hence P . Omega = 1 by A1; ::_thesis: ( ( for A, B being Event of Sigma st A misses B holds P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ) ) thus for A, B being Event of Sigma st A misses B holds P . (A \/ B) = (P . A) + (P . B) ::_thesis: for ASeq being SetSequence of Sigma st ASeq is non-ascending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) proof let A, B be Event of Sigma; ::_thesis: ( A misses B implies P . (A \/ B) = (P . A) + (P . B) ) assume A2: A misses B ; ::_thesis: P . (A \/ B) = (P . A) + (P . B) A3: ( the Element of Omega in A & not the Element of Omega in B implies the Element of Omega in A \/ B ) by XBOOLE_0:def_3; A4: ( not the Element of Omega in A & the Element of Omega in B implies ( P . A = 0 & P . B = 1 ) ) by A1; A5: ( not the Element of Omega in A & the Element of Omega in B implies the Element of Omega in A \/ B ) by XBOOLE_0:def_3; A6: ( not the Element of Omega in A & not the Element of Omega in B implies ( P . A = 0 & P . B = 0 ) ) by A1; A7: ( not the Element of Omega in A & not the Element of Omega in B implies not the Element of Omega in A \/ B ) by XBOOLE_0:def_3; ( the Element of Omega in A & not the Element of Omega in B implies ( P . A = 1 & P . B = 0 ) ) by A1; hence P . (A \/ B) = (P . A) + (P . B) by A1, A2, A3, A4, A5, A6, A7, XBOOLE_0:3; ::_thesis: verum end; let ASeq be SetSequence of Sigma; ::_thesis: ( ASeq is non-ascending implies ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ) A8: for n being Element of NAT holds (P * ASeq) . n = P . (ASeq . n) proof let n be Element of NAT ; ::_thesis: (P * ASeq) . n = P . (ASeq . n) dom (P * ASeq) = NAT by FUNCT_2:def_1; hence (P * ASeq) . n = P . (ASeq . n) by FUNCT_1:12; ::_thesis: verum end; A9: ( ( for n being Element of NAT holds the Element of Omega in ASeq . n ) implies for n being Element of NAT holds (P * ASeq) . n = 1 ) proof assume A10: for n being Element of NAT holds the Element of Omega in ASeq . n ; ::_thesis: for n being Element of NAT holds (P * ASeq) . n = 1 for n being Element of NAT holds (P * ASeq) . n = 1 proof let n be Element of NAT ; ::_thesis: (P * ASeq) . n = 1 A11: ( rng ASeq c= Sigma & ASeq . n in rng ASeq ) by NAT_1:51, RELAT_1:def_19; the Element of Omega in ASeq . n by A10; then P . (ASeq . n) = 1 by A1, A11; hence (P * ASeq) . n = 1 by A8; ::_thesis: verum end; hence for n being Element of NAT holds (P * ASeq) . n = 1 ; ::_thesis: verum end; assume A12: ASeq is non-ascending ; ::_thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) A13: ( not for n being Element of NAT holds the Element of Omega in ASeq . n implies ex m being Element of NAT st for n being Element of NAT st m <= n holds (P * ASeq) . n = 0 ) proof assume not for n being Element of NAT holds the Element of Omega in ASeq . n ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds (P * ASeq) . n = 0 then consider m being Element of NAT such that A14: not the Element of Omega in ASeq . m ; take m ; ::_thesis: for n being Element of NAT st m <= n holds (P * ASeq) . n = 0 for n being Element of NAT st m <= n holds (P * ASeq) . n = 0 proof let n be Element of NAT ; ::_thesis: ( m <= n implies (P * ASeq) . n = 0 ) assume m <= n ; ::_thesis: (P * ASeq) . n = 0 then ASeq . n c= ASeq . m by A12, Def4; then A15: not the Element of Omega in ASeq . n by A14; ( rng ASeq c= Sigma & ASeq . n in rng ASeq ) by NAT_1:51, RELAT_1:def_19; then P . (ASeq . n) = 0 by A1, A15; hence (P * ASeq) . n = 0 by A8; ::_thesis: verum end; hence for n being Element of NAT st m <= n holds (P * ASeq) . n = 0 ; ::_thesis: verum end; A16: ( ex m being Element of NAT st for n being Element of NAT st m <= n holds (P * ASeq) . n = 0 implies ( P * ASeq is convergent & lim (P * ASeq) = 0 ) ) by Th1; rng ASeq c= Sigma by RELAT_1:def_19; then A17: Intersection ASeq in Sigma by Def6; reconsider r = 1 as Real ; A18: ( ( for n being Element of NAT holds (P * ASeq) . n = 1 ) implies ( P * ASeq is convergent & lim (P * ASeq) = 1 ) ) proof assume A19: for n being Element of NAT holds (P * ASeq) . n = 1 ; ::_thesis: ( P * ASeq is convergent & lim (P * ASeq) = 1 ) ex m being Element of NAT st for n being Element of NAT st m <= n holds (P * ASeq) . n = r proof take 0 ; ::_thesis: for n being Element of NAT st 0 <= n holds (P * ASeq) . n = r thus for n being Element of NAT st 0 <= n holds (P * ASeq) . n = r by A19; ::_thesis: verum end; hence ( P * ASeq is convergent & lim (P * ASeq) = 1 ) by Th1; ::_thesis: verum end; percases ( ex n being Element of NAT st not the Element of Omega in ASeq . n or for n being Element of NAT holds the Element of Omega in ASeq . n ) ; supposeA20: not for n being Element of NAT holds the Element of Omega in ASeq . n ; ::_thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) then not the Element of Omega in Intersection ASeq by Th13; hence ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by A1, A13, A16, A20, A17; ::_thesis: verum end; supposeA21: for n being Element of NAT holds the Element of Omega in ASeq . n ; ::_thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) then the Element of Omega in Intersection ASeq by Th13; hence ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by A1, A9, A18, A21, A17; ::_thesis: verum end; end; end; end; :: deftheorem Def8 defines Probability PROB_1:def_8_:_ for Omega being non empty set for Sigma being SigmaField of Omega for b3 being Function of Sigma,REAL holds ( b3 is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= b3 . A ) & b3 . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds b3 . (A \/ B) = (b3 . A) + (b3 . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds ( b3 * ASeq is convergent & lim (b3 * ASeq) = b3 . (Intersection ASeq) ) ) ) ); registration let Omega be non empty set ; let Sigma be SigmaField of Omega; cluster -> zeroed for Probability of Sigma; coherence for b1 being Probability of Sigma holds b1 is zeroed proof reconsider E = {} as Event of Sigma by Th4; let P be Probability of Sigma; ::_thesis: P is zeroed A1: ( {} misses [#] Sigma & {} \/ ([#] Sigma) = [#] Sigma ) by XBOOLE_1:65; 1 = P . ([#] Sigma) by Def8; then 1 = (P . E) + 1 by A1, Def8; hence P . {} = 0 ; :: according to VALUED_0:def_19 ::_thesis: verum end; end; theorem :: PROB_1:30 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma holds P . ([#] Sigma) = 1 by Def8; theorem Th31: :: PROB_1:31 for Omega being non empty set for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma holds (P . (([#] Sigma) \ A)) + (P . A) = 1 proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma holds (P . (([#] Sigma) \ A)) + (P . A) = 1 let Sigma be SigmaField of Omega; ::_thesis: for A being Event of Sigma for P being Probability of Sigma holds (P . (([#] Sigma) \ A)) + (P . A) = 1 let A be Event of Sigma; ::_thesis: for P being Probability of Sigma holds (P . (([#] Sigma) \ A)) + (P . A) = 1 let P be Probability of Sigma; ::_thesis: (P . (([#] Sigma) \ A)) + (P . A) = 1 A1: (([#] Sigma) \ A) \/ A = (A `) \/ A .= [#] Omega by SUBSET_1:10 .= Omega ; ([#] Sigma) \ A misses A by XBOOLE_1:79; then (P . (([#] Sigma) \ A)) + (P . A) = P . Omega by A1, Def8 .= 1 by Def8 ; hence (P . (([#] Sigma) \ A)) + (P . A) = 1 ; ::_thesis: verum end; theorem :: PROB_1:32 for Omega being non empty set for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A) let Sigma be SigmaField of Omega; ::_thesis: for A being Event of Sigma for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A) let A be Event of Sigma; ::_thesis: for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A) let P be Probability of Sigma; ::_thesis: P . (([#] Sigma) \ A) = 1 - (P . A) (P . (([#] Sigma) \ A)) + (P . A) = 1 by Th31; hence P . (([#] Sigma) \ A) = 1 - (P . A) ; ::_thesis: verum end; theorem Th33: :: PROB_1:33 for Omega being non empty set for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma st A c= B holds P . (B \ A) = (P . B) - (P . A) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma st A c= B holds P . (B \ A) = (P . B) - (P . A) let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma for P being Probability of Sigma st A c= B holds P . (B \ A) = (P . B) - (P . A) let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma st A c= B holds P . (B \ A) = (P . B) - (P . A) let P be Probability of Sigma; ::_thesis: ( A c= B implies P . (B \ A) = (P . B) - (P . A) ) assume A1: A c= B ; ::_thesis: P . (B \ A) = (P . B) - (P . A) A misses B \ A by XBOOLE_1:79; then (P . A) + (P . (B \ A)) = P . (A \/ (B \ A)) by Def8 .= P . B by A1, XBOOLE_1:45 ; hence P . (B \ A) = (P . B) - (P . A) ; ::_thesis: verum end; theorem Th34: :: PROB_1:34 for Omega being non empty set for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma st A c= B holds P . A <= P . B proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma st A c= B holds P . A <= P . B let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma for P being Probability of Sigma st A c= B holds P . A <= P . B let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma st A c= B holds P . A <= P . B let P be Probability of Sigma; ::_thesis: ( A c= B implies P . A <= P . B ) assume A c= B ; ::_thesis: P . A <= P . B then P . (B \ A) = (P . B) - (P . A) by Th33; then 0 <= (P . B) - (P . A) by Def8; then 0 + (P . A) <= P . B by XREAL_1:19; hence P . A <= P . B ; ::_thesis: verum end; theorem :: PROB_1:35 for Omega being non empty set for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma holds P . A <= 1 proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma holds P . A <= 1 let Sigma be SigmaField of Omega; ::_thesis: for A being Event of Sigma for P being Probability of Sigma holds P . A <= 1 let A be Event of Sigma; ::_thesis: for P being Probability of Sigma holds P . A <= 1 let P be Probability of Sigma; ::_thesis: P . A <= 1 P . ([#] Sigma) = 1 by Def8; hence P . A <= 1 by Th34; ::_thesis: verum end; theorem Th36: :: PROB_1:36 for Omega being non empty set for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A)) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A)) let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A)) let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A)) let P be Probability of Sigma; ::_thesis: P . (A \/ B) = (P . A) + (P . (B \ A)) A1: A misses B \ A by XBOOLE_1:79; P . (A \/ B) = P . (A \/ (B \ A)) by XBOOLE_1:39 .= (P . A) + (P . (B \ A)) by A1, Def8 ; hence P . (A \/ B) = (P . A) + (P . (B \ A)) ; ::_thesis: verum end; theorem Th37: :: PROB_1:37 for Omega being non empty set for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ (A /\ B))) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ (A /\ B))) let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ (A /\ B))) let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ (A /\ B))) let P be Probability of Sigma; ::_thesis: P . (A \/ B) = (P . A) + (P . (B \ (A /\ B))) thus P . (A \/ B) = (P . A) + (P . (B \ A)) by Th36 .= (P . A) + (P . (B \ (A /\ B))) by XBOOLE_1:47 ; ::_thesis: verum end; theorem Th38: :: PROB_1:38 for Omega being non empty set for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma holds P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B)) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma holds P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B)) let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma for P being Probability of Sigma holds P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B)) let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma holds P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B)) let P be Probability of Sigma; ::_thesis: P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B)) P . (A \/ B) = (P . A) + (P . (B \ (A /\ B))) by Th37 .= (P . A) + ((P . B) - (P . (A /\ B))) by Th33, XBOOLE_1:17 ; hence P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B)) ; ::_thesis: verum end; theorem :: PROB_1:39 for Omega being non empty set for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma holds P . (A \/ B) <= (P . A) + (P . B) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma holds P . (A \/ B) <= (P . A) + (P . B) let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma for P being Probability of Sigma holds P . (A \/ B) <= (P . A) + (P . B) let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma holds P . (A \/ B) <= (P . A) + (P . B) let P be Probability of Sigma; ::_thesis: P . (A \/ B) <= (P . A) + (P . B) ( 0 <= P . (A /\ B) & P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B)) ) by Def8, Th38; hence P . (A \/ B) <= (P . A) + (P . B) by XREAL_1:43; ::_thesis: verum end; theorem :: PROB_1:40 for X being set holds bool X is SigmaField of X ; definition let Omega be non empty set ; let X be Subset-Family of Omega; func sigma X -> SigmaField of Omega means :: PROB_1:def 9 ( X c= it & ( for Z being set st X c= Z & Z is SigmaField of Omega holds it c= Z ) ); existence ex b1 being SigmaField of Omega st ( X c= b1 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds b1 c= Z ) ) proof set V = { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; set Y = meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; A1: now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_Omega_:_(_X_c=_S_&_S_is_SigmaField_of_Omega_)__}__holds_ X_c=_Z let Z be set ; ::_thesis: ( Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } implies X c= Z ) assume Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; ::_thesis: X c= Z then ex S being Subset-Family of Omega st ( Z = S & X c= S & S is SigmaField of Omega ) ; hence X c= Z ; ::_thesis: verum end; A2: bool Omega in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; A3: for E being Subset of Omega st E in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } holds E ` in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } proof let E be Subset of Omega; ::_thesis: ( E in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } implies E ` in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ) assume A4: E in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; ::_thesis: E ` in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_Omega_:_(_X_c=_S_&_S_is_SigmaField_of_Omega_)__}__holds_ E_`_in_Z let Z be set ; ::_thesis: ( Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } implies E ` in Z ) assume Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; ::_thesis: E ` in Z then ( E in Z & ex S being Subset-Family of Omega st ( Z = S & X c= S & S is SigmaField of Omega ) ) by A4, SETFAM_1:def_1; hence E ` in Z by Def1; ::_thesis: verum end; hence E ` in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } by A2, SETFAM_1:def_1; ::_thesis: verum end; A5: for BSeq being SetSequence of Omega st rng BSeq c= meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } holds Intersection BSeq in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } proof let BSeq be SetSequence of Omega; ::_thesis: ( rng BSeq c= meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } implies Intersection BSeq in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ) assume A6: rng BSeq c= meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; ::_thesis: Intersection BSeq in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_Omega_:_(_X_c=_S_&_S_is_SigmaField_of_Omega_)__}__holds_ Intersection_BSeq_in_Z let Z be set ; ::_thesis: ( Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } implies Intersection BSeq in Z ) assume A7: Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; ::_thesis: Intersection BSeq in Z now__::_thesis:_for_n_being_Nat_holds_BSeq_._n_in_Z let n be Nat; ::_thesis: BSeq . n in Z BSeq . n in rng BSeq by NAT_1:51; hence BSeq . n in Z by A6, A7, SETFAM_1:def_1; ::_thesis: verum end; then A8: rng BSeq c= Z by NAT_1:52; ex S being Subset-Family of Omega st ( Z = S & X c= S & S is SigmaField of Omega ) by A7; hence Intersection BSeq in Z by A8, Def6; ::_thesis: verum end; hence Intersection BSeq in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } by A2, SETFAM_1:def_1; ::_thesis: verum end; now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_Omega_:_(_X_c=_S_&_S_is_SigmaField_of_Omega_)__}__holds_ {}_in_Z let Z be set ; ::_thesis: ( Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } implies {} in Z ) assume Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; ::_thesis: {} in Z then ex S being Subset-Family of Omega st ( Z = S & X c= S & S is SigmaField of Omega ) ; hence {} in Z by Th4; ::_thesis: verum end; then reconsider Y = meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } as SigmaField of Omega by A2, A5, A3, Def1, Def6, SETFAM_1:3, SETFAM_1:def_1; take Y ; ::_thesis: ( X c= Y & ( for Z being set st X c= Z & Z is SigmaField of Omega holds Y c= Z ) ) for Z being set st X c= Z & Z is SigmaField of Omega holds Y c= Z proof let Z be set ; ::_thesis: ( X c= Z & Z is SigmaField of Omega implies Y c= Z ) assume that A9: X c= Z and A10: Z is SigmaField of Omega ; ::_thesis: Y c= Z reconsider Z = Z as Subset-Family of Omega by A10; Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } by A9, A10; hence Y c= Z by SETFAM_1:3; ::_thesis: verum end; hence ( X c= Y & ( for Z being set st X c= Z & Z is SigmaField of Omega holds Y c= Z ) ) by A2, A1, SETFAM_1:5; ::_thesis: verum end; uniqueness for b1, b2 being SigmaField of Omega st X c= b1 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds b1 c= Z ) & X c= b2 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds b2 c= Z ) holds b1 = b2 proof let R1, R2 be SigmaField of Omega; ::_thesis: ( X c= R1 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds R1 c= Z ) & X c= R2 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds R2 c= Z ) implies R1 = R2 ) assume ( X c= R1 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds R1 c= Z ) & X c= R2 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds R2 c= Z ) ) ; ::_thesis: R1 = R2 then ( R1 c= R2 & R2 c= R1 ) ; hence R1 = R2 by XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem defines sigma PROB_1:def_9_:_ for Omega being non empty set for X being Subset-Family of Omega for b3 being SigmaField of Omega holds ( b3 = sigma X iff ( X c= b3 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds b3 c= Z ) ) ); definition let r be ext-real number ; func halfline r -> Subset of REAL equals :: PROB_1:def 10 ].-infty,r.[; coherence ].-infty,r.[ is Subset of REAL proof ].-infty,r.[ c= REAL proof let x be real number ; :: according to MEMBERED:def_9 ::_thesis: ( not x in ].-infty,r.[ or x in REAL ) assume x in ].-infty,r.[ ; ::_thesis: x in REAL then ( -infty < x & x < r ) by XXREAL_1:4; hence x in REAL by XXREAL_0:48; ::_thesis: verum end; hence ].-infty,r.[ is Subset of REAL ; ::_thesis: verum end; end; :: deftheorem defines halfline PROB_1:def_10_:_ for r being ext-real number holds halfline r = ].-infty,r.[; definition func Family_of_halflines -> Subset-Family of REAL equals :: PROB_1:def 11 { (halfline r) where r is Element of REAL : verum } ; coherence { (halfline r) where r is Element of REAL : verum } is Subset-Family of REAL proof { (halfline r) where r is Element of REAL : verum } c= bool REAL proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { (halfline r) where r is Element of REAL : verum } or p in bool REAL ) assume p in { (halfline r) where r is Element of REAL : verum } ; ::_thesis: p in bool REAL then ex r being Element of REAL st p = halfline r ; hence p in bool REAL ; ::_thesis: verum end; hence { (halfline r) where r is Element of REAL : verum } is Subset-Family of REAL ; ::_thesis: verum end; end; :: deftheorem defines Family_of_halflines PROB_1:def_11_:_ Family_of_halflines = { (halfline r) where r is Element of REAL : verum } ; definition func Borel_Sets -> SigmaField of REAL equals :: PROB_1:def 12 sigma Family_of_halflines; correctness coherence sigma Family_of_halflines is SigmaField of REAL; ; end; :: deftheorem defines Borel_Sets PROB_1:def_12_:_ Borel_Sets = sigma Family_of_halflines; theorem :: PROB_1:41 for X being set for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `) by Lm1; definition let X, Y be set ; let A be Subset-Family of X; let F be Function of Y,(bool A); let x be set ; :: original: . redefine funcF . x -> Subset-Family of X; coherence F . x is Subset-Family of X proof percases ( x in dom F or not x in dom F ) ; supposeA1: x in dom F ; ::_thesis: F . x is Subset-Family of X A2: rng F c= bool A by RELAT_1:def_19; A3: bool A c= bool (bool X) by ZFMISC_1:67; F . x in rng F by A1, FUNCT_1:def_3; then F . x in bool A by A2; hence F . x is Subset-Family of X by A3; ::_thesis: verum end; suppose not x in dom F ; ::_thesis: F . x is Subset-Family of X then F . x = {} by FUNCT_1:def_2; hence F . x is Subset-Family of X by XBOOLE_1:2; ::_thesis: verum end; end; end; end;