:: 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 b₁ -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 b₁ being affinely-independent Subset of V holds b₁ 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 b₁ being one-to-one FinSequence st rng b₁ = X

proof end;

end;

:: deftheorem Def1 defines Enumeration RLAFFIN3:def 1 :
for X being finite set
for b₂ being one-to-one FinSequence holds
( b₂ is Enumeration of X iff rng b₂ = 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 b₁ being Enumeration of A holds b₁ 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 b₁ being Subset of (TOP-REAL n) st b₁ is Affine holds
b₁ 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 b₁ being Function of V,R^1 st
for v being VECTOR of V holds b₁ . v = (v |-- A) . x

proof end;

uniqueness
for b₁, b₂ being Function of V,R^1 st ( for v being VECTOR of V holds b₁ . v = (v |-- A) . x ) & ( for v being VECTOR of V holds b₂ . v = (v |-- A) . x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines |-- RLAFFIN3:def 3 :
for V being RealLinearSpace
for A being Subset of V
for x being set
for b₄ being Function of V,R^1 holds
( b₄ = |-- (A,x) iff for v being VECTOR of V holds b₄ . 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;