:: DYNKIN semantic presentation begin theorem :: DYNKIN:1 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )))) ; theorem :: DYNKIN:2 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "n")) "is" ($#v1_finset_1 :::"finite"::: ) )) ; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k6_card_1 :::"Segm"::: ) "n") -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a", "b", "c" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Omega")); :: original: :::"followed_by"::: redefine func "(" "a" "," "b" ")" :::"followed_by"::: "c" -> ($#m1_subset_1 :::"SetSequence":::) "of" "Omega"; end; theorem :: DYNKIN:3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_card_3 :::"Union"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k13_funct_7 :::"followed_by"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "b"))))) ; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Omega")); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Omega")); func :::"seqIntersection"::: "(" "X" "," "f" ")" -> ($#m1_subset_1 :::"SetSequence":::) "of" "Omega" means :: DYNKIN:def 1 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "X" ($#k9_subset_1 :::"/\"::: ) (Set "(" "f" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"seqIntersection"::: DYNKIN:def 1 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_dynkin :::"seqIntersection"::: ) "(" (Set (Var "X")) "," (Set (Var "f")) ")" )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))))); begin definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Omega")); :: original: :::"disjoint_valued"::: redefine attr "f" is :::"disjoint_valued"::: means :: DYNKIN:def 2 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set "f" ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xboole_0 :::"misses"::: ) (Set "f" ($#k8_nat_1 :::"."::: ) (Set (Var "m"))))); end; :: deftheorem defines :::"disjoint_valued"::: DYNKIN:def 2 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_prob_2 :::"disjoint_valued"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))))) ")" ))); theorem :: DYNKIN:4 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "Y")))) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "y")))) ")" ))) ; notationlet "x" be ($#m1_hidden :::"set"::: ) ; synonym :::"intersection_stable"::: "x" for :::"cap-closed"::: ; end; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Omega")); let "n" be ($#m1_hidden :::"Nat":::); func :::"disjointify"::: "(" "f" "," "n" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "Omega" equals :: DYNKIN:def 3 (Set (Set "(" "f" ($#k8_nat_1 :::"."::: ) "n" ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" "f" ($#k5_relat_1 :::"|"::: ) "n" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"disjointify"::: DYNKIN:def 3 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_dynkin :::"disjointify"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "n")) ")" ) ")" ) ")" )))))); definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "g" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Omega")); func :::"disjointify"::: "g" -> ($#m1_subset_1 :::"SetSequence":::) "of" "Omega" means :: DYNKIN:def 4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_dynkin :::"disjointify"::: ) "(" "g" "," (Set (Var "n")) ")" ))); end; :: deftheorem defines :::"disjointify"::: DYNKIN:def 4 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_dynkin :::"disjointify"::: ) (Set (Var "g")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_dynkin :::"disjointify"::: ) "(" (Set (Var "g")) "," (Set (Var "n")) ")" ))) ")" ))); theorem :: DYNKIN:5 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k4_dynkin :::"disjointify"::: ) (Set (Var "f")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "n")) ")" ) ")" ) ")" )))))) ; theorem :: DYNKIN:6 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) "holds" (Bool (Set ($#k4_dynkin :::"disjointify"::: ) (Set (Var "f"))) "is" bbbadV1_PROB_2()))) ; theorem :: DYNKIN:7 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_dynkin :::"disjointify"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ))))) ; theorem :: DYNKIN:8 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "x")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "y")))) "holds" (Bool (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_dynkin :::"followed_by"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set (Var "Omega")) ")" )) "is" bbbadV1_PROB_2()))) ; theorem :: DYNKIN:9 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "f")) "is" bbbadV1_PROB_2())) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) "holds" (Bool (Set ($#k2_dynkin :::"seqIntersection"::: ) "(" (Set (Var "X")) "," (Set (Var "f")) ")" ) "is" bbbadV1_PROB_2())))) ; theorem :: DYNKIN:10 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) "holds" (Bool (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" ($#k2_dynkin :::"seqIntersection"::: ) "(" (Set (Var "X")) "," (Set (Var "f")) ")" ")" )))))) ; begin definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode :::"Dynkin_System"::: "of" "Omega" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "Omega" means :: DYNKIN:def 5 (Bool "(" (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" "Omega" "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) it) & (Bool (Set (Var "f")) "is" bbbadV1_PROB_2())) "holds" (Bool (Set ($#k1_prob_1 :::"Union"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) it) ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Omega" "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) it) ")" ) & (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) it) ")" ); end; :: deftheorem defines :::"Dynkin_System"::: DYNKIN:def 5 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "b2"))) & (Bool (Set (Var "f")) "is" bbbadV1_PROB_2())) "holds" (Bool (Set ($#k1_prob_1 :::"Union"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool (Set (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" ) & (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" ) ")" ))); registrationlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_dynkin :::"Dynkin_System"::: ) "of" "Omega"; end; theorem :: DYNKIN:11 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "Omega"))) "is" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega")))) ; theorem :: DYNKIN:12 (Bool "for" (Set (Var "F")) "," (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "Y")) "is" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega"))) ")" )) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "F"))) "is" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega")))) ; theorem :: DYNKIN:13 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "D")) "is" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega"))) & (Bool (Set (Var "D")) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) ) & (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "D")))))) ; theorem :: DYNKIN:14 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "D")) "is" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega"))) & (Bool (Set (Var "D")) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) ) & (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "D")))))) ; theorem :: DYNKIN:15 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "D")) "is" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega"))) & (Bool (Set (Var "D")) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "D")))))) ; theorem :: DYNKIN:16 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "D")) "is" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega"))) & (Bool (Set (Var "D")) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_dynkin :::"disjointify"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "D")))))) ; theorem :: DYNKIN:17 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "D")) "is" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega"))) & (Bool (Set (Var "D")) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "D")))))) ; theorem :: DYNKIN:18 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "x")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "x")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "D")))))) ; theorem :: DYNKIN:19 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "y")) ($#k7_subset_1 :::"\"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "D")))))) ; begin theorem :: DYNKIN:20 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "D")) "is" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega"))) & (Bool (Set (Var "D")) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) )) "holds" (Bool (Set (Var "D")) "is" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega"))))) ; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "Omega")); func :::"generated_Dynkin_System"::: "E" -> ($#m1_dynkin :::"Dynkin_System"::: ) "of" "Omega" means :: DYNKIN:def 6 (Bool "(" (Bool "E" ($#r1_tarski :::"c="::: ) it) & (Bool "(" "for" (Set (Var "D")) "being" ($#m1_dynkin :::"Dynkin_System"::: ) "of" "Omega" "st" (Bool (Bool "E" ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ); end; :: deftheorem defines :::"generated_Dynkin_System"::: DYNKIN:def 6 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "b3")) "being" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_dynkin :::"generated_Dynkin_System"::: ) (Set (Var "E")))) "iff" (Bool "(" (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set (Var "b3"))) & (Bool "(" "for" (Set (Var "D")) "being" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set (Var "b3")) ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ) ")" )))); definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Omega")); func :::"DynSys"::: "(" "X" "," "G" ")" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "Omega" means :: DYNKIN:def 7 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Omega" "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) "X") ($#r2_hidden :::"in"::: ) "G") ")" )); end; :: deftheorem defines :::"DynSys"::: DYNKIN:def 7 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_dynkin :::"DynSys"::: ) "(" (Set (Var "X")) "," (Set (Var "G")) ")" )) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" )) ")" ))))); definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Const "Omega")); let "X" be ($#m2_subset_1 :::"Element"::: ) "of" (Set (Const "G")); :: original: :::"DynSys"::: redefine func :::"DynSys"::: "(" "X" "," "G" ")" -> ($#m1_dynkin :::"Dynkin_System"::: ) "of" "Omega"; end; theorem :: DYNKIN:21 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_dynkin :::"generated_Dynkin_System"::: ) (Set (Var "E")))) & (Bool (Set (Var "E")) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Y"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_dynkin :::"generated_Dynkin_System"::: ) (Set (Var "E"))))))) ; theorem :: DYNKIN:22 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k5_dynkin :::"generated_Dynkin_System"::: ) (Set (Var "E")))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_dynkin :::"generated_Dynkin_System"::: ) (Set (Var "E")))) & (Bool (Set (Var "E")) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Y"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_dynkin :::"generated_Dynkin_System"::: ) (Set (Var "E"))))))) ; theorem :: DYNKIN:23 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "E")) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) )) "holds" (Bool (Set ($#k5_dynkin :::"generated_Dynkin_System"::: ) (Set (Var "E"))) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) ))) ; theorem :: DYNKIN:24 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "E")) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) )) "holds" (Bool "for" (Set (Var "D")) "being" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k9_prob_1 :::"sigma"::: ) (Set (Var "E"))) ($#r1_tarski :::"c="::: ) (Set (Var "D")))))) ;