:: Continuity of Barycentric Coordinates in Euclidean Topological Spaces
:: by Karol P\kak
::
:: Received December 21, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

Lm1:  for n being Nat
for f being b1 -element real-valued FinSequence holds f is Point of (TOP-REAL n)
proofend;

theorem Th1: :: RLAFFIN3:1
for f1, f2 being real-valued FinSequence
for r being real number holds (Intervals (f1,r)) ^ (Intervals (f2,r)) = Intervals ((f1 ^ f2),r)
proofend;

theorem Th2: :: RLAFFIN3:2
for x being set
for f1, f2 being FinSequence holds
( x in product (f1 ^ f2) iff ex p1, p2 being FinSequence st
( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 ) )
proofend;

Lm2:  for V being RealLinearSpace
for A being Subset of V holds Lin A = Lin (A \ {(0. V)})
proofend;

theorem Th3: :: RLAFFIN3:3
for V being RealLinearSpace holds
( V is finite-dimensional iff (Omega). V is finite-dimensional )
proofend;

registration
let V be finite-dimensional RealLinearSpace;
cluster affinely-independent  ->  finite affinely-independent for Element of bool the carrier of V;
coherence
 for b1 being affinely-independent Subset of V holds b1 is finite
proofend;
end;

registration
let n be Nat;
cluster TOP-REAL n ->  add-continuous Mult-continuous ;
coherence
 ( TOP-REAL n is add-continuous & TOP-REAL n is Mult-continuous )
proofend;
cluster TOP-REAL n ->  finite-dimensional ;
coherence
 TOP-REAL n is finite-dimensional
proofend;
end;

theorem Th4: :: RLAFFIN3:4
for n being Nat holds dim (TOP-REAL n) = n
proofend;

theorem Th5: :: RLAFFIN3:5
for V being finite-dimensional RealLinearSpace
for A being affinely-independent Subset of V holds card A <= 1 + (dim V)
proofend;

theorem Th6: :: RLAFFIN3:6
for V being finite-dimensional RealLinearSpace
for A being affinely-independent Subset of V holds
( card A = (dim V) + 1 iff Affin A = [#] V )
proofend;

begin

:: Space
theorem Th7: :: RLAFFIN3:7
for k, n being Nat
for An being Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k) st k <= n &amp; An =  {  v where v is Element of (TOP-REAL n) : v | k in Ak  }  holds
( An is open iff Ak is open )
proofend;

Lm3:  for n being Nat holds the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)
proofend;

theorem Th8: :: RLAFFIN3:8
for k, n being Nat
for Ak being Subset of (TOP-REAL k)
for A being Subset of (TOP-REAL (k + n)) st A =  {  (v ^ (n |-> 0)) where v is Element of (TOP-REAL k) : verum  }  holds
for B being Subset of ((TOP-REAL (k + n)) | A) st B =  {  v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak &amp; v in A )  }  holds
( Ak is open iff B is open )
proofend;

theorem Th9: :: RLAFFIN3:9
for V being RealLinearSpace
for A being affinely-independent Subset of V
for B being Subset of V st B c= A holds
(conv A) /\ (Affin B) = conv B
proofend;

