:: Circled Sets, Circled Hull, and Circled Family :: by Fahui Zhai , Jianbing Cao and Xiquan Liang :: :: Received August 30, 2005 :: Copyright (c) 2005-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, XBOOLE_0, RLVECT_1, SUBSET_1, ARYTM_1, RLTOPSP1, REAL_1, COMPLEX1, XXREAL_0, RELAT_1, TARSKI, ARYTM_3, RUSUB_4, RLSUB_1, STRUCT_0, SUPINF_2, SETFAM_1, CARD_1, PRE_TOPC, RLVECT_2, FINSEQ_1, FUNCT_1, CARD_3, NAT_1, FUNCT_2, VALUED_1, ORDINAL4, PARTFUN1, CIRCLED1; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, XREAL_0, FUNCT_1, SETFAM_1, PARTFUN1, FUNCT_2, XXREAL_0, REAL_1, DOMAIN_1, STRUCT_0, PRE_TOPC, RLVECT_1, RUSUB_4, CONVEX1, FINSEQ_1, RLSUB_1, RLVECT_2, RVSUM_1, RLTOPSP1, RUSUB_5; constructors SETFAM_1, DOMAIN_1, REAL_1, BINOP_2, COMPLEX1, FINSOP_1, RVSUM_1, RUSUB_5, CONVEX1, RLTOPSP1, RELSET_1, NUMBERS; registrations SUBSET_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, STRUCT_0, RLVECT_1, RLTOPSP1, VALUED_0, FINSEQ_1, CARD_1, ORDINAL1; requirements BOOLE, REAL, NUMERALS, SUBSET, ARITHM; begin theorem :: CIRCLED1:1 for V being RealLinearSpace, A,B being circled Subset of V holds A-B is circled; registration let V be RealLinearSpace, M,N be circled Subset of V; cluster M - N -> circled; end; definition let V be non empty RLSStruct, M be Subset of V; redefine attr M is circled means :: CIRCLED1:def 1 for u being VECTOR of V, r being Real st |.r.| <= 1 & u in M holds r*u in M; end; theorem :: CIRCLED1:2 for V be RealLinearSpace, M being Subset of V, r being Real st M is circled holds r * M is circled; theorem :: CIRCLED1:3 for V be RealLinearSpace, M1,M2 being Subset of V, r1,r2 being Real st M1 is circled & M2 is circled holds r1*M1 + r2*M2 is circled; theorem :: CIRCLED1:4 for V be RealLinearSpace, M1,M2,M3 being Subset of V, r1,r2,r3 being Real st M1 is circled & M2 is circled & M3 is circled holds r1*M1 + r2*M2 + r3* M3 is circled; theorem :: CIRCLED1:5 for V being RealLinearSpace holds Up((0).V) is circled; theorem :: CIRCLED1:6 for V being RealLinearSpace holds Up((Omega).V) is circled; theorem :: CIRCLED1:7 for V being RealLinearSpace, M,N being circled Subset of V holds M /\ N is circled; theorem :: CIRCLED1:8 for V being RealLinearSpace, M,N being circled Subset of V holds M \/ N is circled; begin :: Circled Hull and Circled Family definition let V be non empty RLSStruct, M be Subset of V; func Circled-Family M -> Subset-Family of V means :: CIRCLED1:def 2 for N being Subset of V holds N in it iff N is circled & M c= N; end; definition let V be RealLinearSpace, M be Subset of V; func Cir M -> circled Subset of V equals :: CIRCLED1:def 3 meet Circled-Family M; end; registration let V be RealLinearSpace, M be Subset of V; cluster Circled-Family M -> non empty; end; theorem :: CIRCLED1:9 for V being RealLinearSpace, M1,M2 being Subset of V st M1 c= M2 holds Circled-Family M2 c= Circled-Family M1; theorem :: CIRCLED1:10 for V being RealLinearSpace, M1,M2 being Subset of V st M1 c= M2 holds Cir M1 c= Cir M2; theorem :: CIRCLED1:11 for V being RealLinearSpace, M being Subset of V holds M c= Cir( M); theorem :: CIRCLED1:12 for V being RealLinearSpace, M being Subset of V, N being circled Subset of V st M c= N holds Cir M c= N; theorem :: CIRCLED1:13 for V being RealLinearSpace, M being circled Subset of V holds Cir M = M; theorem :: CIRCLED1:14 for V being RealLinearSpace holds Cir ({}V) = {}; theorem :: CIRCLED1:15 for V being RealLinearSpace, M being Subset of V, r being Real holds r *Cir M = Cir(r*M); begin :: Basic properties of Combination definition let V be RealLinearSpace, L be Linear_Combination of V; attr L is circled means :: CIRCLED1:def 4 ex F being FinSequence of the carrier of V st F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st len f = len F & Sum(f) = 1 & for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0; end; theorem :: CIRCLED1:16 for V being RealLinearSpace, L being Linear_Combination of V st L is circled holds Carrier L <> {}; theorem :: CIRCLED1:17 for V being RealLinearSpace, L being Linear_Combination of V, v being VECTOR of V st L is circled & L.v <= 0 holds not v in Carrier(L); theorem :: CIRCLED1:18 for V being RealLinearSpace, L being Linear_Combination of V st L is circled holds L <> ZeroLC(V); registration let V be RealLinearSpace; cluster circled for Linear_Combination of V; end; definition let V be RealLinearSpace; mode circled_Combination of V is circled Linear_Combination of V; end; registration let V be RealLinearSpace, M be non empty Subset of V; cluster circled for Linear_Combination of M; end; definition let V be RealLinearSpace, M be non empty Subset of V; mode circled_Combination of M is circled Linear_Combination of M; end; definition let V be RealLinearSpace; func circledComb V -> set means :: CIRCLED1:def 5 for L being object holds L in it iff L is circled_Combination of V; end; definition let V be RealLinearSpace, M be non empty Subset of V; func circledComb M -> set means :: CIRCLED1:def 6 for L being object holds L in it iff L is circled_Combination of M; end; theorem :: CIRCLED1:19 for V being RealLinearSpace, v being VECTOR of V holds ex L being circled_Combination of V st Sum L = v & for A being non empty Subset of V st v in A holds L is circled_Combination of A; theorem :: CIRCLED1:20 for V being RealLinearSpace, v1,v2 being VECTOR of V st v1 <> v2 holds ex L being circled_Combination of V st for A being non empty Subset of V st {v1 ,v2} c= A holds L is circled_Combination of A; theorem :: CIRCLED1:21 for V being RealLinearSpace, L1, L2 being circled_Combination of V, a, b being Real st a * b > 0 holds Carrier(a*L1 + b*L2) = Carrier(a * L1) \/ Carrier(b * L2); theorem :: CIRCLED1:22 for V being RealLinearSpace, v being VECTOR of V, L being Linear_Combination of V st L is circled & Carrier(L) = {v} holds L.v = 1 & Sum( L) = L.v * v; theorem :: CIRCLED1:23 for V being RealLinearSpace, v1,v2 being VECTOR of V, L being Linear_Combination of V st L is circled & Carrier(L) = {v1,v2} & v1 <> v2 holds L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 & Sum(L) = L.v1 * v1 + L.v2 * v2; theorem :: CIRCLED1:24 for V being RealLinearSpace, v being VECTOR of V, L being Linear_Combination of {v} st L is circled holds L.v = 1 & Sum(L) = L.v * v; theorem :: CIRCLED1:25 for V being RealLinearSpace, v1,v2 being VECTOR of V, L being Linear_Combination of {v1,v2} st v1 <> v2 & L is circled holds L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 & Sum(L) = L.v1 * v1 + L.v2 * v2;