:: Some Properties for Convex Combinations
::  by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama
::
:: Received April 3, 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, REAL_1, FINSEQ_1, XBOOLE_0, RLVECT_1, CONVEX1, SUBSET_1,
      BHSP_1, STRUCT_0, RELAT_1, FUNCT_1, PROB_2, XXREAL_0, CARD_1, ARYTM_3,
      ARYTM_1, RLVECT_2, TARSKI, CARD_3, NAT_1, VALUED_1, JORDAN3, PARTFUN1,
      ORDINAL4, FUNCT_2, RLSUB_1, RUSUB_4, CLASSES1, FINSET_1, CONVEX2,
      FUNCT_7, XCMPLX_0;
 notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XXREAL_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1,
      NAT_1, FINSEQ_1, DOMAIN_1, STRUCT_0, ALGSTR_0, RLVECT_1, RLSUB_1,
      RLSUB_2, FINSEQ_4, RLVECT_2, RVSUM_1, BHSP_1, RUSUB_4, CONVEX1, FINSEQ_6,
      CLASSES1;
 constructors WELLORD2, DOMAIN_1, REAL_1, BINOP_2, FINSEQ_4, FINSOP_1, RLSUB_2,
      RUSUB_4, CONVEX1, MATRIX_1, FINSEQ_6, RVSUM_1, CLASSES1, RELSET_1,
      NUMBERS;
 registrations XBOOLE_0, NUMBERS, XXREAL_0, NAT_1, FINSEQ_1, STRUCT_0,
      RLVECT_1, RUSUB_4, CONVEX1, VALUED_0, RELSET_1, RLVECT_2, XREAL_0,
      ORDINAL1, RVSUM_1, CARD_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

theorem :: CONVEX2:1
  for V being non empty RLSStruct, M,N being convex Subset of V holds M
  /\ N is convex;

theorem :: CONVEX2:2
  for V being RealUnitarySpace-like non empty UNITSTR, M being Subset
of V, F being FinSequence of the carrier of V, B being FinSequence of REAL st M
= {u where u is VECTOR of V : for i being Element of NAT st i in (dom F /\ dom
B) holds ex v being VECTOR of V st v = F.i & u .|. v <= B.i} holds M is convex;

theorem :: CONVEX2:3
  for V being RealUnitarySpace-like non empty UNITSTR, M being Subset
of V, F being FinSequence of the carrier of V, B being FinSequence of REAL st M
= {u where u is VECTOR of V : for i being Element of NAT st i in (dom F /\ dom
  B) holds ex v being VECTOR of V st v = F.i & u .|. v < B.i} holds M is convex
;

theorem :: CONVEX2:4
  for V being RealUnitarySpace-like non empty UNITSTR, M being Subset
of V, F being FinSequence of the carrier of V, B being FinSequence of REAL st M
= {u where u is VECTOR of V : for i being Element of NAT st i in (dom F /\ dom
B) holds ex v being VECTOR of V st v = F.i & u .|. v >= B.i} holds M is convex;

theorem :: CONVEX2:5
  for V being RealUnitarySpace-like non empty UNITSTR, M being Subset
of V, F being FinSequence of the carrier of V, B being FinSequence of REAL st M
= {u where u is VECTOR of V : for i being Element of NAT st i in (dom F /\ dom
  B) holds ex v being VECTOR of V st v = F.i & u .|. v > B.i} holds M is convex
;

theorem :: CONVEX2:6
  for V being RealLinearSpace, M being Subset of V holds (for N being
Subset of V, L being Linear_Combination of N st L is convex & N c= M holds Sum(
  L) in M) iff M is convex;

definition
  let V be RealLinearSpace, M be Subset of V;
  func LinComb(M) -> set means
:: CONVEX2:def 1
  for L being object holds L in it iff L is Linear_Combination of M;
end;

registration
  let V be RealLinearSpace;
  cluster convex for Linear_Combination of V;
end;

definition
  let V be RealLinearSpace;
  mode Convex_Combination of V is convex Linear_Combination of V;
end;

registration
  let V be RealLinearSpace, M be non empty Subset of V;
  cluster convex for Linear_Combination of M;
end;

definition
  let V be RealLinearSpace, M be non empty Subset of V;
  mode Convex_Combination of M is convex Linear_Combination of M;
end;

theorem :: CONVEX2:7
  for V being RealLinearSpace, M be Subset of V holds Convex-Family M <> {};

theorem :: CONVEX2:8
  for V being RealLinearSpace, L1,L2 being Convex_Combination of V,
r being Real st 0 < r & r < 1 holds r*L1 + (1-r)*L2 is Convex_Combination of V;

theorem :: CONVEX2:9
  for V being RealLinearSpace, M being non empty Subset of V, L1,L2
being Convex_Combination of M, r being Real st 0 < r & r < 1 holds r*L1 + (1-r)
  *L2 is Convex_Combination of M;

begin  :: Miscellaneous

theorem :: CONVEX2:10
  for V being RealLinearSpace, W1,W2 being Subspace of V holds Up(W1+W2)
  = Up(W1) + Up(W2);

theorem :: CONVEX2:11
  for V being RealLinearSpace, W1,W2 being Subspace of V holds Up(W1 /\
  W2) = Up(W1) /\ Up(W2);

theorem :: CONVEX2:12
  for V being RealLinearSpace, L1, L2 being Convex_Combination of V, a,b
being Real st a * b > 0 holds Carrier(a*L1 + b*L2) = Carrier(a * L1) \/ Carrier
  (b * L2);

theorem :: CONVEX2:13
  for F,G being Function st F,G are_fiberwise_equipotent for x1,x2 being
  set st x1 in dom F & x2 in dom F & x1 <> x2 holds ex z1,z2 being set st z1 in
  dom G & z2 in dom G & z1 <> z2 & F.x1 = G.z1 & F.x2 = G.z2;

theorem :: CONVEX2:14
  for V being RealLinearSpace, L being Linear_Combination of V, A being
  Subset of V st A c= Carrier(L) holds ex L1 being Linear_Combination of V st
  Carrier(L1) = A;