:: RLAFFIN2 semantic presentation begin theorem :: RLAFFIN2:1 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v2_convex1 :::"convex"::: ) ) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) & (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" )))))) ; theorem :: RLAFFIN2:2 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "I")) "being" ($#v1_rlaffin1 :::"affinely-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "I")))) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "I")))) & (Bool (Bool "not" (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set "(" (Set (Var "I")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p1")) ($#k6_domain_1 :::"}"::: ) ) ")" )))) & (Bool (Bool "not" (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set "(" (Set (Var "I")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p2")) ($#k6_domain_1 :::"}"::: ) ) ")" )))) & (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set "(" (Set (Var "I")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p1")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set "(" (Set (Var "I")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p2")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) & (Bool (Set (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Set "(" (Set (Var "s")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "s")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Var "w2"))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) ")" )))))) ; theorem :: RLAFFIN2:3 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "Af")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "If")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_rlaffin1 :::"affinely-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "Af")) "st" (Bool (Bool (Set (Var "Af")) ($#r1_tarski :::"c="::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "If")))) & (Bool (Set ($#k3_rlaffin1 :::"sum"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_rlaffin1 :::"Affin"::: ) (Set (Var "If")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) )(Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L")) ")" ) ($#k5_rlaffin1 :::"|--"::: ) (Set (Var "If")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "F")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool (Set (Var "G")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k4_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_rlaffin1 :::"|--"::: ) (Set (Var "If")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ))) ")" ) ")" ))))) ; theorem :: RLAFFIN2:4 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "Aff")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "Aff")) "is" ($#v2_rusub_4 :::"Affine"::: ) ) & (Bool (Set (Set "(" ($#k3_convex1 :::"conv"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_convex1 :::"conv"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "Aff"))) & (Bool (Set ($#k3_convex1 :::"conv"::: ) (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "Aff"))) & (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "Aff"))))) "holds" (Bool (Set (Set "(" ($#k3_convex1 :::"conv"::: ) (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_convex1 :::"conv"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_convex1 :::"conv"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_convex1 :::"conv"::: ) (Set (Var "B")) ")" )))))) ; begin definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); func :::"Int"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "V" means :: RLAFFIN2:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) "A")) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "V" "holds" (Bool "(" "not" (Bool (Set (Var "B")) ($#r2_xboole_0 :::"c<"::: ) "A") "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "B")))) ")" ) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"Int"::: RLAFFIN2:def 1 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_rlaffin2 :::"Int"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "A")))) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" "not" (Bool (Set (Var "B")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "A"))) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "B")))) ")" ) ")" ) ")" ) ")" )) ")" ))); registrationlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); cluster (Set ($#k1_rlaffin2 :::"Int"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: RLAFFIN2:5 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_rlaffin2 :::"Int"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "A")))))) ; theorem :: RLAFFIN2:6 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k1_rlaffin2 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) "iff" (Bool (Set (Var "A")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ) ")" ))) ; theorem :: RLAFFIN2:7 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "A"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_rlaffin2 :::"Int"::: ) (Set (Var "B")))))) ; theorem :: RLAFFIN2:8 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k1_rlaffin2 :::"Int"::: ) (Set (Var "B")) ")" ) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) : (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) "}" )))) ; theorem :: RLAFFIN2:9 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rlaffin2 :::"Int"::: ) (Set (Var "A")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k3_convex1 :::"conv"::: ) (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) where v "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) : (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" ")" ))))) ; theorem :: RLAFFIN2:10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rlaffin2 :::"Int"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "L")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_convex1 :::"convex"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L")))) ")" ))))) ; theorem :: RLAFFIN2:11 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v2_convex1 :::"convex"::: ) ) & (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rlaffin2 :::"Int"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))))) ; theorem :: RLAFFIN2:12 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "I")) "being" ($#v1_rlaffin1 :::"affinely-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v2_convex1 :::"convex"::: ) ) & (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Var "I")))) "holds" (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rlaffin2 :::"Int"::: ) (Set (Var "I"))))))) ; theorem :: RLAFFIN2:13 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set ($#k1_rlaffin2 :::"Int"::: ) (Set (Var "A"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) ))) ; theorem :: RLAFFIN2:14 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "I")) "being" ($#v1_rlaffin1 :::"affinely-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rlaffin2 :::"Int"::: ) (Set (Var "I")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set "(" (Set (Var "I")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) & (Bool (Set (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "u")))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rlaffin2 :::"Int"::: ) (Set "(" (Set (Var "I")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ))))))) ; begin definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); func :::"center_of_mass"::: "V" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") means :: RLAFFIN2:def 2 (Bool "(" (Bool "(" "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "V" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "A")) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set (Var "A")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "V" "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"infinite"::: ) )) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "V")) ")" ) ")" ); end; :: deftheorem defines :::"center_of_mass"::: RLAFFIN2:def 2 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_rlaffin2 :::"center_of_mass"::: ) (Set (Var "V")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "A")) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set (Var "A")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"infinite"::: ) )) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ) ")" ) ")" ))); theorem :: RLAFFIN2:15 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "Af")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "L")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "Af")) "st" (Bool "(" (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set (Var "Af")) ")" ))) & (Bool (Set ($#k3_rlaffin1 :::"sum"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Af")) ")" ))) & (Bool (Set (Var "L")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_2 :::"ZeroLC"::: ) (Set (Var "V")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "Af")) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "r")) ")" ))) ")" ))))) ; theorem :: RLAFFIN2:16 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "Af")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "Af")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Set "(" ($#k2_rlaffin2 :::"center_of_mass"::: ) (Set (Var "V")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "Af"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "Af")))))) ; theorem :: RLAFFIN2:17 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Set "(" ($#k2_rlaffin2 :::"center_of_mass"::: ) (Set (Var "V")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" ))))) ; theorem :: RLAFFIN2:18 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "If")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_rlaffin1 :::"affinely-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "If")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k2_rlaffin2 :::"center_of_mass"::: ) (Set (Var "V")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "If")) ")" ) ($#k5_rlaffin1 :::"|--"::: ) (Set (Var "If")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "If")) ")" )))))) ; theorem :: RLAFFIN2:19 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "If")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_rlaffin1 :::"affinely-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_rlaffin2 :::"center_of_mass"::: ) (Set (Var "V")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "If"))) ($#r2_hidden :::"in"::: ) (Set (Var "If"))) "iff" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "If"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ))) ; theorem :: RLAFFIN2:20 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "If")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_rlaffin1 :::"affinely-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "If")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Set "(" ($#k2_rlaffin2 :::"center_of_mass"::: ) (Set (Var "V")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "If"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rlaffin2 :::"Int"::: ) (Set (Var "If")))))) ; theorem :: RLAFFIN2:21 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "If")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_rlaffin1 :::"affinely-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "If"))) & (Bool (Set (Set "(" ($#k2_rlaffin2 :::"center_of_mass"::: ) (Set (Var "V")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "If"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_rlaffin1 :::"Affin"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "If")) ($#r1_hidden :::"="::: ) (Set (Var "A")))))) ; theorem :: RLAFFIN2:22 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "Af")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "Af"))) & (Bool (Bool "not" (Set (Set (Var "Af")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Set "(" ($#k2_rlaffin2 :::"center_of_mass"::: ) (Set (Var "V")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "Af"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Af")) ")" ) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" ($#k2_rlaffin2 :::"center_of_mass"::: ) (Set (Var "V")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "Af")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Af")) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )))))) ; theorem :: RLAFFIN2:23 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "If")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_rlaffin1 :::"affinely-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "If")))) & (Bool (Bool "not" (Set (Var "If")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "A"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_rlaffin2 :::"Int"::: ) (Set (Var "If"))))) "holds" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "If"))) & (Bool (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "B")))) ")" ))))) ; theorem :: RLAFFIN2:24 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L2")))) & (Bool (Set ($#k3_rlaffin1 :::"sum"::: ) (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rlaffin1 :::"sum"::: ) (Set (Var "L2"))))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Set (Set (Var "L1")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "L2")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))))))) ; theorem :: RLAFFIN2:25 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set (Var "r")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L1")) ")" ) ($#k7_rlvect_2 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L2")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set (Var "s")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L1")) ")" ) ($#k7_rlvect_2 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "s")) ")" ) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L2")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))))) "holds" (Bool "ex" (Set (Var "rs")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "rs")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L1")) ")" ) ($#k7_rlvect_2 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "rs")) ")" ) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L2")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & "(" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s")))) "implies" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "rs"))) & (Bool (Set (Var "rs")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) "implies" (Bool "(" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "rs"))) & (Bool (Set (Var "rs")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" ) ")" ")" ))))))) ; theorem :: RLAFFIN2:26 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "A")))) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "A")))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "u")))) "holds" (Bool "ex" (Set (Var "p")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))(Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) & (Bool (Set ($#k1_xboole_0 :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) & (Bool (Set (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" )))))) ; theorem :: RLAFFIN2:27 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )) "is" ($#v1_rlaffin1 :::"affinely-independent"::: ) ) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_rlaffin1 :::"affinely-independent"::: ) ) & (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "or" "not" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k4_rlaffin1 :::"Affin"::: ) (Set (Var "A")))) ")" ) ")" ) ")" )))) ; theorem :: RLAFFIN2:28 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "Af")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "I")) "being" ($#v1_rlaffin1 :::"affinely-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "Af")) ($#r1_tarski :::"c="::: ) (Set (Var "I"))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "Af")))) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" ($#k2_rlaffin2 :::"center_of_mass"::: ) (Set (Var "V")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "Af")) ")" ) ($#k1_tarski :::"}"::: ) )) "is" ($#v1_rlaffin1 :::"affinely-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))))))) ; theorem :: RLAFFIN2:29 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "F")) "being" ($#v6_ordinal1 :::"c=-linear"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) "is" ($#v1_rlaffin1 :::"affinely-independent"::: ) )) "holds" (Bool (Set (Set "(" ($#k2_rlaffin2 :::"center_of_mass"::: ) (Set (Var "V")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "F"))) "is" ($#v1_rlaffin1 :::"affinely-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))))) ; theorem :: RLAFFIN2:30 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "F")) "being" ($#v6_ordinal1 :::"c=-linear"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) "is" ($#v1_rlaffin1 :::"affinely-independent"::: ) ) & (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k1_rlaffin2 :::"Int"::: ) (Set "(" (Set "(" ($#k2_rlaffin2 :::"center_of_mass"::: ) (Set (Var "V")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "F")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_rlaffin2 :::"Int"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" ))))) ;