:: The Geometric Interior in Real Linear Spaces
:: by Karol P\c{a}k
::
:: Copyright (c) 2010-2019 Association of Mizar Users

Lm1: for r being Real
for V being RealLinearSpace
for v, u, w 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 )
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 )
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) ) ) ) )
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)
proof end;

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 & ( 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 & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) )
proof end;
uniqueness
for b1, b2 being Subset of V st ( for x being set holds
( x in b1 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 b2 iff ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) ) ) holds
b1 = b2
proof end;
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 & ( 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

by Def1;

registration
let V be non empty RLSStruct ;
let A be empty Subset of V;
cluster Int A -> empty ;
coherence
Int A is empty
proof end;
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 )
proof end;

theorem :: RLAFFIN2:7
for V being RealLinearSpace
for A, B being Subset of V st A c< B holds
conv A misses Int B
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 }
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 } )
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 )
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
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
proof end;

theorem :: RLAFFIN2:13
for V being RealLinearSpace
for A being Subset of V st not Int A is empty holds
A is finite
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})
proof end;

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) ) & ( 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) ) & ( for A being Subset of V st A is infinite holds
b1 . A = 0. V ) )
proof end;
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) ) & ( for A being Subset of V st A is infinite holds
b1 . A = 0. V ) & ( for A being non empty finite Subset of V holds b2 . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds
b2 . A = 0. V ) holds
b1 = b2
proof end;
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) ) & ( for A being Subset of V st A is infinite holds
b2 . A = 0. V ) ) );

reconsider jj = 1 as Real ;

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 = () +* (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
() . 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
() .: F c= conv ()
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
((() . 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
( () . 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
() . 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 & () . 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
() . Af = ((1 - (1 / (card Af))) * (() /. (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 )
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
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 ) ) )
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 )
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;

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}) \/ {(() . 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
() .: 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 (() .: F) c= Int ()
proof end;