theorem Th10: :: RLAFFIN3:10
for r being Real
for V being non empty RLSStruct
for A being non empty set
for f being PartFunc of A, the carrier of V
for X being set holds (r (#) f) .: X = r * (f .: X)
proofend;

theorem Th11: :: RLAFFIN3:11
for n being Nat
for An being Subset of (TOP-REAL n) st 0* n in An holds
Affin An = [#] (Lin An)
proofend;

registration
let V be non empty addLoopStr ;
let A be finite Subset of V;
let v be Element of V;
clusterv + A ->  finite ;
coherence
 v + A is finite
proofend;
end;

Lm4:  for V being non empty RLSStruct
for A being Subset of V
for r being Real holds card (r * A) c= card A
proofend;

registration
let V be non empty RLSStruct ;
let A be finite Subset of V;
let r be Real;
clusterr * A ->  finite ;
coherence
 r * A is finite
proofend;
end;

theorem Th12: :: RLAFFIN3:12
for r being Real
for V being RealLinearSpace
for A being Subset of V holds
( card A = card (r * A) iff ( r <> 0 or A is trivial ) )
proofend;

registration
let V be non empty RLSStruct ;
let f be FinSequence of V;
let r be Real;
clusterr (#) f ->  FinSequence-like ;
coherence
 r (#) f is FinSequence-like
proofend;
end;

begin

definition
let X be finite set ;
mode Enumeration of X ->  one-to-one FinSequence means :Def1: :: RLAFFIN3:def 1
 rng it = X;
existence
 ex b1 being one-to-one FinSequence st rng b1 = X
proofend;
end;

:: deftheorem Def1 defines Enumeration RLAFFIN3:def_1_:_
 for X being finite set
for b2 being one-to-one FinSequence holds
( b2 is Enumeration of X iff rng b2 = X );

definition
let X be 1-sorted ;
let A be finite Subset of X;
:: original:Enumeration
redefine mode Enumeration of A ->  one-to-one FinSequence of X;
coherence
 for b1 being Enumeration of A holds b1 is one-to-one FinSequence of X
proofend;
end;

theorem Th13: :: RLAFFIN3:13
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for A being finite Subset of V
for E being Enumeration of A
for v being Element of V holds E + ((card A) |-> v) is Enumeration of v + A
proofend;

theorem :: RLAFFIN3:14
for r being Real
for V being RealLinearSpace
for Av being finite Subset of V
for E being Enumeration of Av holds
( r (#) E is Enumeration of r * Av iff ( r <> 0 or Av is trivial ) )
proofend;

theorem Th15: :: RLAFFIN3:15
for n, m being Nat
for M being Matrix of n,m,F_Real st the_rank_of M = n holds
for A being finite Subset of (TOP-REAL n)
for E being Enumeration of A holds (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A
proofend;

definition
let V be RealLinearSpace;
let Av be finite Subset of V;
let E be Enumeration of Av;
let x be set ;
funcx |-- E ->  FinSequence of REAL  equals :: RLAFFIN3:def 2
(x |-- Av) * E;
coherence
 (x |-- Av) * E is FinSequence of REAL ;
end;

:: deftheorem  defines |-- RLAFFIN3:def_2_:_
 for V being RealLinearSpace
for Av being finite Subset of V
for E being Enumeration of Av
for x being set holds x |-- E = (x |-- Av) * E;

theorem Th16: :: RLAFFIN3:16
for x being set
for V being RealLinearSpace
for Av being finite Subset of V
for E being Enumeration of Av holds len (x |-- E) = card Av
proofend;

theorem Th17: :: RLAFFIN3:17
for V being RealLinearSpace
for v, w being VECTOR of V
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for E being Enumeration of v + Affv st w in Affin Affv &amp; E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E
proofend;

theorem :: RLAFFIN3:18
for r being Real
for V being RealLinearSpace
for v being VECTOR of V
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for rE being Enumeration of r * Affv st v in Affin Affv &amp; rE = r (#) EV &amp; r <> 0 holds
v |-- EV = (r * v) |-- rE
proofend;

theorem Th19: :: RLAFFIN3:19
for n, m being Nat
for Affn being affinely-independent Subset of (TOP-REAL n)
for EN being Enumeration of Affn
for M being Matrix of n,m,F_Real st the_rank_of M = n holds
for ME being Enumeration of (Mx2Tran M) .: Affn st ME = (Mx2Tran M) * EN holds
for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME
proofend;

theorem Th20: :: RLAFFIN3:20
for x being set
for V being RealLinearSpace
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for A being Subset of V st A c= Affv &amp; x in Affin Affv holds
( x in Affin A iff for y being set st y in dom (x |-- EV) &amp; not EV . y in A holds
(x |-- EV) . y = 0 )
proofend;

theorem :: RLAFFIN3:21
for x being set
for k being Nat
for V being RealLinearSpace
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv st x in Affin Affv holds
( x in Affin (EV .: (Seg k)) iff x |-- EV = ((x |-- EV) | k) ^ (((card Affv) -' k) |-> 0) )
proofend;

theorem Th22: :: RLAFFIN3:22
for x being set
for k being Nat
for V being RealLinearSpace
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv st k <= card Affv &amp; x in Affin Affv holds
( x in Affin (Affv \ (EV .: (Seg k))) iff x |-- EV = (k |-> 0) ^ ((x |-- EV) /^ k) )
proofend;

theorem Th23: :: RLAFFIN3:23
for n being Nat
for Affn being affinely-independent Subset of (TOP-REAL n)
for EN being Enumeration of Affn st 0* n in Affn &amp; EN . (len EN) = 0* n holds
( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} &amp; ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )
proofend;

Lm5:  0 in REAL
by XREAL_0:def_1;

theorem Th24: :: RLAFFIN3:24
for n being Nat
for Affn being affinely-independent Subset of (TOP-REAL n)
for EN being Enumeration of Affn
for A being Subset of (n -VectSp_over F_Real) st Affn = A &amp; 0* n in Affn &amp; EN . (len EN) = 0* n holds
for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds
for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)
proofend;

Lm6:  for k being Nat
for V being LinearTopSpace
for A being finite affinely-independent Subset of V
for E being Enumeration of A
for v being Point of V
for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds
for X being set holds (transl (v,V)) .:  {  u where u is Point of V : ( u in Affin A &amp; (u |-- E) | k in X )  }  =  {  w where w is Point of V : ( w in Affin (v + A) &amp; (w |-- Ev) | k in X )  }
proofend;

Lm7:  for n, k being Nat st k <= n holds
for A being non empty finite affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
for E being Enumeration of A st E . (len E) = 0* n holds
for P being Subset of (TOP-REAL k)
for B being Subset of (TOP-REAL n) st B =  {  pn where pn is Point of (TOP-REAL n) : (pn |-- E) | k in P  }  holds
( P is open iff B is open )
proofend;

Lm8:  for n, k being Nat
for A being non empty finite affinely-independent Subset of (TOP-REAL n) st k < card A holds
for E being Enumeration of A st E . (len E) = 0* n holds
for P being Subset of (TOP-REAL k)
for B being Subset of ((TOP-REAL n) | (Affin A)) st B =  {  v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P  }  holds
( P is open iff B is open )
proofend;

theorem Th25: :: RLAFFIN3:25
for n, k being Nat
for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn
for An being Subset of (TOP-REAL n) st k <= n &amp; card Affn = n + 1 &amp; An =  {  pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak  }  holds
( Ak is open iff An is open )
proofend;

theorem Th26: :: RLAFFIN3:26
for n, k being Nat
for An being Subset of (TOP-REAL n)
for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn st k <= n &amp; card Affn = n + 1 &amp; An =  {  pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak  }  holds
( Ak is closed iff An is closed )
proofend;

registration
let n be Nat;
cluster Affine  ->  closed for Element of bool the carrier of (TOP-REAL n);
coherence
 for b1 being Subset of (TOP-REAL n) st b1 is Affine holds
b1 is closed
proofend;
end;

theorem Th27: :: RLAFFIN3:27
for n, k being Nat
for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn
for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn &amp; B =  {  pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak  }  holds
( Ak is open iff B is open )
proofend;

theorem Th28: :: RLAFFIN3:28
for n, k being Nat
for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn
for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn &amp; B =  {  pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak  }  holds
( Ak is closed iff B is closed )
proofend;

registration
let n be Nat;
let p, q be Point of (TOP-REAL n);
cluster halfline (p,q) ->  closed ;
coherence
 halfline (p,q) is closed
proofend;
end;

begin

definition
let V be RealLinearSpace;
let A be Subset of V;
let x be set ;
func |-- (A,x) ->  Function of V,R^1 means :Def3: :: RLAFFIN3:def 3
 for v being VECTOR of V holds it . v = (v |-- A) . x;
existence
 ex b1 being Function of V,R^1 st
for v being VECTOR of V holds b1 . v = (v |-- A) . x
proofend;
uniqueness
 for b1, b2 being Function of V,R^1 st ( for v being VECTOR of V holds b1 . v = (v |-- A) . x ) &amp; ( for v being VECTOR of V holds b2 . v = (v |-- A) . x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines |-- RLAFFIN3:def_3_:_
 for V being RealLinearSpace
for A being Subset of V
for x being set
for b4 being Function of V,R^1 holds
( b4 = |-- (A,x) iff for v being VECTOR of V holds b4 . v = (v |-- A) . x );

theorem Th29: :: RLAFFIN3:29
for x being set
for V being RealLinearSpace
for A being Subset of V st not x in A holds
|-- (A,x) = ([#] V) --> 0
proofend;

theorem :: RLAFFIN3:30
for x being set
for V being RealLinearSpace
for A being affinely-independent Subset of V st |-- (A,x) = ([#] V) --> 0 holds
not x in A
proofend;

theorem Th31: :: RLAFFIN3:31
for x being set
for n being Nat
for Affn being affinely-independent Subset of (TOP-REAL n) holds (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1
proofend;

theorem Th32: :: RLAFFIN3:32
for x being set
for n being Nat
for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds
|-- (Affn,x) is continuous
proofend;

Lm9:  for n being Nat
for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
conv A is closed
proofend;

registration
let n be Nat;
let Affn be affinely-independent Subset of (TOP-REAL n);
cluster conv Affn ->  closed ;
coherence
 conv Affn is closed
proofend;
end;

theorem :: RLAFFIN3:33
for n being Nat
for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds
Int Affn is open
proofend;