:: by Karol P\c{a}k

::

:: Received February 9, 2010

:: Copyright (c) 2010-2012 Association of Mizar Users

begin

Lm1: for r being Real

for V being RealLinearSpace

for u, w, v being VECTOR of V st r <> 1 & (r * u) + ((1 - r) * w) = v holds

w = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u)

proof end;

theorem Th1: :: RLAFFIN2:1

for V being RealLinearSpace

for v being VECTOR of V

for A being Subset of V

for L being Linear_Combination of A st L is convex & v <> Sum L & L . v <> 0 holds

ex p being VECTOR of V st

( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v )

for v being VECTOR of V

for A being Subset of V

for L being Linear_Combination of A st L is convex & v <> Sum L & L . v <> 0 holds

ex p being VECTOR of V st

( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v )

proof end;

theorem :: RLAFFIN2:2

for r, s being Real

for V being RealLinearSpace

for v, u being VECTOR of V

for I being affinely-independent Subset of V

for p1, p2, w1, w2 being Element of V st v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 holds

( w1 = w2 & r = s )

for V being RealLinearSpace

for v, u being VECTOR of V

for I being affinely-independent Subset of V

for p1, p2, w1, w2 being Element of V st v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 holds

( w1 = w2 & r = s )

proof end;

theorem Th3: :: RLAFFIN2:3

for V being RealLinearSpace

for Af being finite Subset of V

for If being finite affinely-independent Subset of V

for L being Linear_Combination of Af st Af c= conv If & sum L = 1 holds

( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st

( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds

F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) )

for Af being finite Subset of V

for If being finite affinely-independent Subset of V

for L being Linear_Combination of Af st Af c= conv If & sum L = 1 holds

( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st

( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds

F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) )

proof end;

theorem :: RLAFFIN2:4

for V being RealLinearSpace

for v being VECTOR of V

for A, B, Aff being Subset of V st Aff is Affine & (conv A) /\ (conv B) c= Aff & conv (A \ {v}) c= Aff & not v in Aff holds

(conv (A \ {v})) /\ (conv B) = (conv A) /\ (conv B)

for v being VECTOR of V

for A, B, Aff being Subset of V st Aff is Affine & (conv A) /\ (conv B) c= Aff & conv (A \ {v}) c= Aff & not v in Aff holds

(conv (A \ {v})) /\ (conv B) = (conv A) /\ (conv B)

proof end;

begin

definition

let V be non empty RLSStruct ;

let A be Subset of V;

ex b_{1} being Subset of V st

for x being set holds

( x in b_{1} iff ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) )

for b_{1}, b_{2} being Subset of V st ( for x being set holds

( x in b_{1} iff ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) ) ) holds

b_{1} = b_{2}

end;
let A be Subset of V;

func Int A -> Subset of V means :Def1: :: RLAFFIN2:def 1

for x being set holds

( x in it iff ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) );

existence for x being set holds

( x in it iff ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) );

ex b

for x being set holds

( x in b

( not B c< A or not x in conv B ) ) ) )

proof end;

uniqueness for b

( x in b

( not B c< A or not x in conv B ) ) ) ) ) & ( for x being set holds

( x in b

( not B c< A or not x in conv B ) ) ) ) ) holds

b

proof end;

:: deftheorem Def1 defines Int RLAFFIN2:def 1 :

for V being non empty RLSStruct

for A, b_{3} being Subset of V holds

( b_{3} = Int A iff for x being set holds

( x in b_{3} iff ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) ) );

for V being non empty RLSStruct

for A, b

( b

( x in b

( not B c< A or not x in conv B ) ) ) ) );

Lm2: for V being non empty RLSStruct

for A being Subset of V holds Int A c= conv A

proof end;

registration
end;

theorem :: RLAFFIN2:5

theorem :: RLAFFIN2:6

for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for A being Subset of V holds

( Int A = A iff A is trivial )

for A being Subset of V holds

( Int A = A iff A is trivial )

proof end;

theorem Th8: :: RLAFFIN2:8

for V being RealLinearSpace

for A being Subset of V holds conv A = union { (Int B) where B is Subset of V : B c= A }

for A being Subset of V holds conv A = union { (Int B) where B is Subset of V : B c= A }

proof end;

theorem :: RLAFFIN2:9

for V being RealLinearSpace

for A being Subset of V holds conv A = (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } )

for A being Subset of V holds conv A = (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } )

