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

proof

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

proof

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;

let A be Subset of C; :: thesis: ( A is simplex-like implies ex B being Subset of K st
( 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;

hence Complex_of SF is SubdivisionStr of K ; :: thesis: verum