:: The Geometric Interior in Real Linear Spaces
:: 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 &amp; (r * u) + ((1 - r) * w) = v holds
w = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u)
proofend;

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 &amp; v <> Sum L &amp; L . v <> 0 holds
ex p being VECTOR of V st
( p in conv (A \ {v}) &amp; Sum L = ((L . v) * v) + ((1 - (L . v)) * p) &amp; ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v )
proofend;

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 &amp; u in conv I &amp; not u in conv (I \ {p1}) &amp; not u in conv (I \ {p2}) &amp; w1 in conv (I \ {p1}) &amp; w2 in conv (I \ {p2}) &amp; (r * u) + ((1 - r) * w1) = v &amp; (s * u) + ((1 - s) * w2) = v &amp; r < 1 &amp; s < 1 holds
( w1 = w2 &amp; r = s )
proofend;

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 &amp; sum L = 1 holds
( Sum L in Affin If &amp; ( 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 &amp; len G = len F &amp; G is one-to-one &amp; rng G = Carrier L &amp; ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) )
proofend;

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 &amp; (conv A) /\ (conv B) c= Aff &amp; conv (A \ {v}) c= Aff &amp; not v in Aff holds
(conv (A \ {v})) /\ (conv B) = (conv A) /\ (conv B)
proofend;

begin

definition
let V be non empty RLSStruct ;
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 &amp; ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) );
existence
 ex b1 being Subset of V st
for x being set holds
( x in b1 iff ( x in conv A &amp; ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) )
proofend;
uniqueness
 for b1, b2 being Subset of V st ( for x being set holds
( x in b1 iff ( x in conv A &amp; ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) ) ) &amp; ( for x being set holds
( x in b2 iff ( x in conv A &amp; ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Int RLAFFIN2:def_1_:_
 for V being non empty RLSStruct
for A, b3 being Subset of V holds
( b3 = Int A iff for x being set holds
( x in b3 iff ( x in conv A &amp; ( for B being Subset of V holds
( 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
proofend;

registration
let V be non empty RLSStruct ;
let A be empty Subset of V;
cluster Int A ->  empty ;
coherence
 Int A is empty
proofend;
end;

theorem :: RLAFFIN2:5
for V being non empty RLSStruct
for A being Subset of V holds Int A c= conv A by Lm2;

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 )
proofend;

theorem :: RLAFFIN2:7
for V being RealLinearSpace
for A, B being Subset of V st A c< B holds
conv A misses Int B
proofend;

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  }
proofend;

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  }  )
proofend;

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 &amp; x = Sum L )
proofend;

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 &amp; Sum L in Int A holds
Carrier L = A
proofend;

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 &amp; Carrier L = I holds
Sum L in Int I
proofend;

theorem :: RLAFFIN2:13
for V being RealLinearSpace
for A being Subset of V st not Int A is empty holds
A is finite
proofend;

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 &amp; u in Int I &amp; p in conv (I \ {v}) &amp; (r * v) + ((1 - r) * p) = u holds
p in Int (I \ {v})
proofend;

begin

definition
let V be RealLinearSpace;
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) ) &amp; ( for A being Subset of V st A is infinite holds
it . A = 0. V ) );
existence
 ex b1 being Function of (BOOL the carrier of V), the carrier of V st
( ( for A being non empty finite Subset of V holds b1 . A = (1 / (card A)) * (Sum A) ) &amp; ( for A being Subset of V st A is infinite holds
b1 . A = 0. V ) )
proofend;
uniqueness
 for b1, b2 being Function of (BOOL the carrier of V), the carrier of V st ( for A being non empty finite Subset of V holds b1 . A = (1 / (card A)) * (Sum A) ) &amp; ( for A being Subset of V st A is infinite holds
b1 . A = 0. V ) &amp; ( for A being non empty finite Subset of V holds b2 . A = (1 / (card A)) * (Sum A) ) &amp; ( for A being Subset of V st A is infinite holds
b2 . A = 0. V ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines center_of_mass RLAFFIN2:def_2_:_
 for V being RealLinearSpace
for b2 being Function of (BOOL the carrier of V), the carrier of V holds
( b2 = center_of_mass V iff ( ( for A being non empty finite Subset of V holds b2 . A = (1 / (card A)) * (Sum A) ) &amp; ( for A being Subset of V st A is infinite holds
b2 . A = 0. V ) ) );

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) &amp; sum L = r * (card Af) &amp; L = (ZeroLC V) +* (Af --> r) )
proofend;

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

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)
proofend;

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)
proofend;

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 )
proofend;

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

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 &amp; (center_of_mass V) . If in Affin A holds
If = A
proofend;

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 &amp; 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)
proofend;

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 &amp; not If is empty &amp; conv A misses Int If holds
ex B being Subset of V st
( B c< If &amp; conv A c= conv B )
proofend;

theorem Th24: :: RLAFFIN2:24
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V st Sum L1 <> Sum L2 &amp; sum L1 = sum L2 holds
ex v being VECTOR of V st L1 . v > L2 . v
proofend;

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)) )
proofend;

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 &amp; p <= ((s * L1) + ((1 - s) * L2)) . v holds
ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p &amp; ( r <= s implies ( r <= rs &amp; rs <= s ) ) &amp; ( s <= r implies ( s <= rs &amp; rs <= r ) ) )
proofend;

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 &amp; u in conv A &amp; v <> u holds
ex p, w being VECTOR of V ex r being Real st
( p in A &amp; w in conv (A \ {p}) &amp; 0 <= r &amp; r < 1 &amp; (r * u) + ((1 - r) * w) = v )
proofend;

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 &amp; ( 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 &amp; v in Af holds
(I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V
proofend;

theorem Th29: :: RLAFFIN2:29
for V being RealLinearSpace
for F being c=-linear Subset-Family of V st union F is finite &amp; union F is affinely-independent holds
(center_of_mass V) .: F is affinely-independent Subset of V
proofend;

theorem :: RLAFFIN2:30
for V being RealLinearSpace
for F being c=-linear Subset-Family of V st union F is affinely-independent &amp; union F is finite holds
Int ((center_of_mass V) .: F) c= Int (union F)
proofend;