proof end;

theorem Th10: :: RLAFFIN2:10

for x being set

for V being RealLinearSpace

for A being Subset of V st x in Int A holds

ex L being Linear_Combination of A st

( L is convex & x = Sum L )

for V being RealLinearSpace

for A being Subset of V st x in Int A holds

ex L being Linear_Combination of A st

( L is convex & x = Sum L )

proof end;

theorem Th11: :: RLAFFIN2:11

for V being RealLinearSpace

for A being Subset of V

for L being Linear_Combination of A st L is convex & Sum L in Int A holds

Carrier L = A

for A being Subset of V

for L being Linear_Combination of A st L is convex & Sum L in Int A holds

Carrier L = A

proof end;

theorem Th12: :: RLAFFIN2:12

for V being RealLinearSpace

for I being affinely-independent Subset of V

for L being Linear_Combination of I st L is convex & Carrier L = I holds

Sum L in Int I

for I being affinely-independent Subset of V

for L being Linear_Combination of I st L is convex & Carrier L = I holds

Sum L in Int I

proof end;

theorem :: RLAFFIN2:14

for r being Real

for V being RealLinearSpace

for v, u, p being VECTOR of V

for I being affinely-independent Subset of V st v in I & u in Int I & p in conv (I \ {v}) & (r * v) + ((1 - r) * p) = u holds

p in Int (I \ {v})

for V being RealLinearSpace

for v, u, p being VECTOR of V

for I being affinely-independent Subset of V st v in I & u in Int I & p in conv (I \ {v}) & (r * v) + ((1 - r) * p) = u holds

p in Int (I \ {v})

proof end;

begin

definition

let V be RealLinearSpace;

ex b_{1} being Function of (BOOL the carrier of V), the carrier of V st

( ( for A being non empty finite Subset of V holds b_{1} . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds

b_{1} . A = 0. V ) )

for b_{1}, b_{2} being Function of (BOOL the carrier of V), the carrier of V st ( for A being non empty finite Subset of V holds b_{1} . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds

b_{1} . A = 0. V ) & ( for A being non empty finite Subset of V holds b_{2} . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds

b_{2} . A = 0. V ) holds

b_{1} = b_{2}

end;
func center_of_mass V -> Function of (BOOL the carrier of V), the carrier of V means :Def2: :: RLAFFIN2:def 2

( ( for A being non empty finite Subset of V holds it . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds

it . A = 0. V ) );

existence ( ( for A being non empty finite Subset of V holds it . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds

it . A = 0. V ) );

ex b

