:: KURATO_0 semantic presentation begin theorem :: KURATO_0:1 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k4_funct_6 :::"meet"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))) ; theorem :: KURATO_0:2 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "C")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k9_setfam_1 :::"bool"::: ) "X")) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "T" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"non-empty"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) "T") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k9_setfam_1 :::"bool"::: ) "T")) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "T" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); :: original: :::"Union"::: redefine func :::"Union"::: "F" -> ($#m1_subset_1 :::"Subset":::) "of" "X"; :: original: :::"meet"::: redefine func :::"meet"::: "F" -> ($#m1_subset_1 :::"Subset":::) "of" "X"; end; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); func :::"lim_inf"::: "F" -> ($#m1_subset_1 :::"Subset":::) "of" "X" means :: KURATO_0:def 1 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" "X" "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k2_kurato_0 :::"meet"::: ) (Set "(" "F" ($#k10_nat_1 :::"^\"::: ) (Set (Var "n")) ")" ))) ")" ) ")" )); func :::"lim_sup"::: "F" -> ($#m1_subset_1 :::"Subset":::) "of" "X" means :: KURATO_0:def 2 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" "X" "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k2_kurato_0 :::"meet"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set "(" "F" ($#k10_nat_1 :::"^\"::: ) (Set (Var "n")) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"lim_inf"::: KURATO_0:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k2_kurato_0 :::"meet"::: ) (Set "(" (Set (Var "F")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "n")) ")" ))) ")" ) ")" )) ")" )))); :: deftheorem defines :::"lim_sup"::: KURATO_0:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_kurato_0 :::"meet"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set "(" (Set (Var "F")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "n")) ")" ))) ")" ) ")" )) ")" )))); theorem :: KURATO_0:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_0 :::"meet"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "z"))))) ")" )))) ; theorem :: KURATO_0:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ))))) ")" )))) ; theorem :: KURATO_0:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ))))) ")" )))) ; theorem :: KURATO_0:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "F")))))) ; theorem :: KURATO_0:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_kurato_0 :::"meet"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "F")))))) ; theorem :: KURATO_0:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "F")))))) ; theorem :: KURATO_0:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "F")) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: KURATO_0:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "C")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "B")) ")" ))))) ; theorem :: KURATO_0:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "C")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "B")) ")" ))))) ; theorem :: KURATO_0:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "C")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool (Set (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "C")))))) ; theorem :: KURATO_0:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "C")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "B")) ")" ))))) ; theorem :: KURATO_0:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" )) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "B")))))) ; theorem :: KURATO_0:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" )) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "B")))))) ; theorem :: KURATO_0:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k5_subset_1 :::"\+\"::: ) (Set "(" (Set (Var "A")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool (Set (Set (Var "C")) ($#k5_subset_1 :::"\+\"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "B"))))))) ; theorem :: KURATO_0:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k5_subset_1 :::"\+\"::: ) (Set "(" (Set (Var "A")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool (Set (Set (Var "C")) ($#k5_subset_1 :::"\+\"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "B"))))))) ; begin theorem :: KURATO_0:18 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))) ; definitionlet "T" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "T")); :: original: :::"non-ascending"::: redefine attr "S" is :::"non-ascending"::: means :: KURATO_0:def 3 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "S" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set "S" ($#k3_funct_2 :::"."::: ) (Set (Var "i"))))); :: original: :::"non-descending"::: redefine attr "S" is :::"non-descending"::: means :: KURATO_0:def 4 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "S" ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set "S" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))); end; :: deftheorem defines :::"non-ascending"::: KURATO_0:def 3 : (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_prob_1 :::"non-ascending"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))))) ")" ))); :: deftheorem defines :::"non-descending"::: KURATO_0:def 4 : (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_prob_1 :::"non-descending"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" ))); theorem :: KURATO_0:19 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) "is" bbbadV2_PROB_1()) & (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "k")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_0 :::"meet"::: ) (Set (Var "F"))))))) ; theorem :: KURATO_0:20 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" bbbadV2_PROB_1())) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k2_kurato_0 :::"meet"::: ) (Set (Var "F")))))) ; theorem :: KURATO_0:21 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" bbbadV3_PROB_1())) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "F")))))) ; begin definitionlet "T" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "T")); attr "S" is :::"convergent"::: means :: KURATO_0:def 5 (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) "S") ($#r1_hidden :::"="::: ) (Set ($#k3_kurato_0 :::"lim_inf"::: ) "S")); end; :: deftheorem defines :::"convergent"::: KURATO_0:def 5 : (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) "iff" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "S")))) ")" ))); theorem :: KURATO_0:22 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool (Set ($#k3_funct_1 :::"the_value_of"::: ) (Set (Var "S"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))))) ; registrationlet "T" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k9_setfam_1 :::"bool"::: ) "T")) -> bbbadV2_PROB_1() bbbadV3_PROB_1() ($#v3_kurato_0 :::"convergent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "T" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "T" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) "T") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k9_setfam_1 :::"bool"::: ) "T")) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "T" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; notationlet "T" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#v3_kurato_0 :::"convergent"::: ) ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "T")); synonym :::"Lim_K"::: "S" for :::"lim_sup"::: "S"; end; theorem :: KURATO_0:23 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_kurato_0 :::"convergent"::: ) ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_kurato_0 :::"Lim_K"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ))))) ")" )))) ;