:: SIMPLEX0 semantic presentation begin notationlet "X" be ($#m1_hidden :::"set"::: ) ; antonym :::"with_empty_element"::: "X" for :::"with_non-empty_elements"::: ; end; registration cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v1_classes1 :::"subset-closed"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_setfam_1 :::"with_empty_element"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) -> ($#v1_setfam_1 :::"with_empty_element"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_cohsp_1 :::"Sub_of_Fin"::: ) "X") -> ($#v5_finset_1 :::"finite-membered"::: ) ; end; registrationlet "X" be ($#v1_classes1 :::"subset-closed"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_cohsp_1 :::"Sub_of_Fin"::: ) "X") -> ($#v1_classes1 :::"subset-closed"::: ) ; end; theorem :: SIMPLEX0:1 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v1_classes1 :::"subset-closed"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) ")" )) ; registrationlet "A", "B" be ($#v1_classes1 :::"subset-closed"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k2_xboole_0 :::"\/"::: ) "B") -> ($#v1_classes1 :::"subset-closed"::: ) ; cluster (Set "A" ($#k3_xboole_0 :::"/\"::: ) "B") -> ($#v1_classes1 :::"subset-closed"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"subset-closed_closure_of"::: "X" -> ($#v1_classes1 :::"subset-closed"::: ) ($#m1_hidden :::"set"::: ) means :: SIMPLEX0:def 1 (Bool "(" (Bool "X" ($#r1_tarski :::"c="::: ) it) & (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "X" ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) "is" ($#v1_classes1 :::"subset-closed"::: ) )) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ); end; :: deftheorem defines :::"subset-closed_closure_of"::: SIMPLEX0:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v1_classes1 :::"subset-closed"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_simplex0 :::"subset-closed_closure_of"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "b2"))) & (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) "is" ($#v1_classes1 :::"subset-closed"::: ) )) "holds" (Bool (Set (Var "b2")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ) ")" ))); theorem :: SIMPLEX0:2 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_simplex0 :::"subset-closed_closure_of"::: ) (Set (Var "X")))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ")" )) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); :: original: :::"subset-closed_closure_of"::: redefine func :::"subset-closed_closure_of"::: "F" -> ($#v1_classes1 :::"subset-closed"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" "X"; end; registration cluster (Set ($#k1_simplex0 :::"subset-closed_closure_of"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) -> ($#v1_xboole_0 :::"empty"::: ) ($#v1_classes1 :::"subset-closed"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_simplex0 :::"subset-closed_closure_of"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) ; end; registrationlet "X" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_simplex0 :::"subset-closed_closure_of"::: ) "X") -> ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#v1_classes1 :::"subset-closed"::: ) ; end; registrationlet "X" be ($#v5_finset_1 :::"finite-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_simplex0 :::"subset-closed_closure_of"::: ) "X") -> ($#v5_finset_1 :::"finite-membered"::: ) ($#v1_classes1 :::"subset-closed"::: ) ; end; theorem :: SIMPLEX0:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) "is" ($#v1_classes1 :::"subset-closed"::: ) )) "holds" (Bool (Set ($#k1_simplex0 :::"subset-closed_closure_of"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) ; theorem :: SIMPLEX0:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_simplex0 :::"subset-closed_closure_of"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))))) ; theorem :: SIMPLEX0:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_simplex0 :::"subset-closed_closure_of"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_simplex0 :::"subset-closed_closure_of"::: ) (Set (Var "X")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k1_simplex0 :::"subset-closed_closure_of"::: ) (Set (Var "Y")) ")" )))) ; theorem :: SIMPLEX0:6 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "Y"))) "iff" (Bool (Set ($#k1_simplex0 :::"subset-closed_closure_of"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_simplex0 :::"subset-closed_closure_of"::: ) (Set (Var "Y")))) ")" )) ; theorem :: SIMPLEX0:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_classes1 :::"subset-closed"::: ) )) "holds" (Bool (Set ($#k1_simplex0 :::"subset-closed_closure_of"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) ; theorem :: SIMPLEX0:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_simplex0 :::"subset-closed_closure_of"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "X")) "is" ($#v1_classes1 :::"subset-closed"::: ) )) ; definitionlet "Y", "X", "n" be ($#m1_hidden :::"set"::: ) ; func :::"the_subsets_with_limited_card"::: "(" "n" "," "X" "," "Y" ")" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "Y" means :: SIMPLEX0:def 2 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) "n")) ")" ) ")" )); end; :: deftheorem defines :::"the_subsets_with_limited_card"::: SIMPLEX0:def 2 : (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "," (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_simplex0 :::"the_subsets_with_limited_card"::: ) "(" (Set (Var "n")) "," (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "n")))) ")" ) ")" )) ")" ))); registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v5_finset_1 :::"finite-membered"::: ) ($#v1_classes1 :::"subset-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "D" ")" )); end; registrationlet "Y", "X" be ($#m1_hidden :::"set"::: ) ; let "n" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_simplex0 :::"the_subsets_with_limited_card"::: ) "(" "n" "," "X" "," "Y" ")" ) -> ($#v5_finset_1 :::"finite-membered"::: ) ; end; registrationlet "Y" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#v1_classes1 :::"subset-closed"::: ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_simplex0 :::"the_subsets_with_limited_card"::: ) "(" "n" "," "X" "," "Y" ")" ) -> ($#v1_classes1 :::"subset-closed"::: ) ; end; registrationlet "Y" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#v1_setfam_1 :::"with_empty_element"::: ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_simplex0 :::"the_subsets_with_limited_card"::: ) "(" "n" "," "X" "," "Y" ")" ) -> ($#v1_setfam_1 :::"with_empty_element"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#v1_classes1 :::"subset-closed"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "D")); let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_simplex0 :::"the_subsets_with_limited_card"::: ) "(" "n" "," "X" "," "D" ")" ) -> ($#v2_setfam_1 :::"with_non-empty_element"::: ) ; end; notationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); let "n" be ($#m1_hidden :::"set"::: ) ; synonym :::"the_subsets_with_limited_card"::: "(" "n" "," "Y" ")" for :::"the_subsets_with_limited_card"::: "(" "n" "," "Y" "," "X" ")" ; end; theorem :: SIMPLEX0:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "X")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "X")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ; theorem :: SIMPLEX0:10 (Bool "for" (Set (Var "X")) "being" ($#v6_ordinal1 :::"c=-linear"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) )) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "X")) ")" )))) ; theorem :: SIMPLEX0:11 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "X")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "x")) ")" ) ($#k1_tarski :::"}"::: ) )) "is" ($#v6_ordinal1 :::"c=-linear"::: ) )) ; theorem :: SIMPLEX0:12 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) ) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "Y")))) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "Z"))) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z"))) & (Bool (Set (Set (Var "Z")) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" ) ")" ))) ; theorem :: SIMPLEX0:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) ) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool "ex" (Set (Var "Y1")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Y1"))) & (Bool (Set (Var "Y1")) "is" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ) & (Bool (Set (Var "Y1")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) ) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "Y1")))) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "Y1"))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "Z"))) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z"))) & (Bool (Set (Set (Var "Z")) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "Y1"))) ")" )) ")" ) ")" )))) ; begin definitionmode SimplicialComplexStr is ($#l1_pre_topc :::"TopStruct"::: ) ; end; notationlet "K" be ($#l1_pre_topc :::"SimplicialComplexStr":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "K")); synonym :::"simplex-like"::: "A" for :::"open"::: ; end; notationlet "K" be ($#l1_pre_topc :::"SimplicialComplexStr":::); let "S" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "K")); synonym :::"simplex-like"::: "S" for :::"open"::: ; end; registrationlet "K" be ($#l1_pre_topc :::"SimplicialComplexStr":::); cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_tops_2 :::"simplex-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ")" )); end; theorem :: SIMPLEX0:14 (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_tops_2 :::"simplex-like"::: ) ) "iff" (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "K")))) ")" ))) ; definitionlet "K" be ($#l1_pre_topc :::"SimplicialComplexStr":::); let "v" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); attr "v" is :::"vertex-like"::: means :: SIMPLEX0:def 3 (Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" "K" "st" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"simplex-like"::: ) ) & (Bool "v" ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" )); end; :: deftheorem defines :::"vertex-like"::: SIMPLEX0:def 3 : (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "v")) "is" ($#v1_simplex0 :::"vertex-like"::: ) ) "iff" (Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "K")) "st" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"simplex-like"::: ) ) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" )) ")" ))); definitionlet "K" be ($#l1_pre_topc :::"SimplicialComplexStr":::); func :::"Vertices"::: "K" -> ($#m1_subset_1 :::"Subset":::) "of" "K" means :: SIMPLEX0:def 4 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "K" "holds" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "v")) "is" ($#v1_simplex0 :::"vertex-like"::: ) ) ")" )); end; :: deftheorem defines :::"Vertices"::: SIMPLEX0:def 4 : (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_simplex0 :::"Vertices"::: ) (Set (Var "K")))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "v")) "is" ($#v1_simplex0 :::"vertex-like"::: ) ) ")" )) ")" ))); definitionlet "K" be ($#l1_pre_topc :::"SimplicialComplexStr":::); mode Vertex of "K" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_simplex0 :::"Vertices"::: ) "K"); end; definitionlet "K" be ($#l1_pre_topc :::"SimplicialComplexStr":::); attr "K" is :::"finite-vertices"::: means :: SIMPLEX0:def 5 (Bool (Set ($#k4_simplex0 :::"Vertices"::: ) "K") "is" ($#v1_finset_1 :::"finite"::: ) ); end; :: deftheorem defines :::"finite-vertices"::: SIMPLEX0:def 5 : (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) "holds" (Bool "(" (Bool (Set (Var "K")) "is" ($#v2_simplex0 :::"finite-vertices"::: ) ) "iff" (Bool (Set ($#k4_simplex0 :::"Vertices"::: ) (Set (Var "K"))) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" )); definitionlet "K" be ($#l1_pre_topc :::"SimplicialComplexStr":::); attr "K" is :::"locally-finite"::: means :: SIMPLEX0:def 6 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "K" "holds" (Bool "{" (Set (Var "S")) where S "is" ($#m1_subset_1 :::"Subset":::) "of" "K" : (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"simplex-like"::: ) ) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ) "}" "is" ($#v1_finset_1 :::"finite"::: ) )); end; :: deftheorem defines :::"locally-finite"::: SIMPLEX0:def 6 : (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) "holds" (Bool "(" (Bool (Set (Var "K")) "is" ($#v3_simplex0 :::"locally-finite"::: ) ) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "K")) "holds" (Bool "{" (Set (Var "S")) where S "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "K")) : (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"simplex-like"::: ) ) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ) "}" "is" ($#v1_finset_1 :::"finite"::: ) )) ")" )); definitionlet "K" be ($#l1_pre_topc :::"SimplicialComplexStr":::); attr "K" is :::"empty-membered"::: means :: SIMPLEX0:def 7 (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "K") "is" ($#v2_setfam_1 :::"empty-membered"::: ) ); attr "K" is :::"with_non-empty_elements"::: means :: SIMPLEX0:def 8 (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "K") "is" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ); end; :: deftheorem defines :::"empty-membered"::: SIMPLEX0:def 7 : (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) "holds" (Bool "(" (Bool (Set (Var "K")) "is" ($#v4_simplex0 :::"empty-membered"::: ) ) "iff" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "K"))) "is" ($#v2_setfam_1 :::"empty-membered"::: ) ) ")" )); :: deftheorem defines :::"with_non-empty_elements"::: SIMPLEX0:def 8 : (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) "holds" (Bool "(" (Bool (Set (Var "K")) "is" ($#v5_simplex0 :::"with_non-empty_elements"::: ) ) "iff" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "K"))) "is" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ) ")" )); notationlet "K" be ($#l1_pre_topc :::"SimplicialComplexStr":::); antonym :::"with_non-empty_element"::: "K" for :::"empty-membered"::: ; antonym :::"with_empty_element"::: "K" for :::"with_non-empty_elements"::: ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode :::"SimplicialComplexStr"::: "of" "X" -> ($#l1_pre_topc :::"SimplicialComplexStr":::) means :: SIMPLEX0:def 9 (Bool (Set ($#k2_struct_0 :::"[#]"::: ) it) ($#r1_tarski :::"c="::: ) "X"); end; :: deftheorem defines :::"SimplicialComplexStr"::: SIMPLEX0:def 9 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); attr "KX" is :::"total"::: means :: SIMPLEX0:def 10 (Bool (Set ($#k2_struct_0 :::"[#]"::: ) "KX") ($#r1_hidden :::"="::: ) "X"); end; :: deftheorem defines :::"total"::: SIMPLEX0:def 10 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "KX")) "is" ($#v6_simplex0 :::"total"::: ) ) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "KX"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" ))); registration cluster ($#v5_simplex0 :::"with_empty_element"::: ) -> ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v4_simplex0 :::"with_non-empty_element"::: ) -> ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v4_simplex0 :::"empty-membered"::: ) -> ($#v5_simplex0 :::"with_empty_element"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) -> ($#v5_simplex0 :::"with_empty_element"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v4_simplex0 :::"empty-membered"::: ) -> ($#v1_matroid0 :::"subset-closed"::: ) ($#v2_simplex0 :::"finite-vertices"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v2_simplex0 :::"finite-vertices"::: ) -> ($#v4_matroid0 :::"finite-degree"::: ) ($#v3_simplex0 :::"locally-finite"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v1_matroid0 :::"subset-closed"::: ) ($#v3_simplex0 :::"locally-finite"::: ) -> ($#v3_matroid0 :::"finite-membered"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v2_struct_0 :::"empty"::: ) ($#v1_pre_topc :::"strict"::: ) ($#v3_pencil_1 :::"void"::: ) ($#v4_simplex0 :::"empty-membered"::: ) for ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" "X"; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v4_simplex0 :::"empty-membered"::: ) ($#v6_simplex0 :::"total"::: ) for ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" "D"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_matroid0 :::"subset-closed"::: ) ($#v2_simplex0 :::"finite-vertices"::: ) ($#v4_simplex0 :::"with_non-empty_element"::: ) ($#v5_simplex0 :::"with_empty_element"::: ) ($#v6_simplex0 :::"total"::: ) for ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" "D"; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_matroid0 :::"subset-closed"::: ) ($#v2_simplex0 :::"finite-vertices"::: ) ($#v4_simplex0 :::"with_non-empty_element"::: ) ($#v5_simplex0 :::"with_empty_element"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "K" be ($#v4_simplex0 :::"with_non-empty_element"::: ) ($#l1_pre_topc :::"SimplicialComplexStr":::); cluster (Set ($#k4_simplex0 :::"Vertices"::: ) "K") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "K" be ($#v2_simplex0 :::"finite-vertices"::: ) ($#l1_pre_topc :::"SimplicialComplexStr":::); cluster ($#v1_tops_2 :::"simplex-like"::: ) -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ")" )); end; registrationlet "K" be ($#v3_matroid0 :::"finite-membered"::: ) ($#l1_pre_topc :::"SimplicialComplexStr":::); cluster ($#v1_tops_2 :::"simplex-like"::: ) -> ($#v5_finset_1 :::"finite-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ")" )); end; theorem :: SIMPLEX0:15 (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) "holds" (Bool "(" (Bool (Set ($#k4_simplex0 :::"Vertices"::: ) (Set (Var "K"))) "is" ($#v1_xboole_0 :::"empty"::: ) ) "iff" (Bool (Set (Var "K")) "is" ($#v4_simplex0 :::"empty-membered"::: ) ) ")" )) ; theorem :: SIMPLEX0:16 (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) "holds" (Bool (Set ($#k4_simplex0 :::"Vertices"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "K")))))) ; theorem :: SIMPLEX0:17 (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"simplex-like"::: ) )) "holds" (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set ($#k4_simplex0 :::"Vertices"::: ) (Set (Var "K")))))) ; theorem :: SIMPLEX0:18 (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) "st" (Bool (Bool (Set (Var "K")) "is" ($#v2_simplex0 :::"finite-vertices"::: ) )) "holds" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "K"))) "is" ($#v1_finset_1 :::"finite"::: ) )) ; theorem :: SIMPLEX0:19 (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) "st" (Bool (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "K"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Bool "not" (Set (Var "K")) "is" ($#v2_simplex0 :::"finite-vertices"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "K")) "is" ($#v3_matroid0 :::"finite-membered"::: ) ))) ; theorem :: SIMPLEX0:20 (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) "st" (Bool (Bool (Set (Var "K")) "is" ($#v1_matroid0 :::"subset-closed"::: ) ) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "K"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Var "K")) "is" ($#v2_simplex0 :::"finite-vertices"::: ) )) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); func :::"Complex_of"::: "Y" -> ($#v1_pre_topc :::"strict"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" "X" equals :: SIMPLEX0:def 11 (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" "X" "," (Set "(" ($#k2_simplex0 :::"subset-closed_closure_of"::: ) "Y" ")" ) "#)" ); end; :: deftheorem defines :::"Complex_of"::: SIMPLEX0:def 11 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k5_simplex0 :::"Complex_of"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set (Var "X")) "," (Set "(" ($#k2_simplex0 :::"subset-closed_closure_of"::: ) (Set (Var "Y")) ")" ) "#)" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); cluster (Set ($#k5_simplex0 :::"Complex_of"::: ) "Y") -> ($#v1_pre_topc :::"strict"::: ) ($#v1_matroid0 :::"subset-closed"::: ) ($#v6_simplex0 :::"total"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); cluster (Set ($#k5_simplex0 :::"Complex_of"::: ) "Y") -> ($#v1_pre_topc :::"strict"::: ) ($#v5_simplex0 :::"with_empty_element"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v5_finset_1 :::"finite-membered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); cluster (Set ($#k5_simplex0 :::"Complex_of"::: ) "Y") -> ($#v1_pre_topc :::"strict"::: ) ($#v3_matroid0 :::"finite-membered"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_finset_1 :::"finite"::: ) ($#v5_finset_1 :::"finite-membered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); cluster (Set ($#k5_simplex0 :::"Complex_of"::: ) "Y") -> ($#v1_pre_topc :::"strict"::: ) ($#v2_simplex0 :::"finite-vertices"::: ) ; end; theorem :: SIMPLEX0:21 (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) "st" (Bool (Bool (Set (Var "K")) "is" ($#v1_matroid0 :::"subset-closed"::: ) )) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "K"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k5_simplex0 :::"Complex_of"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "K")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode SimplicialComplex of "X" is ($#v1_matroid0 :::"subset-closed"::: ) ($#v3_matroid0 :::"finite-membered"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" "X"; end; definitionlet "K" be ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#l1_pre_topc :::"SimplicialComplexStr":::); mode Simplex of "K" is ($#v3_pre_topc :::"simplex-like"::: ) ($#m1_subset_1 :::"Subset":::) "of" "K"; end; registrationlet "K" be ($#v5_simplex0 :::"with_empty_element"::: ) ($#l1_pre_topc :::"SimplicialComplexStr":::); cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v3_pre_topc :::"simplex-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")); cluster ($#v1_xboole_0 :::"empty"::: ) ($#v3_pre_topc :::"simplex-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")); end; registrationlet "K" be ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v3_matroid0 :::"finite-membered"::: ) ($#l1_pre_topc :::"SimplicialComplexStr":::); cluster ($#v1_finset_1 :::"finite"::: ) ($#v3_pre_topc :::"simplex-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")); end; begin definitionlet "K" be ($#l1_pre_topc :::"SimplicialComplexStr":::); func :::"degree"::: "K" -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) means :: SIMPLEX0:def 12 (Bool "(" (Bool "(" "for" (Set (Var "S")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "K" "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"simplex-like"::: ) )) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "S"))) ($#r1_xxreal_0 :::"<="::: ) (Set it ($#k1_xxreal_3 :::"+"::: ) (Num 1))) ")" ) & (Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" "K" "st" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"simplex-like"::: ) ) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set it ($#k1_xxreal_3 :::"+"::: ) (Num 1))) ")" )) ")" ) if (Bool "(" (Bool (Bool "not" "K" "is" ($#v3_pencil_1 :::"void"::: ) )) & (Bool "K" "is" ($#v4_matroid0 :::"finite-degree"::: ) ) ")" ) (Bool it ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_3 :::"-"::: ) (Num 1))) if (Bool "K" "is" ($#v3_pencil_1 :::"void"::: ) ) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) )); end; :: deftheorem defines :::"degree"::: SIMPLEX0:def 12 : (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "K")) "is" ($#v3_pencil_1 :::"void"::: ) )) & (Bool (Set (Var "K")) "is" ($#v4_matroid0 :::"finite-degree"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "K")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "S")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"simplex-like"::: ) )) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "S"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "b2")) ($#k1_xxreal_3 :::"+"::: ) (Num 1))) ")" ) & (Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "K")) "st" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"simplex-like"::: ) ) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k1_xxreal_3 :::"+"::: ) (Num 1))) ")" )) ")" ) ")" ) ")" & "(" (Bool (Bool (Set (Var "K")) "is" ($#v3_pencil_1 :::"void"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "K")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_3 :::"-"::: ) (Num 1))) ")" ) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "K")) "is" ($#v3_pencil_1 :::"void"::: ) ) "or" "not" (Bool (Set (Var "K")) "is" ($#v4_matroid0 :::"finite-degree"::: ) ) ")" ) & (Bool (Bool "not" (Set (Var "K")) "is" ($#v3_pencil_1 :::"void"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "K")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) )) ")" ) ")" ")" ))); registrationlet "K" be ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"SimplicialComplexStr":::); cluster (Set (Set "(" ($#k6_simplex0 :::"degree"::: ) "K" ")" ) ($#k1_xxreal_3 :::"+"::: ) (Num 1)) -> ($#v7_ordinal1 :::"natural"::: ) ; cluster (Set ($#k6_simplex0 :::"degree"::: ) "K") -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#v1_int_1 :::"integer"::: ) ; end; theorem :: SIMPLEX0:22 (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) "holds" (Bool "(" (Bool (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_3 :::"-"::: ) (Num 1))) "iff" (Bool (Set (Var "K")) "is" ($#v4_simplex0 :::"empty-membered"::: ) ) ")" )) ; theorem :: SIMPLEX0:23 (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) "holds" (Bool (Set ($#k2_xxreal_3 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "K"))))) ; theorem :: SIMPLEX0:24 (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) (Bool "for" (Set (Var "S")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"simplex-like"::: ) )) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "S"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k6_simplex0 :::"degree"::: ) (Set (Var "K")) ")" ) ($#k1_xxreal_3 :::"+"::: ) (Num 1))))) ; theorem :: SIMPLEX0:25 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "K")) "being" ($#l1_pre_topc :::"SimplicialComplexStr":::) "st" (Bool (Bool "(" "not" (Bool (Set (Var "K")) "is" ($#v3_pencil_1 :::"void"::: ) ) "or" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k2_xxreal_3 :::"-"::: ) (Num 1))) ")" )) "holds" (Bool "(" (Bool (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "K"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) "iff" (Bool "(" (Bool (Set (Var "K")) "is" ($#v3_matroid0 :::"finite-membered"::: ) ) & (Bool "(" "for" (Set (Var "S")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"simplex-like"::: ) )) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "S"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "i")) ($#k1_xxreal_3 :::"+"::: ) (Num 1))) ")" ) ")" ) ")" ))) ; theorem :: SIMPLEX0:26 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k6_simplex0 :::"degree"::: ) (Set "(" ($#k5_simplex0 :::"Complex_of"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "A")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "A")) ")" ) ($#k3_xxreal_3 :::"-"::: ) (Num 1))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); mode :::"SubSimplicialComplex"::: "of" "KX" -> ($#m1_simplex0 :::"SimplicialComplex":::) "of" "X" means :: SIMPLEX0:def 13 (Bool "(" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) it) ($#r1_tarski :::"c="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) "KX")) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "KX")) ")" ); end; :: deftheorem defines :::"SubSimplicialComplex"::: SIMPLEX0:def 13 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_simplex0 :::"SimplicialComplex":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX"))) "iff" (Bool "(" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "b3"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "KX")))) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "b3"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "KX")))) ")" ) ")" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); cluster ($#v2_struct_0 :::"empty"::: ) ($#v1_pre_topc :::"strict"::: ) ($#v3_pencil_1 :::"void"::: ) ($#v1_matroid0 :::"subset-closed"::: ) ($#v3_matroid0 :::"finite-membered"::: ) for ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" "KX"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#v3_pencil_1 :::"void"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); cluster -> ($#v3_pencil_1 :::"void"::: ) for ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" "KX"; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "KD" be ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "D")); cluster ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#v3_matroid0 :::"finite-membered"::: ) for ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" "KD"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#v2_simplex0 :::"finite-vertices"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); cluster -> ($#v2_simplex0 :::"finite-vertices"::: ) for ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" "KX"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#v4_matroid0 :::"finite-degree"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); cluster -> ($#v4_matroid0 :::"finite-degree"::: ) for ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" "KX"; end; theorem :: SIMPLEX0:27 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "SX")) "being" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX")) (Bool "for" (Set (Var "S1")) "being" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "SX")) "holds" (Bool (Set (Var "S1")) "is" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX"))))))) ; theorem :: SIMPLEX0:28 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "KX")) (Bool "for" (Set (Var "S")) "being" ($#v5_finset_1 :::"finite-membered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k2_simplex0 :::"subset-closed_closure_of"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "KX"))))) "holds" (Bool (Set ($#k5_simplex0 :::"Complex_of"::: ) (Set (Var "S"))) "is" ($#v1_pre_topc :::"strict"::: ) ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX"))))))) ; theorem :: SIMPLEX0:29 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#v1_matroid0 :::"subset-closed"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "KX")) (Bool "for" (Set (Var "S")) "being" ($#v5_finset_1 :::"finite-membered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "KX"))))) "holds" (Bool (Set ($#k5_simplex0 :::"Complex_of"::: ) (Set (Var "S"))) "is" ($#v1_pre_topc :::"strict"::: ) ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX"))))))) ; theorem :: SIMPLEX0:30 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y1")) "is" ($#v5_finset_1 :::"finite-membered"::: ) ) & (Bool (Set (Var "Y1")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "Y2")))) "holds" (Bool (Set ($#k5_simplex0 :::"Complex_of"::: ) (Set (Var "Y1"))) "is" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set ($#k5_simplex0 :::"Complex_of"::: ) (Set (Var "Y2")))))) ; theorem :: SIMPLEX0:31 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "SX")) "being" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX")) "holds" (Bool (Set ($#k4_simplex0 :::"Vertices"::: ) (Set (Var "SX"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_simplex0 :::"Vertices"::: ) (Set (Var "KX"))))))) ; theorem :: SIMPLEX0:32 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "SX")) "being" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX")) "holds" (Bool (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "SX"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "KX"))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); let "SX" be ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Const "KX")); attr "SX" is :::"maximal"::: means :: SIMPLEX0:def 14 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "SX" "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "KX"))) "holds" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"simplex-like"::: ) )); end; :: deftheorem defines :::"maximal"::: SIMPLEX0:def 14 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "SX")) "being" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX")) "holds" (Bool "(" (Bool (Set (Var "SX")) "is" ($#v7_simplex0 :::"maximal"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "SX")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "KX"))))) "holds" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"simplex-like"::: ) )) ")" )))); theorem :: SIMPLEX0:33 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "SX")) "being" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX")) "holds" (Bool "(" (Bool (Set (Var "SX")) "is" ($#v7_simplex0 :::"maximal"::: ) ) "iff" (Bool (Set (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "SX")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "KX")))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "SX")))) ")" )))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); cluster ($#v1_pre_topc :::"strict"::: ) ($#v1_matroid0 :::"subset-closed"::: ) ($#v3_matroid0 :::"finite-membered"::: ) ($#v7_simplex0 :::"maximal"::: ) for ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" "KX"; end; theorem :: SIMPLEX0:34 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "SX")) "being" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX")) (Bool "for" (Set (Var "S1")) "being" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "SX")) "st" (Bool (Bool (Set (Var "SX")) "is" ($#v7_simplex0 :::"maximal"::: ) ) & (Bool (Set (Var "S1")) "is" ($#v7_simplex0 :::"maximal"::: ) )) "holds" (Bool (Set (Var "S1")) "is" ($#v7_simplex0 :::"maximal"::: ) ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX"))))))) ; theorem :: SIMPLEX0:35 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "SX")) "being" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX")) (Bool "for" (Set (Var "S1")) "being" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "SX")) "st" (Bool (Bool (Set (Var "S1")) "is" ($#v7_simplex0 :::"maximal"::: ) ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX")))) "holds" (Bool (Set (Var "S1")) "is" ($#v7_simplex0 :::"maximal"::: ) ))))) ; theorem :: SIMPLEX0:36 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "K1")) "," (Set (Var "K2")) "being" ($#v7_simplex0 :::"maximal"::: ) ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX")) "st" (Bool (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "K1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "K2"))))) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "K1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "K2"))) "#)" ))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#v1_matroid0 :::"subset-closed"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "KX")); assume (Bool (Set (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Const "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Const "KX")))) "is" ($#v5_finset_1 :::"finite-membered"::: ) ) ; func "KX" :::"|"::: "A" -> ($#v1_pre_topc :::"strict"::: ) ($#v7_simplex0 :::"maximal"::: ) ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" "KX" means :: SIMPLEX0:def 15 (Bool (Set ($#k2_struct_0 :::"[#]"::: ) it) ($#r1_hidden :::"="::: ) "A"); end; :: deftheorem defines :::"|"::: SIMPLEX0:def 15 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#v1_matroid0 :::"subset-closed"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "KX")) "st" (Bool (Bool (Set (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "KX")))) "is" ($#v5_finset_1 :::"finite-membered"::: ) )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#v1_pre_topc :::"strict"::: ) ($#v7_simplex0 :::"maximal"::: ) ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "KX")) ($#k7_simplex0 :::"|"::: ) (Set (Var "A")))) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" ))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "SC" be ($#m1_simplex0 :::"SimplicialComplex":::) "of" (Set (Const "X")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "SC")); redefine func "SC" :::"|"::: "A" means :: SIMPLEX0:def 16 (Bool (Set ($#k2_struct_0 :::"[#]"::: ) it) ($#r1_hidden :::"="::: ) "A"); end; :: deftheorem defines :::"|"::: SIMPLEX0:def 16 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SC")) "being" ($#m1_simplex0 :::"SimplicialComplex":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "SC")) (Bool "for" (Set (Var "b4")) "being" ($#v1_pre_topc :::"strict"::: ) ($#v7_simplex0 :::"maximal"::: ) ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "SC")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "SC")) ($#k7_simplex0 :::"|"::: ) (Set (Var "A")))) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" ))))); theorem :: SIMPLEX0:37 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SC")) "being" ($#m1_simplex0 :::"SimplicialComplex":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "SC")) "holds" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" (Set (Var "SC")) ($#k7_simplex0 :::"|"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "SC")))))))) ; theorem :: SIMPLEX0:38 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SC")) "being" ($#m1_simplex0 :::"SimplicialComplex":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "SC")) (Bool "for" (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "SC")) ($#k7_simplex0 :::"|"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set "(" (Set (Var "SC")) ($#k7_simplex0 :::"|"::: ) (Set (Var "A")) ")" ) ($#k7_simplex0 :::"|"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "SC")) ($#k7_simplex0 :::"|"::: ) (Set (Var "B")))))))) ; theorem :: SIMPLEX0:39 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SC")) "being" ($#m1_simplex0 :::"SimplicialComplex":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "SC")) ($#k7_simplex0 :::"|"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "SC")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "SC"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "SC"))) "#)" )))) ; theorem :: SIMPLEX0:40 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SC")) "being" ($#m1_simplex0 :::"SimplicialComplex":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "SC")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "SC")) ($#k7_simplex0 :::"|"::: ) (Set (Var "A"))) "is" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Set (Var "SC")) ($#k7_simplex0 :::"|"::: ) (Set (Var "B"))))))) ; registration cluster ($#v1_int_1 :::"integer"::: ) -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); let "i" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"Skeleton_of"::: "(" "KX" "," "i" ")" -> ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" "X" equals :: SIMPLEX0:def 17 (Set ($#k5_simplex0 :::"Complex_of"::: ) (Set "(" ($#k3_simplex0 :::"the_subsets_with_limited_card"::: ) "(" (Set "(" "i" ($#k1_xxreal_3 :::"+"::: ) (Num 1) ")" ) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "KX") ")" ")" )); end; :: deftheorem defines :::"Skeleton_of"::: SIMPLEX0:def 17 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "i")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k8_simplex0 :::"Skeleton_of"::: ) "(" (Set (Var "KX")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_simplex0 :::"Complex_of"::: ) (Set "(" ($#k3_simplex0 :::"the_subsets_with_limited_card"::: ) "(" (Set "(" (Set (Var "i")) ($#k1_xxreal_3 :::"+"::: ) (Num 1) ")" ) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "KX"))) ")" ")" )))))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); cluster (Set ($#k8_simplex0 :::"Skeleton_of"::: ) "(" "KX" "," (Set "(" ($#k2_xxreal_3 :::"-"::: ) (Num 1) ")" ) ")" ) -> ($#v4_simplex0 :::"empty-membered"::: ) ; let "i" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k8_simplex0 :::"Skeleton_of"::: ) "(" "KX" "," "i" ")" ) -> ($#v4_matroid0 :::"finite-degree"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#v4_simplex0 :::"empty-membered"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); let "i" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k8_simplex0 :::"Skeleton_of"::: ) "(" "KX" "," "i" ")" ) -> ($#v4_simplex0 :::"empty-membered"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "KD" be ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "D")); let "i" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k8_simplex0 :::"Skeleton_of"::: ) "(" "KD" "," "i" ")" ) -> ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ; end; theorem :: SIMPLEX0:41 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k2_xxreal_3 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i1"))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2")))) "holds" (Bool (Set ($#k8_simplex0 :::"Skeleton_of"::: ) "(" (Set (Var "KX")) "," (Set (Var "i1")) ")" ) "is" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set ($#k8_simplex0 :::"Skeleton_of"::: ) "(" (Set (Var "KX")) "," (Set (Var "i2")) ")" ))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#v1_matroid0 :::"subset-closed"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); let "i" be ($#m1_hidden :::"Integer":::); :: original: :::"Skeleton_of"::: redefine func :::"Skeleton_of"::: "(" "KX" "," "i" ")" -> ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" "KX"; end; theorem :: SIMPLEX0:42 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "KX")) "is" ($#v1_matroid0 :::"subset-closed"::: ) ) & (Bool (Set ($#k8_simplex0 :::"Skeleton_of"::: ) "(" (Set (Var "KX")) "," (Set (Var "i")) ")" ) "is" ($#v4_simplex0 :::"empty-membered"::: ) ) & (Bool (Bool "not" (Set (Var "KX")) "is" ($#v4_simplex0 :::"empty-membered"::: ) ))) "holds" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_3 :::"-"::: ) (Num 1)))))) ; theorem :: SIMPLEX0:43 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k6_simplex0 :::"degree"::: ) (Set "(" ($#k8_simplex0 :::"Skeleton_of"::: ) "(" (Set (Var "KX")) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "KX"))))))) ; theorem :: SIMPLEX0:44 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k2_xxreal_3 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))) "holds" (Bool (Set ($#k6_simplex0 :::"degree"::: ) (Set "(" ($#k8_simplex0 :::"Skeleton_of"::: ) "(" (Set (Var "KX")) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))))) ; theorem :: SIMPLEX0:45 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k2_xxreal_3 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set ($#k8_simplex0 :::"Skeleton_of"::: ) "(" (Set (Var "KX")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "KX"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "KX"))) "#)" ))) "holds" (Bool (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "KX"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))))) ; theorem :: SIMPLEX0:46 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "KX")) "is" ($#v1_matroid0 :::"subset-closed"::: ) ) & (Bool (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "KX"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))) "holds" (Bool (Set ($#k8_simplex0 :::"Skeleton_of"::: ) "(" (Set (Var "KX")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "KX"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "KX"))) "#)" ))))) ; definitionlet "K" be ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#l1_pre_topc :::"SimplicialComplexStr":::); let "i" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; assume (Bool (Set (Const "i")) "is" ($#v1_int_1 :::"integer"::: ) ) ; mode :::"Simplex"::: "of" "i" "," "K" -> ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Simplex":::) "of" "K" means :: SIMPLEX0:def 18 (Bool (Set ($#k5_card_1 :::"card"::: ) it) ($#r1_hidden :::"="::: ) (Set "i" ($#k1_xxreal_3 :::"+"::: ) (Num 1))) if (Bool "(" (Bool (Set ($#k2_xxreal_3 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) "i") & (Bool "i" ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_simplex0 :::"degree"::: ) "K")) ")" ) otherwise (Bool it "is" ($#v1_xboole_0 :::"empty"::: ) ); end; :: deftheorem defines :::"Simplex"::: SIMPLEX0:def 18 : (Bool "for" (Set (Var "K")) "being" ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#l1_pre_topc :::"SimplicialComplexStr":::) (Bool "for" (Set (Var "i")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "i")) "is" ($#v1_int_1 :::"integer"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Simplex":::) "of" (Set (Var "K")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k2_xxreal_3 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "K"))))) "implies" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m3_simplex0 :::"Simplex"::: ) "of" (Set (Var "i")) "," (Set (Var "K"))) "iff" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k1_xxreal_3 :::"+"::: ) (Num 1))) ")" ) ")" & "(" (Bool (Bool "(" "not" (Bool (Set ($#k2_xxreal_3 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) "or" "not" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "K")))) ")" )) "implies" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m3_simplex0 :::"Simplex"::: ) "of" (Set (Var "i")) "," (Set (Var "K"))) "iff" (Bool (Set (Var "b3")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" ")" )))); registrationlet "K" be ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#l1_pre_topc :::"SimplicialComplexStr":::); cluster -> ($#v1_xboole_0 :::"empty"::: ) for ($#m3_simplex0 :::"Simplex"::: ) "of" (Set ($#k2_xxreal_3 :::"-"::: ) (Num 1)) "," "K"; end; theorem :: SIMPLEX0:47 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "K")) "being" ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#l1_pre_topc :::"SimplicialComplexStr":::) (Bool "for" (Set (Var "S")) "being" ($#m3_simplex0 :::"Simplex"::: ) "of" (Set (Var "i")) "," (Set (Var "K")) "st" (Bool (Bool (Bool "not" (Set (Var "S")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Var "i")) "is" ($#v7_ordinal1 :::"natural"::: ) )))) ; theorem :: SIMPLEX0:48 (Bool "for" (Set (Var "K")) "being" ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#l1_pre_topc :::"SimplicialComplexStr":::) (Bool "for" (Set (Var "S")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Simplex":::) "of" (Set (Var "K")) "holds" (Bool (Set (Var "S")) "is" ($#m3_simplex0 :::"Simplex"::: ) "of" (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "S")) ")" ) ($#k3_xxreal_3 :::"-"::: ) (Num 1)) "," (Set (Var "K"))))) ; theorem :: SIMPLEX0:49 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "S")) "being" ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "K")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "A")) "being" ($#m3_simplex0 :::"Simplex"::: ) "of" (Set (Var "i")) "," (Set (Var "S")) "st" (Bool (Bool "(" "not" (Bool (Set (Var "A")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "S")))) "or" (Bool (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "K")))) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#m3_simplex0 :::"Simplex"::: ) "of" (Set (Var "i")) "," (Set (Var "K")))))))) ; definitionlet "K" be ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#l1_pre_topc :::"SimplicialComplexStr":::); let "i" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; assume that (Bool (Set (Const "i")) "is" ($#v1_int_1 :::"integer"::: ) ) and (Bool (Set (Const "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Const "K")))) ; let "S" be ($#m3_simplex0 :::"Simplex"::: ) "of" (Set (Const "i")) "," (Set (Const "K")); mode :::"Face"::: "of" "S" -> ($#m3_simplex0 :::"Simplex"::: ) "of" (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" "i" ($#k3_xxreal_3 :::"-"::: ) (Num 1) ")" ) "," (Set "(" ($#k2_xxreal_3 :::"-"::: ) (Num 1) ")" ) ")" ) "," "K" means :: SIMPLEX0:def 19 (Bool it ($#r1_tarski :::"c="::: ) "S"); end; :: deftheorem defines :::"Face"::: SIMPLEX0:def 19 : (Bool "for" (Set (Var "K")) "being" ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#l1_pre_topc :::"SimplicialComplexStr":::) (Bool "for" (Set (Var "i")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "i")) "is" ($#v1_int_1 :::"integer"::: ) ) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "K"))))) "holds" (Bool "for" (Set (Var "S")) "being" ($#m3_simplex0 :::"Simplex"::: ) "of" (Set (Var "i")) "," (Set (Var "K")) (Bool "for" (Set (Var "b4")) "being" ($#m3_simplex0 :::"Simplex"::: ) "of" (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" (Set (Var "i")) ($#k3_xxreal_3 :::"-"::: ) (Num 1) ")" ) "," (Set "(" ($#k2_xxreal_3 :::"-"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m4_simplex0 :::"Face"::: ) "of" (Set (Var "S"))) "iff" (Bool (Set (Var "b4")) ($#r1_tarski :::"c="::: ) (Set (Var "S"))) ")" ))))); theorem :: SIMPLEX0:50 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#l1_pre_topc :::"SimplicialComplexStr":::) (Bool "for" (Set (Var "S")) "being" ($#m3_simplex0 :::"Simplex"::: ) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "K"))))) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#m4_simplex0 :::"Face"::: ) "of" (Set (Var "S"))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "S")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" )) ")" ))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); let "P" be ($#m1_hidden :::"Function":::); func :::"subdivision"::: "(" "P" "," "KX" ")" -> ($#v1_pre_topc :::"strict"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" "X" means :: SIMPLEX0:def 20 (Bool "(" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) "KX")) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" it "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"simplex-like"::: ) ) "iff" (Bool "ex" (Set (Var "S")) "being" ($#v6_ordinal1 :::"c=-linear"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_tops_2 :::"simplex-like"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" "KX" "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "P" ($#k7_relat_1 :::".:"::: ) (Set (Var "S"))))) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"subdivision"::: SIMPLEX0:def 20 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b4")) "being" ($#v1_pre_topc :::"strict"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set (Var "P")) "," (Set (Var "KX")) ")" )) "iff" (Bool "(" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "KX")))) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "b4")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"simplex-like"::: ) ) "iff" (Bool "ex" (Set (Var "S")) "being" ($#v6_ordinal1 :::"c=-linear"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_tops_2 :::"simplex-like"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "KX")) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k7_relat_1 :::".:"::: ) (Set (Var "S"))))) ")" ) ")" ) ")" ) ")" ))))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); let "P" be ($#m1_hidden :::"Function":::); cluster (Set ($#k10_simplex0 :::"subdivision"::: ) "(" "P" "," "KX" ")" ) -> ($#v1_pre_topc :::"strict"::: ) ($#v1_matroid0 :::"subset-closed"::: ) ($#v3_matroid0 :::"finite-membered"::: ) ($#v5_simplex0 :::"with_empty_element"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#v3_pencil_1 :::"void"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); let "P" be ($#m1_hidden :::"Function":::); cluster (Set ($#k10_simplex0 :::"subdivision"::: ) "(" "P" "," "KX" ")" ) -> ($#v1_pre_topc :::"strict"::: ) ($#v4_simplex0 :::"empty-membered"::: ) ; end; theorem :: SIMPLEX0:51 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k6_simplex0 :::"degree"::: ) (Set "(" ($#k10_simplex0 :::"subdivision"::: ) "(" (Set (Var "P")) "," (Set (Var "KX")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k6_simplex0 :::"degree"::: ) (Set (Var "KX")) ")" ) ($#k1_xxreal_3 :::"+"::: ) (Num 1)))))) ; theorem :: SIMPLEX0:52 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P"))) "is" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) )) "holds" (Bool (Set ($#k6_simplex0 :::"degree"::: ) (Set "(" ($#k10_simplex0 :::"subdivision"::: ) "(" (Set (Var "P")) "," (Set (Var "KX")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "KX"))))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#v4_matroid0 :::"finite-degree"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); let "P" be ($#m1_hidden :::"Function":::); cluster (Set ($#k10_simplex0 :::"subdivision"::: ) "(" "P" "," "KX" ")" ) -> ($#v1_pre_topc :::"strict"::: ) ($#v4_matroid0 :::"finite-degree"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#v2_simplex0 :::"finite-vertices"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); let "P" be ($#m1_hidden :::"Function":::); cluster (Set ($#k10_simplex0 :::"subdivision"::: ) "(" "P" "," "KX" ")" ) -> ($#v1_pre_topc :::"strict"::: ) ($#v2_simplex0 :::"finite-vertices"::: ) ; end; theorem :: SIMPLEX0:53 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#v1_matroid0 :::"subset-closed"::: ) ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P"))) "is" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "KX"))))) "holds" (Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "KX")) "st" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"simplex-like"::: ) ) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set ($#k1_orders_1 :::"BOOL"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P")))) & (Bool (Set (Set (Var "P")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k1_orders_1 :::"BOOL"::: ) (Set (Var "S")) ")" )) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "KX"))) & (Bool (Set (Set (Var "P")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k1_orders_1 :::"BOOL"::: ) (Set (Var "S")) ")" )) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" )) ")" )) "holds" (Bool (Set ($#k6_simplex0 :::"degree"::: ) (Set "(" ($#k10_simplex0 :::"subdivision"::: ) "(" (Set (Var "P")) "," (Set (Var "KX")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_simplex0 :::"degree"::: ) (Set (Var "KX"))))))) ; theorem :: SIMPLEX0:54 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set "(" (Set (Var "P")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "KX")) ")" ) "is" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set "(" (Set (Var "P")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Z")) ")" ) "," (Set (Var "KX")) ")" ))))) ; theorem :: SIMPLEX0:55 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "KX")))) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set "(" (Set (Var "P")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "KX")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set (Var "P")) "," (Set (Var "KX")) ")" ))))) ; theorem :: SIMPLEX0:56 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "P")) ")" ) "," (Set (Var "KX")) ")" ) "is" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set "(" (Set (Var "Z")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "P")) ")" ) "," (Set (Var "KX")) ")" ))))) ; theorem :: SIMPLEX0:57 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "P")) ($#k7_relat_1 :::".:"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "KX")))) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "P")) ")" ) "," (Set (Var "KX")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set (Var "P")) "," (Set (Var "KX")) ")" ))))) ; theorem :: SIMPLEX0:58 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "SX")) "being" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set (Var "P")) "," (Set (Var "SX")) ")" ) "is" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set (Var "P")) "," (Set (Var "KX")) ")" )))))) ; theorem :: SIMPLEX0:59 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "SX")) "being" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k10_simplex0 :::"subdivision"::: ) "(" (Set (Var "P")) "," (Set (Var "KX")) ")" ")" ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "SX")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "SX"))))) "holds" (Bool (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set (Var "P")) "," (Set (Var "SX")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_simplex0 :::"subdivision"::: ) "(" (Set (Var "P")) "," (Set (Var "KX")) ")" ")" ) ($#k7_simplex0 :::"|"::: ) (Set (Var "A"))))))))) ; theorem :: SIMPLEX0:60 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "K1")) "," (Set (Var "K2")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "K1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "K2"))) "#)" ))) "holds" (Bool (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set (Var "P")) "," (Set (Var "K1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set (Var "P")) "," (Set (Var "K2")) ")" ))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "KX" be ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Const "X")); let "P" be ($#m1_hidden :::"Function":::); let "n" be ($#m1_hidden :::"Nat":::); func :::"subdivision"::: "(" "n" "," "P" "," "KX" ")" -> ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" "X" means :: SIMPLEX0:def 21 (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ($#r1_hidden :::"="::: ) "KX") & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) "n") ($#r1_hidden :::"="::: ) it) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "KX1")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" "X" "st" (Bool (Bool (Set (Var "KX1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_simplex0 :::"subdivision"::: ) "(" "P" "," (Set (Var "KX1")) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"subdivision"::: SIMPLEX0:def 21 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k11_simplex0 :::"subdivision"::: ) "(" (Set (Var "n")) "," (Set (Var "P")) "," (Set (Var "KX")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "KX"))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "b5"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "KX1")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "KX1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set (Var "P")) "," (Set (Var "KX1")) ")" ))) ")" ) ")" )) ")" )))))); theorem :: SIMPLEX0:61 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k11_simplex0 :::"subdivision"::: ) "(" (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Set (Var "P")) "," (Set (Var "KX")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "KX")))))) ; theorem :: SIMPLEX0:62 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k11_simplex0 :::"subdivision"::: ) "(" (Num 1) "," (Set (Var "P")) "," (Set (Var "KX")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_simplex0 :::"subdivision"::: ) "(" (Set (Var "P")) "," (Set (Var "KX")) ")" ))))) ; theorem :: SIMPLEX0:63 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k11_simplex0 :::"subdivision"::: ) "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) "," (Set (Var "P")) "," (Set (Var "KX")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_simplex0 :::"subdivision"::: ) "(" (Set (Var "n")) "," (Set (Var "P")) "," (Set "(" ($#k11_simplex0 :::"subdivision"::: ) "(" (Set (Var "k")) "," (Set (Var "P")) "," (Set (Var "KX")) ")" ")" ) ")" )))))) ; theorem :: SIMPLEX0:64 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k11_simplex0 :::"subdivision"::: ) "(" (Set (Var "n")) "," (Set (Var "P")) "," (Set (Var "KX")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "KX")))))))) ; theorem :: SIMPLEX0:65 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "KX")) "being" ($#m1_simplex0 :::"SimplicialComplexStr"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "SX")) "being" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set (Var "KX")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k11_simplex0 :::"subdivision"::: ) "(" (Set (Var "n")) "," (Set (Var "P")) "," (Set (Var "SX")) ")" ) "is" ($#m2_simplex0 :::"SubSimplicialComplex"::: ) "of" (Set ($#k11_simplex0 :::"subdivision"::: ) "(" (Set (Var "n")) "," (Set (Var "P")) "," (Set (Var "KX")) ")" ))))))) ;