let V be RealLinearSpace; :: thesis: 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

let K be with_empty_element SimplicialComplex of V; :: thesis: ( |.K.| c= [#] K implies 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 )

assume A1: |.K.| c= [#] K ; :: thesis: 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

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

B . S in conv (@ S) ) implies subdivision (B,K) is SubdivisionStr of K )

assume A2: for S being Simplex of K st not S is empty holds

B . S in conv (@ S) ; :: thesis: subdivision (B,K) is SubdivisionStr of K

set P = subdivision (B,K);

defpred S_{1}[ Nat] means for x being set

for A being Simplex of K st x in conv (@ A) & card A = $1 holds

ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A );

A3: dom B = BOOL the carrier of V by FUNCT_2:def 1;

A4: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A32, A4);

thus |.K.| c= |.(subdivision (B,K)).| :: according to SIMPLEX1:def 4 :: thesis: for A being Subset of (subdivision (B,K)) st A is simplex-like holds

ex B being Subset of K st

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

ex B being Subset of K st

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

ex B being Subset of K st

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

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

let K be with_empty_element SimplicialComplex of V; :: thesis: ( |.K.| c= [#] K implies 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 )

assume A1: |.K.| c= [#] K ; :: thesis: 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

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

B . S in conv (@ S) ) implies subdivision (B,K) is SubdivisionStr of K )

assume A2: for S being Simplex of K st not S is empty holds

B . S in conv (@ S) ; :: thesis: subdivision (B,K) is SubdivisionStr of K

set P = subdivision (B,K);

defpred S

for A being Simplex of K st x in conv (@ A) & card A = $1 holds

ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A );

A3: dom B = BOOL the carrier of V by FUNCT_2:def 1;

A4: for n being Nat st S

S

proof

A32:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A5: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let x be set ; :: thesis: for A being Simplex of K st x in conv (@ A) & card A = n + 1 holds

ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A )

let A be Simplex of K; :: thesis: ( x in conv (@ A) & card A = n + 1 implies ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A ) )

assume that

A6: x in conv (@ A) and

A7: card A = n + 1 ; :: thesis: ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A )

reconsider A1 = @ A as non empty Subset of V by A6;

A8: union {A} = A by ZFMISC_1:25;

A9: for P being Subset of K st P in {A} holds

P is simplex-like by TARSKI:def 1;

then A10: {A} is simplex-like ;

A11: B . A1 in conv (@ A) by A2;

then reconsider BA = B . A as Element of V ;

A1 = A ;

then A12: A in dom B by A3, ZFMISC_1:56;

A13: B .: {A} = Im (B,A) by RELAT_1:def 16;

then A14: B .: {A} = {BA} by A12, FUNCT_1:59;

( BA in conv A1 & conv A1 c= |.K.| ) by A2, Th5;

then BA in |.K.| ;

then ( [#] (subdivision (B,K)) = [#] K & {BA} is Subset of K ) by A1, SIMPLEX0:def 20, ZFMISC_1:31;

then reconsider BY = B .: {A} as Subset of (subdivision (B,K)) by A12, A13, FUNCT_1:59;

end;assume A5: S

let x be set ; :: thesis: for A being Simplex of K st x in conv (@ A) & card A = n + 1 holds

ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A )

let A be Simplex of K; :: thesis: ( x in conv (@ A) & card A = n + 1 implies ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A ) )

assume that

A6: x in conv (@ A) and

A7: card A = n + 1 ; :: thesis: ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A )

reconsider A1 = @ A as non empty Subset of V by A6;

A8: union {A} = A by ZFMISC_1:25;

A9: for P being Subset of K st P in {A} holds

P is simplex-like by TARSKI:def 1;

then A10: {A} is simplex-like ;

A11: B . A1 in conv (@ A) by A2;

then reconsider BA = B . A as Element of V ;

A1 = A ;

then A12: A in dom B by A3, ZFMISC_1:56;

A13: B .: {A} = Im (B,A) by RELAT_1:def 16;

then A14: B .: {A} = {BA} by A12, FUNCT_1:59;

( BA in conv A1 & conv A1 c= |.K.| ) by A2, Th5;

then BA in |.K.| ;

