:: by Karol P\c{a}k

::

:: Received February 9, 2010

:: Copyright (c) 2010-2018 Association of Mizar Users

theorem Th1: :: SIMPLEX1:1

for X being set

for R being Relation

for C being Cardinal st ( for x being object st x in X holds

card (Im (R,x)) = C ) holds

card R = (card (R | ((dom R) \ X))) +` (C *` (card X))

for R being Relation

for C being Cardinal st ( for x being object st x in X holds

card (Im (R,x)) = C ) holds

card R = (card (R | ((dom R) \ X))) +` (C *` (card X))

proof end;

theorem Th2: :: SIMPLEX1:2

for X being set

for Y being non empty finite set st card X = (card Y) + 1 holds

for f being Function of X,Y st f is onto holds

ex y being set st

( y in Y & card (f " {y}) = 2 & ( for x being set st x in Y & x <> y holds

card (f " {x}) = 1 ) )

for Y being non empty finite set st card X = (card Y) + 1 holds

for f being Function of X,Y st f is onto holds

ex y being set st

( y in Y & card (f " {y}) = 2 & ( for x being set st x in Y & x <> y holds

card (f " {x}) = 1 ) )

proof end;

definition

let X be 1-sorted ;

mode SimplicialComplexStr of X is SimplicialComplexStr of the carrier of X;

mode SimplicialComplex of X is SimplicialComplex of the carrier of X;

end;
mode SimplicialComplexStr of X is SimplicialComplexStr of the carrier of X;

mode SimplicialComplex of X is SimplicialComplex of the carrier of X;

definition

let X be 1-sorted ;

let K be SimplicialComplexStr of X;

let A be Subset of K;

coherence

A is Subset of X

end;
let K be SimplicialComplexStr of X;

let A be Subset of K;

coherence

A is Subset of X

proof end;

:: deftheorem defines @ SIMPLEX1:def 1 :

for X being 1-sorted

for K being SimplicialComplexStr of X

for A being Subset of K holds @ A = A;

for X being 1-sorted

for K being SimplicialComplexStr of X

for A being Subset of K holds @ A = A;

definition

let X be 1-sorted ;

let K be SimplicialComplexStr of X;

let A be Subset-Family of K;

coherence

A is Subset-Family of X

end;
let K be SimplicialComplexStr of X;

let A be Subset-Family of K;

coherence

A is Subset-Family of X

proof end;

:: deftheorem defines @ SIMPLEX1:def 2 :

for X being 1-sorted

for K being SimplicialComplexStr of X

for A being Subset-Family of K holds @ A = A;

for X being 1-sorted

for K being SimplicialComplexStr of X

for A being Subset-Family of K holds @ A = A;

theorem Th3: :: SIMPLEX1:3

for X being 1-sorted

for K being subset-closed SimplicialComplexStr of X st K is total holds

for S being finite Subset of K st S is simplex-like holds

Complex_of {(@ S)} is SubSimplicialComplex of K

for K being subset-closed SimplicialComplexStr of X st K is total holds

for S being finite Subset of K st S is simplex-like holds

Complex_of {(@ S)} is SubSimplicialComplex of K

proof end;

definition

let RLS be non empty RLSStruct ;

let Kr be SimplicialComplexStr of RLS;

ex b_{1} being Subset of RLS st

for x being set holds

( x in b_{1} iff ex A being Subset of Kr st

( A is simplex-like & x in conv (@ A) ) )

for b_{1}, b_{2} being Subset of RLS st ( for x being set holds

( x in b_{1} iff ex A being Subset of Kr st

( A is simplex-like & x in conv (@ A) ) ) ) & ( for x being set holds

( x in b_{2} iff ex A being Subset of Kr st

( A is simplex-like & x in conv (@ A) ) ) ) holds

b_{1} = b_{2}

end;
let Kr be SimplicialComplexStr of RLS;

func |.Kr.| -> Subset of RLS means :Def3: :: SIMPLEX1:def 3

for x being set holds

( x in it iff ex A being Subset of Kr st

( A is simplex-like & x in conv (@ A) ) );

existence for x being set holds

( x in it iff ex A being Subset of Kr st

( A is simplex-like & x in conv (@ A) ) );

ex b

for x being set holds

( x in b

( A is simplex-like & x in conv (@ A) ) )

proof end;

uniqueness for b

( x in b

( A is simplex-like & x in conv (@ A) ) ) ) & ( for x being set holds

( x in b

( A is simplex-like & x in conv (@ A) ) ) ) holds

b

proof end;

:: deftheorem Def3 defines |. SIMPLEX1:def 3 :

for RLS being non empty RLSStruct

for Kr being SimplicialComplexStr of RLS

for b_{3} being Subset of RLS holds

( b_{3} = |.Kr.| iff for x being set holds

( x in b_{3} iff ex A being Subset of Kr st

( A is simplex-like & x in conv (@ A) ) ) );

for RLS being non empty RLSStruct

for Kr being SimplicialComplexStr of RLS

for b

( b

( x in b

( A is simplex-like & x in conv (@ A) ) ) );

theorem Th4: :: SIMPLEX1:4

for RLS being non empty RLSStruct

for K1r, K2r being SimplicialComplexStr of RLS st the topology of K1r c= the topology of K2r holds

|.K1r.| c= |.K2r.|

for K1r, K2r being SimplicialComplexStr of RLS st the topology of K1r c= the topology of K2r holds

|.K1r.| c= |.K2r.|

proof end;

theorem :: SIMPLEX1:6

for x being set

for V being RealLinearSpace

for K being subset-closed SimplicialComplexStr of V holds

( x in |.K.| iff ex A being Subset of K st

( A is simplex-like & x in Int (@ A) ) )

for V being RealLinearSpace

for K being subset-closed SimplicialComplexStr of V holds

( x in |.K.| iff ex A being Subset of K st

( A is simplex-like & x in Int (@ A) ) )

proof end;

theorem Th7: :: SIMPLEX1:7

for RLS being non empty RLSStruct

for Kr being SimplicialComplexStr of RLS holds

( |.Kr.| is empty iff Kr is empty-membered )

for Kr being SimplicialComplexStr of RLS holds

( |.Kr.| is empty iff Kr is empty-membered )

proof end;

theorem :: SIMPLEX1:9

for RLS being non empty RLSStruct

for A, B being Subset-Family of RLS holds |.(Complex_of (A \/ B)).| = |.(Complex_of A).| \/ |.(Complex_of B).|

for A, B being Subset-Family of RLS holds |.(Complex_of (A \/ B)).| = |.(Complex_of A).| \/ |.(Complex_of B).|

proof end;

definition

let RLS be non empty RLSStruct ;

let Kr be SimplicialComplexStr of RLS;

ex b_{1} being SimplicialComplexStr of RLS st

( |.Kr.| c= |.b_{1}.| & ( for A being Subset of b_{1} st A is simplex-like holds

ex B being Subset of Kr st

( B is simplex-like & conv (@ A) c= conv (@ B) ) ) )

end;
let Kr be SimplicialComplexStr of RLS;

mode SubdivisionStr of Kr -> SimplicialComplexStr of RLS means :Def4: :: SIMPLEX1:def 4

( |.Kr.| c= |.it.| & ( for A being Subset of it st A is simplex-like holds

ex B being Subset of Kr st

( B is simplex-like & conv (@ A) c= conv (@ B) ) ) );

existence ( |.Kr.| c= |.it.| & ( for A being Subset of it st A is simplex-like holds

ex B being Subset of Kr st

( B is simplex-like & conv (@ A) c= conv (@ B) ) ) );

ex b

( |.Kr.| c= |.b

ex B being Subset of Kr st

( B is simplex-like & conv (@ A) c= conv (@ B) ) ) )

proof end;

:: deftheorem Def4 defines SubdivisionStr SIMPLEX1:def 4 :

for RLS being non empty RLSStruct

for Kr, b_{3} being SimplicialComplexStr of RLS holds

( b_{3} is SubdivisionStr of Kr iff ( |.Kr.| c= |.b_{3}.| & ( for A being Subset of b_{3} st A is simplex-like holds

ex B being Subset of Kr st

( B is simplex-like & conv (@ A) c= conv (@ B) ) ) ) );

for RLS being non empty RLSStruct

for Kr, b

( b

ex B being Subset of Kr st

( B is simplex-like & conv (@ A) c= conv (@ B) ) ) ) );

theorem Th10: :: SIMPLEX1:10

for RLS being non empty RLSStruct

for Kr being SimplicialComplexStr of RLS

for P being SubdivisionStr of Kr holds |.Kr.| = |.P.|

for Kr being SimplicialComplexStr of RLS

for P being SubdivisionStr of Kr holds |.Kr.| = |.P.|

proof end;

registration

let RLS be non empty RLSStruct ;

let Kr be with_non-empty_element SimplicialComplexStr of RLS;

coherence

for b_{1} being SubdivisionStr of Kr holds b_{1} is with_non-empty_element

end;
let Kr be with_non-empty_element SimplicialComplexStr of RLS;

coherence

for b

proof end;

theorem Th11: :: SIMPLEX1:11

for RLS being non empty RLSStruct

for Kr being SimplicialComplexStr of RLS holds Kr is SubdivisionStr of Kr

for Kr being SimplicialComplexStr of RLS holds Kr is SubdivisionStr of Kr

proof end;

theorem Th12: :: SIMPLEX1:12

for RLS being non empty RLSStruct

for Kr being SimplicialComplexStr of RLS holds Complex_of the topology of Kr is SubdivisionStr of Kr

for Kr being SimplicialComplexStr of RLS holds Complex_of the topology of Kr is SubdivisionStr of Kr

proof end;

theorem Th13: :: SIMPLEX1:13

for V being RealLinearSpace

for K being subset-closed SimplicialComplexStr of V

for SF being Subset-Family of K st SF = Sub_of_Fin the topology of K holds

Complex_of SF is SubdivisionStr of K

for K being subset-closed SimplicialComplexStr of V

for SF being Subset-Family of K st SF = Sub_of_Fin the topology of K holds

Complex_of SF is SubdivisionStr of K

proof end;

theorem Th14: :: SIMPLEX1:14

for RLS being non empty RLSStruct

for Kr being SimplicialComplexStr of RLS

for P1 being SubdivisionStr of Kr

for P2 being SubdivisionStr of P1 holds P2 is SubdivisionStr of Kr

for Kr being SimplicialComplexStr of RLS

for P1 being SubdivisionStr of Kr

for P2 being SubdivisionStr of P1 holds P2 is SubdivisionStr of Kr

proof end;

registration

let V be RealLinearSpace;

let K be SimplicialComplexStr of V;

existence

ex b_{1} being SubdivisionStr of K st

( b_{1} is finite-membered & b_{1} is subset-closed )

end;
let K be SimplicialComplexStr of V;

existence

ex b

( b

proof end;

definition

let V be RealLinearSpace;

let K be SimplicialComplexStr of V;

mode Subdivision of K is subset-closed finite-membered SubdivisionStr of K;

end;
let K be SimplicialComplexStr of V;

mode Subdivision of K is subset-closed finite-membered SubdivisionStr of K;

theorem Th15: :: SIMPLEX1:15

for V being RealLinearSpace

for K being with_empty_element SimplicialComplex of V st |.K.| c= [#] K holds

for B being Function of (BOOL the carrier of V), the carrier of V st ( for S being Simplex of K st not S is empty holds

B . S in conv (@ S) ) holds

subdivision (B,K) is SubdivisionStr of K

for K being with_empty_element SimplicialComplex of V st |.K.| c= [#] K holds

for B being Function of (BOOL the carrier of V), the carrier of V st ( for S being Simplex of K st not S is empty holds

B . S in conv (@ S) ) holds

subdivision (B,K) is SubdivisionStr of K

proof end;

registration

let V be RealLinearSpace;

let Kv be non void SimplicialComplex of V;

existence

not for b_{1} being Subdivision of Kv holds b_{1} is void

end;
let Kv be non void SimplicialComplex of V;

existence

not for b

proof end;

definition

let V be RealLinearSpace;

let Kv be non void SimplicialComplex of V;

assume A1: |.Kv.| c= [#] Kv ;

subdivision ((center_of_mass V),Kv) is non void Subdivision of Kv

end;
let Kv be non void SimplicialComplex of V;

assume A1: |.Kv.| c= [#] Kv ;

func BCS Kv -> non void Subdivision of Kv equals :Def5: :: SIMPLEX1:def 5

subdivision ((center_of_mass V),Kv);

coherence subdivision ((center_of_mass V),Kv);

subdivision ((center_of_mass V),Kv) is non void Subdivision of Kv

proof end;

:: deftheorem Def5 defines BCS SIMPLEX1:def 5 :

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

BCS Kv = subdivision ((center_of_mass V),Kv);

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

BCS Kv = subdivision ((center_of_mass V),Kv);

definition

let n be Nat;

let V be RealLinearSpace;

let Kv be non void SimplicialComplex of V;

assume A1: |.Kv.| c= [#] Kv ;

subdivision (n,(center_of_mass V),Kv) is non void Subdivision of Kv

end;
let V be RealLinearSpace;

let Kv be non void SimplicialComplex of V;

assume A1: |.Kv.| c= [#] Kv ;

func BCS (n,Kv) -> non void Subdivision of Kv equals :Def6: :: SIMPLEX1:def 6

subdivision (n,(center_of_mass V),Kv);

coherence subdivision (n,(center_of_mass V),Kv);

subdivision (n,(center_of_mass V),Kv) is non void Subdivision of Kv

proof end;

:: deftheorem Def6 defines BCS SIMPLEX1:def 6 :

for n being Nat

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

BCS (n,Kv) = subdivision (n,(center_of_mass V),Kv);

for n being Nat

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

BCS (n,Kv) = subdivision (n,(center_of_mass V),Kv);

theorem Th16: :: SIMPLEX1:16

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

BCS (0,Kv) = Kv

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

BCS (0,Kv) = Kv

proof end;

theorem Th17: :: SIMPLEX1:17

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

BCS (1,Kv) = BCS Kv

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

BCS (1,Kv) = BCS Kv

proof end;

theorem Th18: :: SIMPLEX1:18

for n being Nat

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

[#] (BCS (n,Kv)) = [#] Kv

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

[#] (BCS (n,Kv)) = [#] Kv

proof end;

theorem :: SIMPLEX1:19

theorem Th20: :: SIMPLEX1:20

for n being Nat

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

BCS ((n + 1),Kv) = BCS (BCS (n,Kv))

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

BCS ((n + 1),Kv) = BCS (BCS (n,Kv))

proof end;

theorem Th21: :: SIMPLEX1:21

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv & degree Kv <= 0 holds

TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv & degree Kv <= 0 holds

TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv

proof end;

theorem Th22: :: SIMPLEX1:22

for n being Nat

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st n > 0 & |.Kv.| c= [#] Kv & degree Kv <= 0 holds

TopStruct(# the carrier of Kv, the topology of Kv #) = BCS (n,Kv)

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st n > 0 & |.Kv.| c= [#] Kv & degree Kv <= 0 holds

TopStruct(# the carrier of Kv, the topology of Kv #) = BCS (n,Kv)

proof end;

theorem Th23: :: SIMPLEX1:23

for n being Nat

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V

for Sv being non void SubSimplicialComplex of Kv st |.Kv.| c= [#] Kv & |.Sv.| c= [#] Sv holds

BCS (n,Sv) is SubSimplicialComplex of BCS (n,Kv)

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V

for Sv being non void SubSimplicialComplex of Kv st |.Kv.| c= [#] Kv & |.Sv.| c= [#] Sv holds

BCS (n,Sv) is SubSimplicialComplex of BCS (n,Kv)

proof end;

theorem Th24: :: SIMPLEX1:24

for n being Nat

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

Vertices Kv c= Vertices (BCS (n,Kv))

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

Vertices Kv c= Vertices (BCS (n,Kv))

proof end;

registration

let n be Nat;

let V be RealLinearSpace;

let K be non void total SimplicialComplex of V;

coherence

BCS (n,K) is total

end;
let V be RealLinearSpace;

let K be non void total SimplicialComplex of V;

coherence

BCS (n,K) is total

proof end;

registration

let n be Nat;

let V be RealLinearSpace;

let K be non void finite-vertices total SimplicialComplex of V;

coherence

BCS (n,K) is finite-vertices

end;
let V be RealLinearSpace;

let K be non void finite-vertices total SimplicialComplex of V;

coherence

BCS (n,K) is finite-vertices

proof end;

definition

let V be RealLinearSpace;

let K be SimplicialComplexStr of V;

end;
let K be SimplicialComplexStr of V;

attr K is affinely-independent means :Def7: :: SIMPLEX1:def 7

for A being Subset of K st A is simplex-like holds

@ A is affinely-independent ;

for A being Subset of K st A is simplex-like holds

@ A is affinely-independent ;

:: deftheorem Def7 defines affinely-independent SIMPLEX1:def 7 :

for V being RealLinearSpace

for K being SimplicialComplexStr of V holds

( K is affinely-independent iff for A being Subset of K st A is simplex-like holds

@ A is affinely-independent );

for V being RealLinearSpace

for K being SimplicialComplexStr of V holds

( K is affinely-independent iff for A being Subset of K st A is simplex-like holds

@ A is affinely-independent );

definition

let RLS be non empty RLSStruct ;

let Kr be SimplicialComplexStr of RLS;

end;
let Kr be SimplicialComplexStr of RLS;

attr Kr is simplex-join-closed means :Def8: :: SIMPLEX1:def 8

for A, B being Subset of Kr st A is simplex-like & B is simplex-like holds

(conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B));

for A, B being Subset of Kr st A is simplex-like & B is simplex-like holds

(conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B));

:: deftheorem Def8 defines simplex-join-closed SIMPLEX1:def 8 :

for RLS being non empty RLSStruct

for Kr being SimplicialComplexStr of RLS holds

( Kr is simplex-join-closed iff for A, B being Subset of Kr st A is simplex-like & B is simplex-like holds

(conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) );

for RLS being non empty RLSStruct

for Kr being SimplicialComplexStr of RLS holds

( Kr is simplex-join-closed iff for A, B being Subset of Kr st A is simplex-like & B is simplex-like holds

(conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) );

registration

let V be RealLinearSpace;

coherence

for b_{1} being SimplicialComplexStr of V st b_{1} is empty-membered holds

b_{1} is affinely-independent

coherence

Complex_of F is affinely-independent

end;
coherence

for b

b

proof end;

let F be affinely-independent Subset-Family of V;coherence

Complex_of F is affinely-independent

proof end;

registration

let RLS be non empty RLSStruct ;

coherence

for b_{1} being SimplicialComplexStr of RLS st b_{1} is empty-membered holds

b_{1} is simplex-join-closed

end;
coherence

for b

b

proof end;

registration

let V be RealLinearSpace;

let I be affinely-independent Subset of V;

coherence

Complex_of {I} is simplex-join-closed

end;
let I be affinely-independent Subset of V;

coherence

Complex_of {I} is simplex-join-closed

proof end;

registration

let V be RealLinearSpace;

existence

ex b_{1} being Subset of V st

( b_{1} is 1 -element & b_{1} is affinely-independent )

end;
existence

ex b

( b

proof end;

registration

let V be RealLinearSpace;

ex b_{1} being SimplicialComplex of V st

( b_{1} is with_non-empty_element & b_{1} is finite-vertices & b_{1} is affinely-independent & b_{1} is simplex-join-closed & b_{1} is total )

end;
cluster subset-closed finite-membered finite-vertices with_non-empty_element total affinely-independent simplex-join-closed for SimplicialComplex of ;

existence ex b

( b

proof end;

registration

let V be RealLinearSpace;

let K be affinely-independent SimplicialComplexStr of V;

coherence

for b_{1} being SubSimplicialComplex of K holds b_{1} is affinely-independent

end;
let K be affinely-independent SimplicialComplexStr of V;

coherence

for b

proof end;

registration

let V be RealLinearSpace;

let K be simplex-join-closed SimplicialComplexStr of V;

coherence

for b_{1} being SubSimplicialComplex of K holds b_{1} is simplex-join-closed

end;
let K be simplex-join-closed SimplicialComplexStr of V;

coherence

for b

proof end;

theorem Th25: :: SIMPLEX1:25

for V being RealLinearSpace

for K being subset-closed SimplicialComplexStr of V holds

( K is simplex-join-closed iff for A, B being Subset of K st A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) holds

A = B )

for K being subset-closed SimplicialComplexStr of V holds

( K is simplex-join-closed iff for A, B being Subset of K st A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) holds

A = B )

proof end;

registration

let V be RealLinearSpace;

let Ka be non void affinely-independent SimplicialComplex of V;

let S be Simplex of Ka;

coherence

@ S is affinely-independent by Def7;

end;
let Ka be non void affinely-independent SimplicialComplex of V;

let S be Simplex of Ka;

coherence

@ S is affinely-independent by Def7;

theorem Th26: :: SIMPLEX1:26

for V being RealLinearSpace

for Ks being simplex-join-closed SimplicialComplex of V

for As, Bs being Subset of Ks st As is simplex-like & Bs is simplex-like & Int (@ As) meets conv (@ Bs) holds

As c= Bs

for Ks being simplex-join-closed SimplicialComplex of V

for As, Bs being Subset of Ks st As is simplex-like & Bs is simplex-like & Int (@ As) meets conv (@ Bs) holds

As c= Bs

proof end;

theorem :: SIMPLEX1:27

for V being RealLinearSpace

for Ks being simplex-join-closed SimplicialComplex of V

for As, Bs being Subset of Ks st As is simplex-like & @ As is affinely-independent & Bs is simplex-like holds

( Int (@ As) c= conv (@ Bs) iff As c= Bs )

for Ks being simplex-join-closed SimplicialComplex of V

for As, Bs being Subset of Ks st As is simplex-like & @ As is affinely-independent & Bs is simplex-like holds

( Int (@ As) c= conv (@ Bs) iff As c= Bs )

proof end;

theorem Th28: :: SIMPLEX1:28

for V being RealLinearSpace

for Ka being non void affinely-independent SimplicialComplex of V st |.Ka.| c= [#] Ka holds

BCS Ka is affinely-independent

for Ka being non void affinely-independent SimplicialComplex of V st |.Ka.| c= [#] Ka holds

BCS Ka is affinely-independent

proof end;

registration

let V be RealLinearSpace;

let Ka be non void total affinely-independent SimplicialComplex of V;

coherence

BCS Ka is affinely-independent

coherence

BCS (n,Ka) is affinely-independent

end;
let Ka be non void total affinely-independent SimplicialComplex of V;

coherence

BCS Ka is affinely-independent

proof end;

let n be Nat;coherence

BCS (n,Ka) is affinely-independent

proof end;

registration

let V be RealLinearSpace;

let Kas be non void affinely-independent simplex-join-closed SimplicialComplex of V;

coherence

(center_of_mass V) | the topology of Kas is one-to-one

end;
let Kas be non void affinely-independent simplex-join-closed SimplicialComplex of V;

coherence

(center_of_mass V) | the topology of Kas is one-to-one

proof end;

theorem Th29: :: SIMPLEX1:29

for V being RealLinearSpace

for Kas being non void affinely-independent simplex-join-closed SimplicialComplex of V st |.Kas.| c= [#] Kas holds

BCS Kas is simplex-join-closed

for Kas being non void affinely-independent simplex-join-closed SimplicialComplex of V st |.Kas.| c= [#] Kas holds

BCS Kas is simplex-join-closed

proof end;

registration

let V be RealLinearSpace;

let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V;

coherence

BCS K is simplex-join-closed

coherence

BCS (n,K) is simplex-join-closed

end;
let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V;

coherence

BCS K is simplex-join-closed

proof end;

let n be Nat;coherence

BCS (n,K) is simplex-join-closed

proof end;

theorem Th30: :: SIMPLEX1:30

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv & ( for n being Nat st n <= degree Kv holds

ex S being Simplex of Kv st

( card S = n + 1 & @ S is affinely-independent ) ) holds

degree Kv = degree (BCS Kv)

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv & ( for n being Nat st n <= degree Kv holds

ex S being Simplex of Kv st

( card S = n + 1 & @ S is affinely-independent ) ) holds

degree Kv = degree (BCS Kv)

proof end;

theorem Th31: :: SIMPLEX1:31

for V being RealLinearSpace

for Ka being non void affinely-independent SimplicialComplex of V st |.Ka.| c= [#] Ka holds

degree Ka = degree (BCS Ka)

for Ka being non void affinely-independent SimplicialComplex of V st |.Ka.| c= [#] Ka holds

degree Ka = degree (BCS Ka)

proof end;

theorem Th32: :: SIMPLEX1:32

for n being Nat

for V being RealLinearSpace

for Ka being non void affinely-independent SimplicialComplex of V st |.Ka.| c= [#] Ka holds

degree Ka = degree (BCS (n,Ka))

for V being RealLinearSpace

for Ka being non void affinely-independent SimplicialComplex of V st |.Ka.| c= [#] Ka holds

degree Ka = degree (BCS (n,Ka))

proof end;

theorem Th33: :: SIMPLEX1:33

for V being RealLinearSpace

for Kas being non void affinely-independent simplex-join-closed SimplicialComplex of V

for S being simplex-like Subset-Family of Kas st S is with_non-empty_elements holds

card S = card ((center_of_mass V) .: S)

for Kas being non void affinely-independent simplex-join-closed SimplicialComplex of V

for S being simplex-like Subset-Family of Kas st S is with_non-empty_elements holds

card S = card ((center_of_mass V) .: S)

proof end;

theorem Th34: :: SIMPLEX1:34

for V being RealLinearSpace

for Kas being non void affinely-independent simplex-join-closed SimplicialComplex of V

for S1, S2 being simplex-like Subset-Family of Kas st |.Kas.| c= [#] Kas & S1 is with_non-empty_elements & (center_of_mass V) .: S2 is Simplex of (BCS Kas) & (center_of_mass V) .: S1 c= (center_of_mass V) .: S2 holds

( S1 c= S2 & S2 is c=-linear )

for Kas being non void affinely-independent simplex-join-closed SimplicialComplex of V

for S1, S2 being simplex-like Subset-Family of Kas st |.Kas.| c= [#] Kas & S1 is with_non-empty_elements & (center_of_mass V) .: S2 is Simplex of (BCS Kas) & (center_of_mass V) .: S1 c= (center_of_mass V) .: S2 holds

( S1 c= S2 & S2 is c=-linear )

proof end;

theorem Th35: :: SIMPLEX1:35

for n being Nat

for V being RealLinearSpace

for Aff being finite affinely-independent Subset of V

for Bf being finite Subset of V

for S being finite Subset-Family of V st S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff holds

( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) )

for V being RealLinearSpace

for Aff being finite affinely-independent Subset of V

for Bf being finite Subset of V

for S being finite Subset-Family of V st S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff holds

( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) )

proof end;

theorem Th36: :: SIMPLEX1:36

for V being RealLinearSpace

for Aff being finite affinely-independent Subset of V

for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & union Sf c= Aff holds

( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds

ex x being set st

( x in Sf & card x = n ) )

for Aff being finite affinely-independent Subset of V

for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & union Sf c= Aff holds

( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds

ex x being set st

( x in Sf & card x = n ) )

proof end;

Lm1: for V being RealLinearSpace

for S being finite finite-membered Subset-Family of V st S is c=-linear & S is with_non-empty_elements & card S = card (union S) holds

for A being non empty finite Subset of V st A misses union S & (union S) \/ A is affinely-independent holds

((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)})

proof end;

theorem Th37: :: SIMPLEX1:37

for V being RealLinearSpace

for S being finite Subset-Family of V st S is c=-linear & S is with_non-empty_elements & card S = card (union S) holds

for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & (union S) \/ Af is affinely-independent & (union S) \/ Af c= Bf holds

((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ Af)}) is Simplex of card S, BCS (Complex_of {Bf})

for S being finite Subset-Family of V st S is c=-linear & S is with_non-empty_elements & card S = card (union S) holds

for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & (union S) \/ Af is affinely-independent & (union S) \/ Af c= Bf holds

((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ Af)}) is Simplex of card S, BCS (Complex_of {Bf})

proof end;

theorem Th38: :: SIMPLEX1:38

for V being RealLinearSpace

for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & card Sf = card (union Sf) holds

for v being Element of V st not v in union Sf & (union Sf) \/ {v} is affinely-independent holds

{ S1 where S1 is Simplex of card Sf, BCS (Complex_of {((union Sf) \/ {v})}) : (center_of_mass V) .: Sf c= S1 } = {(((center_of_mass V) .: Sf) \/ ((center_of_mass V) .: {((union Sf) \/ {v})}))}

for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & card Sf = card (union Sf) holds

for v being Element of V st not v in union Sf & (union Sf) \/ {v} is affinely-independent holds

{ S1 where S1 is Simplex of card Sf, BCS (Complex_of {((union Sf) \/ {v})}) : (center_of_mass V) .: Sf c= S1 } = {(((center_of_mass V) .: Sf) \/ ((center_of_mass V) .: {((union Sf) \/ {v})}))}

proof end;

theorem Th39: :: SIMPLEX1:39

for V being RealLinearSpace

for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & (card Sf) + 1 = card (union Sf) & union Sf is affinely-independent holds

card { S1 where S1 is Simplex of card Sf, BCS (Complex_of {(union Sf)}) : (center_of_mass V) .: Sf c= S1 } = 2

for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & (card Sf) + 1 = card (union Sf) & union Sf is affinely-independent holds

card { S1 where S1 is Simplex of card Sf, BCS (Complex_of {(union Sf)}) : (center_of_mass V) .: Sf c= S1 } = 2

proof end;

theorem Th40: :: SIMPLEX1:40

for V being RealLinearSpace

for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Aff being finite affinely-independent Subset of V

for B being Subset of V st Aff is Simplex of K holds

( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) )

for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Aff being finite affinely-independent Subset of V

for B being Subset of V st Aff is Simplex of K holds

( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) )

proof end;

theorem Th41: :: SIMPLEX1:41

for n being Nat

for V being RealLinearSpace

for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Af being finite Subset of V

for Sk being finite simplex-like Subset-Family of K st Sk is with_non-empty_elements & (card Sk) + n <= degree K holds

( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st

( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) )

for V being RealLinearSpace

for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Af being finite Subset of V

for Sk being finite simplex-like Subset-Family of K st Sk is with_non-empty_elements & (card Sk) + n <= degree K holds

( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st

( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) )

proof end;

theorem Th42: :: SIMPLEX1:42

for V being RealLinearSpace

for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Sk being finite simplex-like Subset-Family of K

for Ak being Simplex of K st Sk is c=-linear & Sk is with_non-empty_elements & card Sk = card (union Sk) & union Sk c= Ak & card Ak = (card Sk) + 1 holds

{ S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ Ak) ) } = {(((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: {Ak}))}

for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Sk being finite simplex-like Subset-Family of K

for Ak being Simplex of K st Sk is c=-linear & Sk is with_non-empty_elements & card Sk = card (union Sk) & union Sk c= Ak & card Ak = (card Sk) + 1 holds

{ S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ Ak) ) } = {(((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: {Ak}))}

proof end;

theorem Th43: :: SIMPLEX1:43

for V being RealLinearSpace

for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Sk being finite simplex-like Subset-Family of K st Sk is c=-linear & Sk is with_non-empty_elements & (card Sk) + 1 = card (union Sk) holds

card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2

for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Sk being finite simplex-like Subset-Family of K st Sk is c=-linear & Sk is with_non-empty_elements & (card Sk) + 1 = card (union Sk) holds

card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2

proof end;

theorem Th44: :: SIMPLEX1:44

for n being Nat

for V being RealLinearSpace

for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Af being finite Subset of V st K is Subdivision of Complex_of {Af} & card Af = n + 1 & degree K = n & ( for S being Simplex of n - 1,K

for X being set st X = { S1 where S1 is Simplex of n,K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) ) ) holds

for S being Simplex of n - 1, BCS K

for X being set st X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) )

for V being RealLinearSpace

for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Af being finite Subset of V st K is Subdivision of Complex_of {Af} & card Af = n + 1 & degree K = n & ( for S being Simplex of n - 1,K

for X being set st X = { S1 where S1 is Simplex of n,K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) ) ) holds

for S being Simplex of n - 1, BCS K

for X being set st X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) )

proof end;

theorem Th45: :: SIMPLEX1:45

for X being set

for n, k being Nat

for V being RealLinearSpace

for Aff being finite affinely-independent Subset of V

for S being Simplex of n - 1, BCS (k,(Complex_of {Aff})) st card Aff = n + 1 & X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } holds

( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )

for n, k being Nat

for V being RealLinearSpace

for Aff being finite affinely-independent Subset of V

for S being Simplex of n - 1, BCS (k,(Complex_of {Aff})) st card Aff = n + 1 & X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } holds

( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )

proof end;

theorem Th46: :: SIMPLEX1:46

for k being Nat

for V being RealLinearSpace

for Aff being finite affinely-independent Subset of V

for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))

for B being Subset of V st B c= Aff & v in conv B holds

F . v in B ) holds

ex n being Nat st card { S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff } = (2 * n) + 1

for V being RealLinearSpace

for Aff being finite affinely-independent Subset of V

for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))

for B being Subset of V st B c= Aff & v in conv B holds

F . v in B ) holds

ex n being Nat st card { S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff } = (2 * n) + 1

proof end;

:: Sperner's Lemma

theorem :: SIMPLEX1:47

for k being Nat

for V being RealLinearSpace

for Aff being finite affinely-independent Subset of V

for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))

for B being Subset of V st B c= Aff & v in conv B holds

F . v in B ) holds

ex S being Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) st F .: S = Aff

for V being RealLinearSpace

for Aff being finite affinely-independent Subset of V

for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))

for B being Subset of V st B c= Aff & v in conv B holds

F . v in B ) holds

ex S being Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) st F .: S = Aff

proof end;