:: Convex Hull, Set of Convex Combinations and Convex Cone :: by Noboru Endou and Yasunari Shidama :: :: Received June 16, 2003 :: Copyright (c) 2003-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, RLVECT_1, CONVEX2, FUNCT_2, STRUCT_0, XBOOLE_0, SUBSET_1, CARD_3, RLVECT_2, FUNCT_1, FINSEQ_1, RELAT_1, VALUED_1, TARSKI, NAT_1, XXREAL_0, CARD_1, ARYTM_3, ORDINAL4, CONVEX1, REAL_1, ARYTM_1, RFINSEQ, PARTFUN1, FINSET_1, SUPINF_2, CONVEX3, FUNCT_7, XCMPLX_0; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, XCMPLX_0, XREAL_0, XXREAL_0, REAL_1, RELAT_1, FUNCT_1, FINSET_1, ORDINAL1, DOMAIN_1, PARTFUN1, NUMBERS, STRUCT_0, ALGSTR_0, FUNCT_2, FINSEQ_1, RLVECT_1, RLVECT_2, RVSUM_1, CONVEX1, RFINSEQ, CONVEX2; constructors DOMAIN_1, REAL_1, FINSOP_1, RVSUM_1, RFINSEQ, CONVEX1, BINOP_2, RELSET_1, NUMBERS; registrations XBOOLE_0, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, STRUCT_0, RLVECT_1, VALUED_0, CARD_1, RLVECT_2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Equality of Convex Hull and Set of Convex Combinations definition let V be RealLinearSpace; func ConvexComb(V) -> set means :: CONVEX3:def 1 for L being object holds L in it iff L is Convex_Combination of V; end; definition let V be RealLinearSpace, M be non empty Subset of V; func ConvexComb(M) -> set means :: CONVEX3:def 2 for L being object holds L in it iff L is Convex_Combination of M; end; theorem :: CONVEX3:1 for V being RealLinearSpace, v being VECTOR of V holds ex L being Convex_Combination of V st Sum(L) = v & for A being non empty Subset of V st v in A holds L is Convex_Combination of A; theorem :: CONVEX3:2 for V being RealLinearSpace, v1,v2 being VECTOR of V st v1 <> v2 holds ex L being Convex_Combination of V st for A being non empty Subset of V st {v1, v2} c= A holds L is Convex_Combination of A; theorem :: CONVEX3:3 for V being RealLinearSpace, v1,v2,v3 being VECTOR of V st v1 <> v2 & v1 <> v3 & v2 <> v3 holds ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A; theorem :: CONVEX3:4 for V being RealLinearSpace, M being non empty Subset of V holds M is convex iff {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)} c= M; theorem :: CONVEX3:5 for V being RealLinearSpace, M being non empty Subset of V holds conv( M) = {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)}; begin :: Cone and Convex Cone definition let V be non empty RLSStruct, M be Subset of V; attr M is cone means :: CONVEX3:def 3 for r being Real, v being VECTOR of V st r > 0 & v in M holds r*v in M; end; theorem :: CONVEX3:6 for V being non empty RLSStruct, M being Subset of V st M = {} holds M is cone; registration let V be non empty RLSStruct; cluster cone for Subset of V; end; registration let V be non empty RLSStruct; cluster empty cone for Subset of V; end; registration let V be RealLinearSpace; cluster non empty cone for Subset of V; end; theorem :: CONVEX3:7 for V being non empty RLSStruct, M being cone Subset of V st V is vector-distributive scalar-distributive scalar-associative scalar-unital holds M is convex iff for u,v being VECTOR of V st u in M & v in M holds u + v in M; theorem :: CONVEX3:8 for V being RealLinearSpace, M being Subset of V holds M is convex & M is cone iff for L being Linear_Combination of M st Carrier L <> {} & for v being VECTOR of V st v in Carrier L holds L.v > 0 holds Sum(L) in M; theorem :: CONVEX3:9 for V being non empty RLSStruct, M,N being Subset of V st M is cone & N is cone holds M /\ N is cone;