:: PARTIT1 semantic presentation begin theorem :: PARTIT1:1 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "X")) "," (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "PA"))) & (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "PA"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "V")))))) ; notationlet "SFX", "SFY" be ($#m1_hidden :::"set"::: ) ; synonym "SFX" :::"'<'"::: "SFY" for "SFX" :::"is_finer_than"::: "SFY"; synonym "SFY" :::"'>'"::: "SFX" for "SFX" :::"is_finer_than"::: "SFY"; end; theorem :: PARTIT1:2 (Bool "for" (Set (Var "SFX")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "SFX")) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "SFX"))))) ; theorem :: PARTIT1:3 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "PA")) ($#r1_setfam_1 :::"'>'"::: ) (Set (Var "PB"))) & (Bool (Set (Var "PB")) ($#r1_setfam_1 :::"'>'"::: ) (Set (Var "PA")))) "holds" (Bool (Set (Var "PB")) ($#r1_tarski :::"c="::: ) (Set (Var "PA"))))) ; theorem :: PARTIT1:4 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "PA")) ($#r1_setfam_1 :::"'>'"::: ) (Set (Var "PB"))) & (Bool (Set (Var "PB")) ($#r1_setfam_1 :::"'>'"::: ) (Set (Var "PA")))) "holds" (Bool (Set (Var "PA")) ($#r1_hidden :::"="::: ) (Set (Var "PB"))))) ; theorem :: PARTIT1:5 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "PA")) ($#r1_setfam_1 :::"'>'"::: ) (Set (Var "PB")))) "holds" (Bool (Set (Var "PA")) ($#r2_setfam_1 :::"is_coarser_than"::: ) (Set (Var "PB"))))) ; definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "PA" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")); let "b" be ($#m1_hidden :::"set"::: ) ; pred "b" :::"is_a_dependent_set_of"::: "PA" means :: PARTIT1:def 1 (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) "PA") & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "b" ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "B")))) ")" )); end; :: deftheorem defines :::"is_a_dependent_set_of"::: PARTIT1:def 1 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PA"))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "PA"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "B")))) ")" )) ")" )))); definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "PA", "PB" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")); let "b" be ($#m1_hidden :::"set"::: ) ; pred "b" :::"is_min_depend"::: "PA" "," "PB" means :: PARTIT1:def 2 (Bool "(" (Bool "b" ($#r1_partit1 :::"is_a_dependent_set_of"::: ) "PA") & (Bool "b" ($#r1_partit1 :::"is_a_dependent_set_of"::: ) "PB") & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "d")) ($#r1_tarski :::"c="::: ) "b") & (Bool (Set (Var "d")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) "PA") & (Bool (Set (Var "d")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) "PB")) "holds" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) "b") ")" ) ")" ); end; :: deftheorem defines :::"is_min_depend"::: PARTIT1:def 2 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r2_partit1 :::"is_min_depend"::: ) (Set (Var "PA")) "," (Set (Var "PB"))) "iff" (Bool "(" (Bool (Set (Var "b")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PA"))) & (Bool (Set (Var "b")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PB"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "d")) ($#r1_tarski :::"c="::: ) (Set (Var "b"))) & (Bool (Set (Var "d")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PA"))) & (Bool (Set (Var "d")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PB")))) "holds" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) ")" ) ")" )))); theorem :: PARTIT1:6 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "PA")) ($#r1_setfam_1 :::"'>'"::: ) (Set (Var "PB")))) "holds" (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "PA")))) "holds" (Bool (Set (Var "b")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PB")))))) ; theorem :: PARTIT1:7 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Var "Y")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PA"))))) ; theorem :: PARTIT1:8 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "F"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "X")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PA"))) ")" )) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "F"))) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PA")))))) ; theorem :: PARTIT1:9 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "X0")) "," (Set (Var "X1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X0")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PA"))) & (Bool (Set (Var "X1")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PA"))) & (Bool (Set (Var "X0")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "X1")))) "holds" (Bool (Set (Set (Var "X0")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "X1"))) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PA")))))) ; theorem :: PARTIT1:10 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PA"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PA")))))) ; theorem :: PARTIT1:11 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r2_partit1 :::"is_min_depend"::: ) (Set (Var "PA")) "," (Set (Var "PB"))) ")" ))))) ; theorem :: PARTIT1:12 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) ")" ))))) ; definitionlet "Y" be ($#m1_hidden :::"set"::: ) ; func :::"PARTITIONS"::: "Y" -> ($#m1_hidden :::"set"::: ) means :: PARTIT1:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" "Y") ")" )); end; :: deftheorem defines :::"PARTITIONS"::: PARTIT1:def 3 : (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y"))) ")" )) ")" ))); registrationlet "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_partit1 :::"PARTITIONS"::: ) "Y") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; begin definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "PA", "PB" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")); func "PA" :::"'/\'"::: "PB" -> ($#m1_eqrel_1 :::"a_partition"::: ) "of" "Y" equals :: PARTIT1:def 4 (Set (Set "(" ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" "PA" "," "PB" ")" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "PA")) "," (Set (Var "PB")) ")" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "PB")) "," (Set (Var "PA")) ")" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; end; :: deftheorem defines :::"'/\'"::: PARTIT1:def 4 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "PA")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "PB"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "PA")) "," (Set (Var "PB")) ")" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))))); theorem :: PARTIT1:13 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "PA")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "PA"))) ($#r1_hidden :::"="::: ) (Set (Var "PA"))))) ; theorem :: PARTIT1:14 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "," (Set (Var "PC")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set "(" (Set (Var "PA")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "PB")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "PC"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "PA")) ($#k2_partit1 :::"'/\'"::: ) (Set "(" (Set (Var "PB")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "PC")) ")" ))))) ; theorem :: PARTIT1:15 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Var "PA")) ($#r1_setfam_1 :::"'>'"::: ) (Set (Set (Var "PA")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "PB")))))) ; definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "PA", "PB" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")); func "PA" :::"'\/'"::: "PB" -> ($#m1_eqrel_1 :::"a_partition"::: ) "of" "Y" means :: PARTIT1:def 5 (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "d")) ($#r2_partit1 :::"is_min_depend"::: ) "PA" "," "PB") ")" )); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")) "st" (Bool (Bool "(" "for" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool (Set (Var "d")) ($#r2_partit1 :::"is_min_depend"::: ) (Set (Var "PA")) "," (Set (Var "PB"))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool (Set (Var "d")) ($#r2_partit1 :::"is_min_depend"::: ) (Set (Var "PB")) "," (Set (Var "PA"))) ")" ))) ; end; :: deftheorem defines :::"'\/'"::: PARTIT1:def 5 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "," (Set (Var "b4")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "PA")) ($#k3_partit1 :::"'\/'"::: ) (Set (Var "PB")))) "iff" (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool (Set (Var "d")) ($#r2_partit1 :::"is_min_depend"::: ) (Set (Var "PA")) "," (Set (Var "PB"))) ")" )) ")" ))); theorem :: PARTIT1:16 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Var "PA")) ($#r1_setfam_1 :::"'<'"::: ) (Set (Set (Var "PA")) ($#k3_partit1 :::"'\/'"::: ) (Set (Var "PB")))))) ; theorem :: PARTIT1:17 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "PA")) ($#k3_partit1 :::"'\/'"::: ) (Set (Var "PA"))) ($#r1_hidden :::"="::: ) (Set (Var "PA"))))) ; theorem :: PARTIT1:18 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "z0")) "," (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PC")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "PA")) ($#r1_setfam_1 :::"'<'"::: ) (Set (Var "PC"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "PC"))) & (Bool (Set (Var "z0")) ($#r2_hidden :::"in"::: ) (Set (Var "PA"))) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "z0")))) "holds" (Bool (Set (Var "z0")) ($#r1_tarski :::"c="::: ) (Set (Var "x")))))) ; theorem :: PARTIT1:19 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "z0")) "," (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "PA")) ($#k3_partit1 :::"'\/'"::: ) (Set (Var "PB")))) & (Bool (Set (Var "z0")) ($#r2_hidden :::"in"::: ) (Set (Var "PA"))) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "z0")))) "holds" (Bool (Set (Var "z0")) ($#r1_tarski :::"c="::: ) (Set (Var "x")))))) ; begin definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "PA" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")); func :::"ERl"::: "PA" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "Y" means :: PARTIT1:def 6 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "PA") & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" )); end; :: deftheorem defines :::"ERl"::: PARTIT1:def 6 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_partit1 :::"ERl"::: ) (Set (Var "PA")))) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "PA"))) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" )) ")" )))); definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"Rel"::: "Y" -> ($#m1_hidden :::"Function":::) means :: PARTIT1:def 7 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_partit1 :::"PARTITIONS"::: ) "Y")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_partit1 :::"PARTITIONS"::: ) "Y"))) "holds" (Bool "ex" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" "Y" "st" (Bool "(" (Bool (Set (Var "PA")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_partit1 :::"ERl"::: ) (Set (Var "PA")))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"Rel"::: PARTIT1:def 7 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_partit1 :::"Rel"::: ) (Set (Var "Y")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "Y"))))) "holds" (Bool "ex" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "PA")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_partit1 :::"ERl"::: ) (Set (Var "PA")))) ")" )) ")" ) ")" ) ")" ))); theorem :: PARTIT1:20 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "PA")) ($#r1_setfam_1 :::"'<'"::: ) (Set (Var "PB"))) "iff" (Bool (Set ($#k4_partit1 :::"ERl"::: ) (Set (Var "PA"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_partit1 :::"ERl"::: ) (Set (Var "PB")))) ")" ))) ; theorem :: PARTIT1:21 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "p0")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "p0")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "p0"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "u")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "PA"))) & (Bool (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set (Var "PB"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Var "p2"))) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "p2"))) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "p3"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "p3"))) ")" )) ")" ) & (Bool (Set (Var "p0")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PA"))) & (Bool (Set (Var "p0")) ($#r1_partit1 :::"is_a_dependent_set_of"::: ) (Set (Var "PB")))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "p0"))))))) ; theorem :: PARTIT1:22 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R1")) ($#k3_eqrel_1 :::"\/"::: ) (Set (Var "R2")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "u")) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R1")) ($#k3_eqrel_1 :::"\/"::: ) (Set (Var "R2")))) ")" )) ")" )) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R1")) ($#k5_eqrel_1 :::""\/""::: ) (Set (Var "R2")))))))) ; theorem :: PARTIT1:23 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k4_partit1 :::"ERl"::: ) (Set "(" (Set (Var "PA")) ($#k3_partit1 :::"'\/'"::: ) (Set (Var "PB")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_partit1 :::"ERl"::: ) (Set (Var "PA")) ")" ) ($#k5_eqrel_1 :::""\/""::: ) (Set "(" ($#k4_partit1 :::"ERl"::: ) (Set (Var "PB")) ")" ))))) ; theorem :: PARTIT1:24 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k4_partit1 :::"ERl"::: ) (Set "(" (Set (Var "PA")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "PB")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_partit1 :::"ERl"::: ) (Set (Var "PA")) ")" ) ($#k4_eqrel_1 :::"/\"::: ) (Set "(" ($#k4_partit1 :::"ERl"::: ) (Set (Var "PB")) ")" ))))) ; theorem :: PARTIT1:25 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set ($#k4_partit1 :::"ERl"::: ) (Set (Var "PA"))) ($#r1_hidden :::"="::: ) (Set ($#k4_partit1 :::"ERl"::: ) (Set (Var "PB"))))) "holds" (Bool (Set (Var "PA")) ($#r1_hidden :::"="::: ) (Set (Var "PB"))))) ; theorem :: PARTIT1:26 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "," (Set (Var "PC")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set "(" (Set (Var "PA")) ($#k3_partit1 :::"'\/'"::: ) (Set (Var "PB")) ")" ) ($#k3_partit1 :::"'\/'"::: ) (Set (Var "PC"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "PA")) ($#k3_partit1 :::"'\/'"::: ) (Set "(" (Set (Var "PB")) ($#k3_partit1 :::"'\/'"::: ) (Set (Var "PC")) ")" ))))) ; theorem :: PARTIT1:27 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "PA")) ($#k2_partit1 :::"'/\'"::: ) (Set "(" (Set (Var "PA")) ($#k3_partit1 :::"'\/'"::: ) (Set (Var "PB")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "PA"))))) ; theorem :: PARTIT1:28 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "PA")) ($#k3_partit1 :::"'\/'"::: ) (Set "(" (Set (Var "PA")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "PB")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "PA"))))) ; theorem :: PARTIT1:29 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "," (Set (Var "PC")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "PA")) ($#r1_setfam_1 :::"'<'"::: ) (Set (Var "PC"))) & (Bool (Set (Var "PB")) ($#r1_setfam_1 :::"'<'"::: ) (Set (Var "PC")))) "holds" (Bool (Set (Set (Var "PA")) ($#k3_partit1 :::"'\/'"::: ) (Set (Var "PB"))) ($#r1_setfam_1 :::"'<'"::: ) (Set (Var "PC"))))) ; theorem :: PARTIT1:30 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "," (Set (Var "PB")) "," (Set (Var "PC")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "PA")) ($#r1_setfam_1 :::"'>'"::: ) (Set (Var "PC"))) & (Bool (Set (Var "PB")) ($#r1_setfam_1 :::"'>'"::: ) (Set (Var "PC")))) "holds" (Bool (Set (Set (Var "PA")) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "PB"))) ($#r1_setfam_1 :::"'>'"::: ) (Set (Var "PC"))))) ; notationlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; synonym :::"%I"::: "Y" for :::"SmallestPartition"::: "Y"; end; definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"%O"::: "Y" -> ($#m1_eqrel_1 :::"a_partition"::: ) "of" "Y" equals :: PARTIT1:def 8 (Set ($#k1_tarski :::"{"::: ) "Y" ($#k1_tarski :::"}"::: ) ); end; :: deftheorem defines :::"%O"::: PARTIT1:def 8 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_partit1 :::"%O"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "Y")) ($#k1_tarski :::"}"::: ) ))); theorem :: PARTIT1:31 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_eqrel_1 :::"%I"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) : (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) "}" )) ; theorem :: PARTIT1:32 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set ($#k6_partit1 :::"%O"::: ) (Set (Var "Y"))) ($#r1_setfam_1 :::"'>'"::: ) (Set (Var "PA"))) & (Bool (Set (Var "PA")) ($#r1_setfam_1 :::"'>'"::: ) (Set ($#k10_eqrel_1 :::"%I"::: ) (Set (Var "Y")))) ")" ))) ; theorem :: PARTIT1:33 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_partit1 :::"ERl"::: ) (Set "(" ($#k6_partit1 :::"%O"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "Y"))))) ; theorem :: PARTIT1:34 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_partit1 :::"ERl"::: ) (Set "(" ($#k10_eqrel_1 :::"%I"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "Y"))))) ; theorem :: PARTIT1:35 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_eqrel_1 :::"%I"::: ) (Set (Var "Y"))) ($#r1_setfam_1 :::"'<'"::: ) (Set ($#k6_partit1 :::"%O"::: ) (Set (Var "Y"))))) ; theorem :: PARTIT1:36 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_partit1 :::"%O"::: ) (Set (Var "Y")) ")" ) ($#k3_partit1 :::"'\/'"::: ) (Set (Var "PA"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partit1 :::"%O"::: ) (Set (Var "Y")))) & (Bool (Set (Set "(" ($#k6_partit1 :::"%O"::: ) (Set (Var "Y")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "PA"))) ($#r1_hidden :::"="::: ) (Set (Var "PA"))) ")" ))) ; theorem :: PARTIT1:37 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k10_eqrel_1 :::"%I"::: ) (Set (Var "Y")) ")" ) ($#k3_partit1 :::"'\/'"::: ) (Set (Var "PA"))) ($#r1_hidden :::"="::: ) (Set (Var "PA"))) & (Bool (Set (Set "(" ($#k10_eqrel_1 :::"%I"::: ) (Set (Var "Y")) ")" ) ($#k2_partit1 :::"'/\'"::: ) (Set (Var "PA"))) ($#r1_hidden :::"="::: ) (Set ($#k10_eqrel_1 :::"%I"::: ) (Set (Var "Y")))) ")" ))) ;