then ( [#] (subdivision (B,K)) = [#] K & {BA} is Subset of K ) by A1, SIMPLEX0:def 20, ZFMISC_1:31;

then reconsider BY = B .: {A} as Subset of (subdivision (B,K)) by A12, A13, FUNCT_1:59;

per cases
( x = B . A or x <> B . A )
;

end;

suppose A15:
x = B . A
; :: thesis: ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A )

take Y ; :: thesis: ex BS being Subset of (subdivision (B,K)) st

( BS = B .: Y & x in conv (@ BS) & union Y c= A )

take BY ; :: thesis: ( BY = B .: Y & x in conv (@ BY) & union Y c= A )

conv {BA} = {BA} by RLAFFIN1:1;

hence ( BY = B .: Y & x in conv (@ BY) & union Y c= A ) by A14, A15, TARSKI:def 1, ZFMISC_1:25; :: thesis: verum

end;

( BS = B .: S & x in conv (@ BS) & union S c= A )

now :: thesis: for x1, x2 being set st x1 in {A} & x2 in {A} holds

x1,x2 are_c=-comparable

then reconsider Y = {A} as c=-linear finite simplex-like Subset-Family of K by A9, ORDINAL1:def 8, TOPS_2:def 1;x1,x2 are_c=-comparable

let x1, x2 be set ; :: thesis: ( x1 in {A} & x2 in {A} implies x1,x2 are_c=-comparable )

assume that

A16: x1 in {A} and

A17: x2 in {A} ; :: thesis: x1,x2 are_c=-comparable

x1 = A by A16, TARSKI:def 1;

hence x1,x2 are_c=-comparable by A17, TARSKI:def 1; :: thesis: verum

end;assume that

A16: x1 in {A} and

A17: x2 in {A} ; :: thesis: x1,x2 are_c=-comparable

x1 = A by A16, TARSKI:def 1;

hence x1,x2 are_c=-comparable by A17, TARSKI:def 1; :: thesis: verum

take Y ; :: thesis: ex BS being Subset of (subdivision (B,K)) st

( BS = B .: Y & x in conv (@ BS) & union Y c= A )

take BY ; :: thesis: ( BY = B .: Y & x in conv (@ BY) & union Y c= A )

conv {BA} = {BA} by RLAFFIN1:1;

hence ( BY = B .: Y & x in conv (@ BY) & union Y c= A ) by A14, A15, TARSKI:def 1, ZFMISC_1:25; :: thesis: verum

suppose
x <> B . A
; :: thesis: ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A )

( BS = B .: S & x in conv (@ BS) & union S c= A )

then consider p, w being Element of V, r being Real such that

A18: p in A and

A19: w in conv (A1 \ {p}) and

A20: ( 0 <= r & r < 1 & (r * BA) + ((1 - r) * w) = x ) by A6, A11, RLAFFIN2:26;

( @ (A \ {p}) = A1 \ {p} & card (A \ {p}) = n ) by A7, A18, STIRL2_1:55;

then consider S being c=-linear finite simplex-like Subset-Family of K, BS being Subset of (subdivision (B,K)) such that

A21: BS = B .: S and

A22: w in conv (@ BS) and

A23: union S c= A \ {p} by A5, A19;

set S1 = S \/ {A};

A24: A \ {p} c= A by XBOOLE_1:36;

then A25: union S c= A by A23;

for x1, x2 being set st x1 in S \/ {A} & x2 in S \/ {A} holds

x1,x2 are_c=-comparable

A28: B .: S1 = BS \/ BY by A21, RELAT_1:120;

then reconsider BS1 = B .: S1 as Subset of (subdivision (B,K)) ;

A29: conv (@ BS) c= conv (@ BS1) by A28, RLTOPSP1:20, XBOOLE_1:7;

BA in BY by A14, TARSKI:def 1;

then A30: BA in @ BS1 by A28, XBOOLE_0:def 3;

take S1 ; :: thesis: ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S1 & x in conv (@ BS) & union S1 c= A )

take BS1 ; :: thesis: ( BS1 = B .: S1 & x in conv (@ BS1) & union S1 c= A )

A31: @ BS1 c= conv (@ BS1) by CONVEX1:41;

union S1 = (union S) \/ A by A8, ZFMISC_1:78

.= A by A23, A24, XBOOLE_1:1, XBOOLE_1:12 ;

hence ( BS1 = B .: S1 & x in conv (@ BS1) & union S1 c= A ) by A20, A22, A29, A30, A31, RLTOPSP1:def 1; :: thesis: verum

end;A18: p in A and

A19: w in conv (A1 \ {p}) and

A20: ( 0 <= r & r < 1 & (r * BA) + ((1 - r) * w) = x ) by A6, A11, RLAFFIN2:26;