( ( for A being non empty finite Subset of V holds b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines center_of_mass RLAFFIN2:def 2 :

for V being RealLinearSpace

for b_{2} being Function of (BOOL the carrier of V), the carrier of V holds

( b_{2} = center_of_mass V iff ( ( for A being non empty finite Subset of V holds b_{2} . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds

b_{2} . A = 0. V ) ) );

for V being RealLinearSpace

for b

( b

b

theorem Th15: :: RLAFFIN2:15

for r being Real

for V being RealLinearSpace

for Af being finite Subset of V ex L being Linear_Combination of Af st

( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) )

for V being RealLinearSpace

for Af being finite Subset of V ex L being Linear_Combination of Af st

( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) )

proof end;

theorem Th16: :: RLAFFIN2:16

for V being RealLinearSpace

for Af being finite Subset of V st not Af is empty holds

(center_of_mass V) . Af in conv Af

for Af being finite Subset of V st not Af is empty holds

(center_of_mass V) . Af in conv Af

proof end;

theorem Th17: :: RLAFFIN2:17

for V being RealLinearSpace

for F being Subset-Family of V st union F is finite holds

(center_of_mass V) .: F c= conv (union F)

for F being Subset-Family of V st union F is finite holds

(center_of_mass V) .: F c= conv (union F)

proof end;

theorem Th18: :: RLAFFIN2:18

for V being RealLinearSpace

for v being VECTOR of V

for If being finite affinely-independent Subset of V st v in If holds

(((center_of_mass V) . If) |-- If) . v = 1 / (card If)

for v being VECTOR of V

for If being finite affinely-independent Subset of V st v in If holds

(((center_of_mass V) . If) |-- If) . v = 1 / (card If)

proof end;

theorem Th19: :: RLAFFIN2:19

for V being RealLinearSpace

for If being finite affinely-independent Subset of V holds

( (center_of_mass V) . If in If iff card If = 1 )

for If being finite affinely-independent Subset of V holds

( (center_of_mass V) . If in If iff card If = 1 )

proof end;

theorem Th20: :: RLAFFIN2:20

for V being RealLinearSpace

for If being finite affinely-independent Subset of V st not If is empty holds

(center_of_mass V) . If in Int If

for If being finite affinely-independent Subset of V st not If is empty holds

(center_of_mass V) . If in Int If

proof end;

theorem :: RLAFFIN2:21

for V being RealLinearSpace

for A being Subset of V

for If being finite affinely-independent Subset of V st A c= If & (center_of_mass V) . If in Affin A holds

If = A

for A being Subset of V

for If being finite affinely-independent Subset of V st A c= If & (center_of_mass V) . If in Affin A holds

If = A

proof end;

theorem Th22: :: RLAFFIN2:22

for V being RealLinearSpace

for v being VECTOR of V

for Af being finite Subset of V st v in Af & not Af \ {v} is empty holds

(center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v)

for v being VECTOR of V

for Af being finite Subset of V st v in Af & not Af \ {v} is empty holds

(center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v)

proof end;

theorem :: RLAFFIN2:23

for V being RealLinearSpace

for A being Subset of V

for If being finite affinely-independent Subset of V st conv A c= conv If & not If is empty & conv A misses Int If holds

ex B being Subset of V st

( B c< If & conv A c= conv B )

for A being Subset of V

for If being finite affinely-independent Subset of V st conv A c= conv If & not If is empty & conv A misses Int If holds

ex B being Subset of V st

( B c< If & conv A c= conv B )

proof end;

theorem Th24: :: RLAFFIN2:24

for V being RealLinearSpace

for L1, L2 being Linear_Combination of V st Sum L1 <> Sum L2 & sum L1 = sum L2 holds

ex v being VECTOR of V st L1 . v > L2 . v

for L1, L2 being Linear_Combination of V st Sum L1 <> Sum L2 & sum L1 = sum L2 holds

ex v being VECTOR of V st L1 . v > L2 . v

proof end;

Lm3: for r, s being Real

for V being RealLinearSpace

for v being VECTOR of V

for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds

( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) )

proof end;

theorem Th25: :: RLAFFIN2:25

for r, s being Real

for V being RealLinearSpace

for v being VECTOR of V

for L1, L2 being Linear_Combination of V

for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds

ex rs being Real st

( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )

for V being RealLinearSpace

for v being VECTOR of V

for L1, L2 being Linear_Combination of V

for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds

ex rs being Real st

( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )

proof end;

theorem :: RLAFFIN2:26

for V being RealLinearSpace

for v, u being VECTOR of V

for A being Subset of V st v in conv A & u in conv A & v <> u holds

ex p, w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

for v, u being VECTOR of V

for A being Subset of V st v in conv A & u in conv A & v <> u holds

ex p, w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

proof end;

theorem Th27: :: RLAFFIN2:27

for V being RealLinearSpace

for v being VECTOR of V

for A being Subset of V holds

( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) ) by RLAFFIN1:82;

for v being VECTOR of V

for A being Subset of V holds

( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) ) by RLAFFIN1:82;

theorem Th28: :: RLAFFIN2:28

for V being RealLinearSpace

for v being VECTOR of V

for Af being finite Subset of V

for I being affinely-independent Subset of V st Af c= I & v in Af holds

(I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V

for v being VECTOR of V

for Af being finite Subset of V

for I being affinely-independent Subset of V st Af c= I & v in Af holds

(I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V

proof end;

theorem Th29: :: RLAFFIN2:29

for V being RealLinearSpace

for F being c=-linear Subset-Family of V st union F is finite & union F is affinely-independent holds

(center_of_mass V) .: F is affinely-independent Subset of V

for F being c=-linear Subset-Family of V st union F is finite & union F is affinely-independent holds

(center_of_mass V) .: F is affinely-independent Subset of V

proof end;

theorem :: RLAFFIN2:30

for V being RealLinearSpace

for F being c=-linear Subset-Family of V st union F is affinely-independent & union F is finite holds

Int ((center_of_mass V) .: F) c= Int (union F)

for F being c=-linear Subset-Family of V st union F is affinely-independent & union F is finite holds

Int ((center_of_mass V) .: F) c= Int (union F)

proof end;