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

let K be subset-closed SimplicialComplexStr of V; :: thesis: for SF being Subset-Family of K st SF = Sub_of_Fin the topology of K holds

Complex_of SF is SubdivisionStr of K

set TOP = the topology of K;

let SF be Subset-Family of K; :: thesis: ( SF = Sub_of_Fin the topology of K implies Complex_of SF is SubdivisionStr of K )

assume A1: SF = Sub_of_Fin the topology of K ; :: thesis: Complex_of SF is SubdivisionStr of K

set C = Complex_of SF;

( [#] (Complex_of SF) = [#] K & [#] K c= the carrier of V ) by SIMPLEX0:def 9;

then reconsider C = Complex_of SF as SimplicialComplexStr of V by SIMPLEX0:def 9;

A2: the_family_of K is subset-closed ;

then A3: the topology of C = SF by A1, SIMPLEX0:7;

C is SubdivisionStr of K

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

Complex_of SF is SubdivisionStr of K

let K be subset-closed SimplicialComplexStr of V; :: thesis: for SF being Subset-Family of K st SF = Sub_of_Fin the topology of K holds

Complex_of SF is SubdivisionStr of K

set TOP = the topology of K;

let SF be Subset-Family of K; :: thesis: ( SF = Sub_of_Fin the topology of K implies Complex_of SF is SubdivisionStr of K )

assume A1: SF = Sub_of_Fin the topology of K ; :: thesis: Complex_of SF is SubdivisionStr of K

set C = Complex_of SF;

( [#] (Complex_of SF) = [#] K & [#] K c= the carrier of V ) by SIMPLEX0:def 9;

then reconsider C = Complex_of SF as SimplicialComplexStr of V by SIMPLEX0:def 9;

A2: the_family_of K is subset-closed ;

then A3: the topology of C = SF by A1, SIMPLEX0:7;

C is SubdivisionStr of K

proof

hence
Complex_of SF is SubdivisionStr of K
; :: thesis: verum
thus
|.K.| c= |.C.|
:: according to SIMPLEX1:def 4 :: thesis: for A being Subset of C st A is simplex-like holds

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

reconsider B = A as Subset of K ;

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

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

then A in the topology of C ;

then A10: B is simplex-like by A1, A3;

@ A = @ B ;

hence ex B being Subset of K st

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

end;ex B being Subset of K st

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

proof

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

assume x in |.K.| ; :: thesis: x in |.C.|

then consider S being Subset of K such that

A4: S is simplex-like and

A5: x in conv (@ S) by Def3;

reconsider S1 = @ S as non empty Subset of V by A5;

x in { (Sum L) where L is Convex_Combination of S1 : L in ConvexComb V } by A5, CONVEX3:5;

then consider L being Convex_Combination of S1 such that

A6: ( x = Sum L & L in ConvexComb V ) ;

reconsider Carr = Carrier L as non empty Subset of V by CONVEX1:21;

A7: Carr c= S by RLVECT_2:def 6;

then reconsider Carr1 = Carr as Subset of C by XBOOLE_1:1;

S in the topology of K by A4;

then Carr1 in the topology of K by A2, A7, CLASSES1:def 1;

then Carr1 in the topology of C by A1, A3, COHSP_1:def 3;

then A8: Carr1 is simplex-like ;

reconsider LC = L as Linear_Combination of Carr by RLVECT_2:def 6;

LC is convex ;

then x in { (Sum M) where M is Convex_Combination of Carr : M in ConvexComb V } by A6;

then A9: x in conv Carr by CONVEX3:5;

Carr = @ Carr1 ;

hence x in |.C.| by A8, A9, Def3; :: thesis: verum

end;assume x in |.K.| ; :: thesis: x in |.C.|

then consider S being Subset of K such that

A4: S is simplex-like and

A5: x in conv (@ S) by Def3;

reconsider S1 = @ S as non empty Subset of V by A5;

x in { (Sum L) where L is Convex_Combination of S1 : L in ConvexComb V } by A5, CONVEX3:5;

then consider L being Convex_Combination of S1 such that

A6: ( x = Sum L & L in ConvexComb V ) ;

reconsider Carr = Carrier L as non empty Subset of V by CONVEX1:21;

A7: Carr c= S by RLVECT_2:def 6;

then reconsider Carr1 = Carr as Subset of C by XBOOLE_1:1;

S in the topology of K by A4;

then Carr1 in the topology of K by A2, A7, CLASSES1:def 1;

then Carr1 in the topology of C by A1, A3, COHSP_1:def 3;

then A8: Carr1 is simplex-like ;

reconsider LC = L as Linear_Combination of Carr by RLVECT_2:def 6;

LC is convex ;

then x in { (Sum M) where M is Convex_Combination of Carr : M in ConvexComb V } by A6;

then A9: x in conv Carr by CONVEX3:5;

Carr = @ Carr1 ;

hence x in |.C.| by A8, A9, Def3; :: thesis: verum

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

reconsider B = A as Subset of K ;

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

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

then A in the topology of C ;

then A10: B is simplex-like by A1, A3;

@ A = @ B ;

hence ex B being Subset of K st

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