( @ (A \ {p}) = A1 \ {p} & card (A \ {p}) = n ) by A7, A18, STIRL2_1:55;

then consider S being c=-linear finite simplex-like Subset-Family of K, BS being Subset of (subdivision (B,K)) such that

A21: BS = B .: S and

A22: w in conv (@ BS) and

A23: union S c= A \ {p} by A5, A19;

set S1 = S \/ {A};

A24: A \ {p} c= A by XBOOLE_1:36;

then A25: union S c= A by A23;

for x1, x2 being set st x1 in S \/ {A} & x2 in S \/ {A} holds

x1,x2 are_c=-comparable

proof

then reconsider S1 = S \/ {A} as c=-linear finite simplex-like Subset-Family of K by A10, ORDINAL1:def 8, TOPS_2:13;
let x1, x2 be set ; :: thesis: ( x1 in S \/ {A} & x2 in S \/ {A} implies x1,x2 are_c=-comparable )

assume A26: ( x1 in S \/ {A} & x2 in S \/ {A} ) ; :: thesis: x1,x2 are_c=-comparable

end;assume A26: ( x1 in S \/ {A} & x2 in S \/ {A} ) ; :: thesis: x1,x2 are_c=-comparable

per cases
( ( x1 in S & x2 in S ) or ( x1 in S & x2 in {A} ) or ( x2 in S & x1 in {A} ) or ( x1 in {A} & x2 in {A} ) )
by A26, XBOOLE_0:def 3;

end;

suppose
( x1 in S & x2 in {A} )
; :: thesis: x1,x2 are_c=-comparable

then
( x1 c= union S & x2 = A )
by TARSKI:def 1, ZFMISC_1:74;

then x1 c= x2 by A25;

hence x1,x2 are_c=-comparable ; :: thesis: verum

end;then x1 c= x2 by A25;

hence x1,x2 are_c=-comparable ; :: thesis: verum

suppose
( x2 in S & x1 in {A} )
; :: thesis: x1,x2 are_c=-comparable

then
( x2 c= union S & x1 = A )
by TARSKI:def 1, ZFMISC_1:74;

then x2 c= x1 by A25;

hence x1,x2 are_c=-comparable ; :: thesis: verum

end;then x2 c= x1 by A25;

hence x1,x2 are_c=-comparable ; :: thesis: verum

A28: B .: S1 = BS \/ BY by A21, RELAT_1:120;

then reconsider BS1 = B .: S1 as Subset of (subdivision (B,K)) ;

A29: conv (@ BS) c= conv (@ BS1) by A28, RLTOPSP1:20, XBOOLE_1:7;

BA in BY by A14, TARSKI:def 1;

then A30: BA in @ BS1 by A28, XBOOLE_0:def 3;

take S1 ; :: thesis: ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S1 & x in conv (@ BS) & union S1 c= A )

take BS1 ; :: thesis: ( BS1 = B .: S1 & x in conv (@ BS1) & union S1 c= A )

A31: @ BS1 c= conv (@ BS1) by CONVEX1:41;

union S1 = (union S) \/ A by A8, ZFMISC_1:78

.= A by A23, A24, XBOOLE_1:1, XBOOLE_1:12 ;

hence ( BS1 = B .: S1 & x in conv (@ BS1) & union S1 c= A ) by A20, A22, A29, A30, A31, RLTOPSP1:def 1; :: thesis: verum

proof

A35:
for n being Nat holds S
let x be set ; :: thesis: for A being Simplex of K st x in conv (@ A) & card A = 0 holds

ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A )

let A be Simplex of K; :: thesis: ( x in conv (@ A) & card A = 0 implies ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A ) )

assume that

A33: x in conv (@ A) and

A34: card A = 0 ; :: thesis: ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A )

not @ A is empty by A33;

hence ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A ) by A34; :: thesis: verum

end;ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A )

let A be Simplex of K; :: thesis: ( x in conv (@ A) & card A = 0 implies ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A ) )

assume that

A33: x in conv (@ A) and

A34: card A = 0 ; :: thesis: ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A )

not @ A is empty by A33;

hence ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st

( BS = B .: S & x in conv (@ BS) & union S c= A ) by A34; :: thesis: verum

thus |.K.| c= |.(subdivision (B,K)).| :: according to SIMPLEX1:def 4 :: thesis: for A being Subset of (subdivision (B,K)) st A is simplex-like holds

ex B being Subset of K st

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

proof

