:: 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;