:: CONVEX3  semantic presentation begin  definitionlet "V" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); func  :::"ConvexComb"::: "V" ->    ($#m1_hidden :::"set"::: )   means :: CONVEX3:def 1 (Bool  "for" (Set (Var "L")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "L"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "L")) "is"   ($#m1_rlvect_2 :::"Convex_Combination":::) "of" "V")  ")" )); end; 





:: deftheorem    defines :::"ConvexComb"::: CONVEX3:def 1 :  (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_convex3 :::"ConvexComb"::: )  (Set (Var "V")))) "iff" (Bool  "for" (Set (Var "L")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "L"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool (Set (Var "L")) "is"   ($#m1_rlvect_2 :::"Convex_Combination":::) "of" (Set (Var "V")))  ")" ))  ")" ))); 
 definitionlet "V" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); let "M" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); func  :::"ConvexComb"::: "M" ->    ($#m1_hidden :::"set"::: )   means :: CONVEX3:def 2 (Bool  "for" (Set (Var "L")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "L"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "L")) "is"   ($#m2_rlvect_2 :::"Convex_Combination":::) "of" "M")  ")" )); end; 






:: deftheorem    defines :::"ConvexComb"::: CONVEX3:def 2 :  (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_convex3 :::"ConvexComb"::: )  (Set (Var "M")))) "iff" (Bool  "for" (Set (Var "L")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "L"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool (Set (Var "L")) "is"   ($#m2_rlvect_2 :::"Convex_Combination":::) "of" (Set (Var "M")))  ")" ))  ")" )))); 
 
theorem :: CONVEX3: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  "ex" (Set (Var "L")) "being"   ($#m1_rlvect_2 :::"Convex_Combination":::) "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set   ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set (Var "v"))) & (Bool  "("   "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "L")) "is"   ($#m2_rlvect_2 :::"Convex_Combination":::) "of" (Set (Var "A")))  ")" )  ")" )))) ; 
 
theorem :: CONVEX3:2 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "v1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v2")))) "holds"  (Bool  "ex" (Set (Var "L")) "being"   ($#m1_rlvect_2 :::"Convex_Combination":::) "of" (Set (Var "V")) "st"  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k7_domain_1 :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "L")) "is"   ($#m2_rlvect_2 :::"Convex_Combination":::) "of" (Set (Var "A"))))))) ; 
 
theorem :: CONVEX3:3 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "v1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v2"))) & (Bool (Set (Var "v1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v3"))) & (Bool (Set (Var "v2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v3")))) "holds"  (Bool  "ex" (Set (Var "L")) "being"   ($#m1_rlvect_2 :::"Convex_Combination":::) "of" (Set (Var "V")) "st"  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) ($#k8_domain_1 :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "L")) "is"   ($#m2_rlvect_2 :::"Convex_Combination":::) "of" (Set (Var "A"))))))) ; 
 
theorem :: CONVEX3:4 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v1_convex1 :::"convex"::: )  ) "iff" (Bool  "{"  (Set  "("  ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "L")) ")" ) where L "is"   ($#m2_rlvect_2 :::"Convex_Combination":::) "of" (Set (Var "M")) : (Bool (Set (Var "L"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_convex3 :::"ConvexComb"::: )  (Set (Var "V"))))  "}"    ($#r1_tarski :::"c="::: )  (Set (Var "M")))  ")" ))) ; 
 
theorem :: CONVEX3:5 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k3_convex1 :::"conv"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "L")) ")" ) where L "is"   ($#m2_rlvect_2 :::"Convex_Combination":::) "of" (Set (Var "M")) : (Bool (Set (Var "L"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_convex3 :::"ConvexComb"::: )  (Set (Var "V"))))  "}"  ))) ; 
 begin  definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )  ; let "M" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); attr "M" is  :::"cone":::  means :: CONVEX3:def 3 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" "V"  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  "M")) "holds"  (Bool (Set (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "v")))  ($#r2_hidden :::"in"::: )  "M"))); end; 





:: deftheorem    defines :::"cone"::: CONVEX3:def 3 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v1_convex3 :::"cone"::: )  ) "iff" (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool (Set (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "v")))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))))  ")" ))); 
 
theorem :: CONVEX3:6 (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Var "M")) "is"   ($#v1_convex3 :::"cone"::: )  ))) ; 
 registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )  ; 
cluster   ($#v1_convex3 :::"cone"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V"))); 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )  ; 
cluster   ($#v1_xboole_0 :::"empty"::: )     ($#v1_convex3 :::"cone"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V"))); 
end; registrationlet "V" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_convex3 :::"cone"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V"))); 
end; 
theorem :: CONVEX3:7 (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#v1_convex3 :::"cone"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "V")) "is"   ($#v5_rlvect_1 :::"vector-distributive"::: )  ) & (Bool (Set (Var "V")) "is"   ($#v6_rlvect_1 :::"scalar-distributive"::: )  ) & (Bool (Set (Var "V")) "is"   ($#v7_rlvect_1 :::"scalar-associative"::: )  ) & (Bool (Set (Var "V")) "is"   ($#v8_rlvect_1 :::"scalar-unital"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v1_convex1 :::"convex"::: )  ) "iff" (Bool  "for" (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "u"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool (Set (Set (Var "u"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "v")))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))))  ")" ))) ; 
 
theorem :: CONVEX3:8 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v1_convex1 :::"convex"::: )  ) & (Bool (Set (Var "M")) "is"   ($#v1_convex3 :::"cone"::: )  )  ")" ) "iff" (Bool  "for" (Set (Var "L")) "being"    ($#m2_rlvect_2 :::"Linear_Combination"::: )   "of" (Set (Var "M"))  "st" (Bool (Bool (Set   ($#k3_rlvect_2 :::"Carrier"::: )  (Set (Var "L")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_rlvect_2 :::"Carrier"::: )  (Set (Var "L"))))) "holds"  (Bool (Set (Set (Var "L"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set   ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "L")))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))))  ")" ))) ; 
 
theorem :: CONVEX3:9 (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )    (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "M")) "is"   ($#v1_convex3 :::"cone"::: )  ) & (Bool (Set (Var "N")) "is"   ($#v1_convex3 :::"cone"::: )  )) "holds"  (Bool (Set (Set (Var "M"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "N"))) "is"   ($#v1_convex3 :::"cone"::: )  ))) ;