for A being Subset of (subdivision (B,K)) st A is simplex-like holds
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in |.K.| or x in |.(subdivision (B,K)).| )

assume x in |.K.| ; :: thesis: x in |.(subdivision (B,K)).|

then consider A being Subset of K such that

A36: A is simplex-like and

A37: x in conv (@ A) by Def3;

reconsider A = A as Simplex of K by A36;

S_{1}[ card A]
by A35;

then consider S being c=-linear finite simplex-like Subset-Family of K, BS being Subset of (subdivision (B,K)) such that

A38: BS = B .: S and

A39: x in conv (@ BS) and

union S c= A by A37;

BS is simplex-like by A38, SIMPLEX0:def 20;

then conv (@ BS) c= |.(subdivision (B,K)).| by Th5;

hence x in |.(subdivision (B,K)).| by A39; :: thesis: verum

end;assume x in |.K.| ; :: thesis: x in |.(subdivision (B,K)).|

then consider A being Subset of K such that

A36: A is simplex-like and

A37: x in conv (@ A) by Def3;

reconsider A = A as Simplex of K by A36;

S

then consider S being c=-linear finite simplex-like Subset-Family of K, BS being Subset of (subdivision (B,K)) such that

A38: BS = B .: S and

A39: x in conv (@ BS) and

union S c= A by A37;

BS is simplex-like by A38, SIMPLEX0:def 20;

then conv (@ BS) c= |.(subdivision (B,K)).| by Th5;

hence x in |.(subdivision (B,K)).| by A39; :: thesis: verum

ex B being Subset of K st

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

proof

hence
for A being Subset of (subdivision (B,K)) st A is simplex-like holds
let A be Subset of (subdivision (B,K)); :: thesis: ( A is simplex-like implies ex B being Subset of K st

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

assume A is simplex-like ; :: thesis: ex B being Subset of K st

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

then consider S being c=-linear finite simplex-like Subset-Family of K such that

A40: A = B .: S by SIMPLEX0:def 20;

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

assume A is simplex-like ; :: thesis: ex B being Subset of K st

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

then consider S being c=-linear finite simplex-like Subset-Family of K such that

A40: A = B .: S by SIMPLEX0:def 20;

per cases
( S is empty or not S is empty )
;

end;

suppose A41:
S is empty
; :: thesis: ex B being Subset of K st

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

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

take
{} K
; :: thesis: ( {} K is simplex-like & conv (@ A) c= conv (@ ({} K)) )

thus ( {} K is simplex-like & conv (@ A) c= conv (@ ({} K)) ) by A40, A41; :: thesis: verum

end;thus ( {} K is simplex-like & conv (@ A) c= conv (@ ({} K)) ) by A40, A41; :: thesis: verum

suppose A42:
not S is empty
; :: thesis: ex B being Subset of K st

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

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

take U = union S; :: thesis: ( U is simplex-like & conv (@ A) c= conv (@ U) )

A43: A c= conv (@ U)

hence ( U is simplex-like & conv (@ A) c= conv (@ U) ) by A43, CONVEX1:30, TOPS_2:def 1; :: thesis: verum

end;A43: A c= conv (@ U)

proof

U in S
by A42, SIMPLEX0:9;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in conv (@ U) )

assume x in A ; :: thesis: x in conv (@ U)

then consider y being object such that

A44: y in dom B and

A45: y in S and

A46: B . y = x by A40, FUNCT_1:def 6;

reconsider y = y as Simplex of K by A45, TOPS_2:def 1;

y <> {} by A44, ZFMISC_1:56;

then A47: B . y in conv (@ y) by A2;

conv (@ y) c= conv (@ U) by A45, RLTOPSP1:20, ZFMISC_1:74;

hence x in conv (@ U) by A46, A47; :: thesis: verum

end;assume x in A ; :: thesis: x in conv (@ U)

then consider y being object such that

A44: y in dom B and

A45: y in S and

A46: B . y = x by A40, FUNCT_1:def 6;

reconsider y = y as Simplex of K by A45, TOPS_2:def 1;

y <> {} by A44, ZFMISC_1:56;

then A47: B . y in conv (@ y) by A2;

conv (@ y) c= conv (@ U) by A45, RLTOPSP1:20, ZFMISC_1:74;

hence x in conv (@ U) by A46, A47; :: thesis: verum

hence ( U is simplex-like & conv (@ A) c= conv (@ U) ) by A43, CONVEX1:30, TOPS_2:def 1; :: thesis: verum

ex B being Subset of K st

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