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

environ

vocabularies HIDDEN, ALGSTR_0, AOFA_I00, ARYTM_1, ARYTM_3, CARD_1, CARD_3, CLASSES1, COMPLEX1, CONVEX1, EUCLID, EUCLID_9, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, FUNCOP_1, FUNCSDOM, FUNCT_1, FUNCT_2, LMOD_7, MATRIX_1, MATRIX_3, MATRIX13, MATRLIN, MATRLIN2, MESFUNC1, METRIC_1, MONOID_0, NAT_1, NUMBERS, ORDINAL2, ORDINAL4, PARTFUN1, PCOMPS_1, PRE_TOPC, PROB_1, PRVECT_1, QC_LANG1, RCOMP_1, REAL_1, RELAT_1, RFINSEQ, RLAFFIN1, RLSUB_1, RLTOPSP1, RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_5, RUSUB_4, SEMI_AF1, SETFAM_1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI, TOPMETR, TOPS_1, TOPS_2, VALUED_0, VALUED_1, VECTSP_1, XBOOLE_0, XCMPLX_0, XXREAL_0, XXREAL_1, ZFMISC_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, CARD_1, XREAL_0, REAL_1, FINSET_1, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, FUNCOP_1, STRUCT_0, FINSEQ_2, FINSEQOP, RVSUM_1, RLVECT_1, RLVECT_2, RUSUB_4, CONVEX1, RLAFFIN1, COMPLEX1, VALUED_0, METRIC_1, PRE_TOPC, PCOMPS_1, ALGSTR_0, FUNCSDOM, TOPS_2, RLTOPSP1, EUCLID, VFUNCT_1, FVSUM_1, RLSUB_1, RLVECT_3, RLVECT_5, CARD_3, RCOMP_1, EUCLID_9, VECTSP_1, MATRIX_0, MATRIX_1, NAT_D, MATRIX_3, MATRIX_6, VECTSP_6, VECTSP_7, MATRIX13, MATRLIN, RLSUB_2, RFINSEQ, TOPMETR, RLAFFIN2, SETFAM_1, PRVECT_1, TOPREAL9, MATRTOP1;
definitions RLTOPSP1, TARSKI, XBOOLE_0;
theorems BORSUK_5, CARD_1, CARD_2, CARD_3, COMPLEX1, CONVEX1, EUCLID, EUCLID_7, EUCLID_9, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FUNCOP_1, FUNCT_1, FUNCT_2, FVSUM_1, GOBOARD6, JORDAN2B, JORDAN6, LAPLACE, MATRIX_6, MATRIX13, MATRLIN, MATRLIN2, MATRTOP1, MATRTOP2, METRIC_1, METRIZTS, NAT_1, PARTFUN1, PCOMPS_1, PRALG_3, PRE_TOPC, RELAT_1, RFINSEQ, RLAFFIN1, RLAFFIN2, RLSUB_1, RLSUB_2, RLTOPSP1, RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_5, RUSUB_4, RVSUM_1, SETFAM_1, SPPOL_1, STIRL2_1, TARSKI, TOPGRP_1, TOPMETR, TOPREAL9, TOPS_1, TOPS_2, TREAL_1, TSEP_1, URYSOHN1, VECTSP_1, VECTSP_4, VECTSP_7, VECTSP_9, VFUNCT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_0, XREAL_1, XXREAL_0, XXREAL_1, ZFMISC_1, NAT_D, TOPREAL3;
schemes FINSEQ_1, FUNCT_2, TREES_2;
registrations CARD_1, EUCLID, EUCLID_7, EUCLID_9, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_1, JORDAN2B, MATRIX13, MATRTOP1, MONOID_0, NAT_1, NUMBERS, PRE_TOPC, PRVECT_1, RELSET_1, RLAFFIN1, RLTOPSP1, RLVECT_5, RVSUM_1, STRUCT_0, SUBSET_1, TOPMETR, TOPREAL1, TOPS_1, VALUED_0, VECTSP_1, VECTSP_9, XBOOLE_0, XREAL_0, XXREAL_0, ORDINAL1;
constructors HIDDEN, BINOP_2, CONVEX1, EUCLID_9, FUNCSDOM, FVSUM_1, MATRIX_6, MATRIX13, MATRTOP1, MONOID_0, NAT_D, RANKNULL, RCOMP_1, REAL_1, REALSET1, RFINSEQ, RLAFFIN1, RLAFFIN2, RLSUB_2, RLVECT_3, RLVECT_5, RUSUB_5, TOPMETR, TOPREAL9, TOPS_2, VECTSP_7, VFUNCT_1, WELLORD2, MATRIX_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities FINSEQ_1, MATRIX13, MATRTOP1, STRUCT_0, SUBSET_1;
expansions FINSEQ_1, STRUCT_0, TARSKI, XBOOLE_0;


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

:: Space
theorem Th7: :: RLAFFIN3:7
for n, k 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 n, k 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;

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 object ;
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 object holds x |-- E = (x |-- Av) * E;

theorem Th16: :: RLAFFIN3:16
for V being RealLinearSpace
for Av being finite Subset of V
for x being object
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;

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

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

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

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

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;

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