:: Continuity of Barycentric Coordinates in Euclidean Topological Spaces
:: by Karol P\kak
::
:: Received December 21, 2010
:: Copyright (c) 2010-2011 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)
proof end;

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)
proof end;

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 ) )
proof end;

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

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

registration
let V be finite-dimensional RealLinearSpace;
cluster affinely-independent -> finite affinely-independent Element of bool the carrier of V;
coherence
for b1 being affinely-independent Subset of V holds b1 is finite
proof end;
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 )
proof end;
cluster TOP-REAL n -> finite-dimensional ;
coherence
TOP-REAL n is finite-dimensional
proof end;
end;

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

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

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 )
proof end;

begin

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 & An = { v where v is Element of (TOP-REAL n) : v | k in Ak } holds
( An is open iff Ak is open )
proof end;

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

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 & v in A ) } holds
( Ak is open iff B is open )
proof end;

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
proof end;

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)
proof end;

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)
proof end;

registration
let V be non empty addLoopStr ;
let A be finite Subset of V;
let v be Element of V;
cluster v + A -> finite ;
coherence
v + A is finite
proof end;
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
proof end;

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

registration
let V be non empty RLSStruct ;
let f be FinSequence of V;
let r be Real;
cluster r (#) f -> FinSequence-like ;
coherence
r (#) f is FinSequence-like
proof end;
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
proof end;
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
proof end;
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
proof end;

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 ) )
proof end;

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
proof end;

definition
let V be RealLinearSpace;
let Av be finite Subset of V;
let E be Enumeration of Av;
let x be set ;
func x |-- 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
proof end;

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 & E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E
proof end;

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 & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
proof end;

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
proof end;

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 & x in Affin Affv holds
( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds
(x |-- EV) . y = 0 )
proof end;

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) )
proof end;

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 & x in Affin Affv holds
( x in Affin (Affv \ (EV .: (Seg k))) iff x |-- EV = (k |-> 0) ^ ((x |-- EV) /^ k) )
proof end;

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 & EN . (len EN) = 0* n holds
( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )
proof end;

X: 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 & 0* n in Affn & 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)
proof end;

Lm5: for k being Nat
for V being non empty 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 & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }
proof end;

Lm6: 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 )
proof end;

Lm7: 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 )
proof end;

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 & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is open iff An is open )
proof end;

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 & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is closed iff An is closed )
proof end;

registration
let n be Nat;
cluster Affine -> closed 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
proof end;
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 & 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 )
proof end;

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 & 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 )
proof end;

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
proof end;
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
proof end;
uniqueness
for b1, b2 being Function of V,R^1 st ( for v being VECTOR of V holds b1 . v = (v |-- A) . x ) & ( for v being VECTOR of V holds b2 . v = (v |-- A) . x ) holds
b1 = b2
proof end;
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
proof end;

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
proof end;

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
proof end;

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
proof end;

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

registration
let n be Nat;
let Affn be affinely-independent Subset of (TOP-REAL n);
cluster conv Affn -> closed ;
coherence
conv Affn is closed
proof end;
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
proof end;