let RLS be non empty RLSStruct ; :: thesis: for Kr being SimplicialComplexStr of RLS holds Complex_of the topology of Kr is SubdivisionStr of Kr

let Kr be SimplicialComplexStr of RLS; :: thesis: Complex_of the topology of Kr is SubdivisionStr of Kr

set TOP = the topology of Kr;

set C = Complex_of the topology of Kr;

( [#] (Complex_of the topology of Kr) = [#] Kr & [#] Kr c= the carrier of RLS ) by SIMPLEX0:def 9;

then reconsider C = Complex_of the topology of Kr as SimplicialComplexStr of RLS by SIMPLEX0:def 9;

A1: |.Kr.| c= |.C.|

ex B being Subset of Kr st

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

let Kr be SimplicialComplexStr of RLS; :: thesis: Complex_of the topology of Kr is SubdivisionStr of Kr

set TOP = the topology of Kr;

set C = Complex_of the topology of Kr;

( [#] (Complex_of the topology of Kr) = [#] Kr & [#] Kr c= the carrier of RLS ) by SIMPLEX0:def 9;

then reconsider C = Complex_of the topology of Kr as SimplicialComplexStr of RLS by SIMPLEX0:def 9;

A1: |.Kr.| c= |.C.|

proof

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

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

then consider A being Subset of Kr such that

A2: A is simplex-like and

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

reconsider B = A as Subset of C ;

A in the topology of Kr by A2;

then A in the topology of C by SIMPLEX0:2;

then A4: B is simplex-like ;

@ A = @ B ;

hence x in |.C.| by A3, A4, Def3; :: thesis: verum

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

then consider A being Subset of Kr such that

A2: A is simplex-like and

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

reconsider B = A as Subset of C ;

A in the topology of Kr by A2;

then A in the topology of C by SIMPLEX0:2;

then A4: B is simplex-like ;

@ A = @ B ;

hence x in |.C.| by A3, A4, Def3; :: thesis: verum

ex B being Subset of Kr st

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

proof

hence
Complex_of the topology of Kr is SubdivisionStr of Kr
by A1, Def4; :: thesis: verum
let A be Subset of C; :: thesis: ( A is simplex-like implies ex B being Subset of Kr st

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

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

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

then A in the topology of C ;

then consider B being set such that

A5: A c= B and

A6: B in the topology of Kr by SIMPLEX0:2;

reconsider B = B as Subset of Kr by A6;

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

thus ( B is simplex-like & conv (@ A) c= conv (@ B) ) by A5, A6, RLAFFIN1:3; :: thesis: verum

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

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

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

then A in the topology of C ;

then consider B being set such that

A5: A c= B and

A6: B in the topology of Kr by SIMPLEX0:2;

reconsider B = B as Subset of Kr by A6;

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

thus ( B is simplex-like & conv (@ A) c= conv (@ B) ) by A5, A6, RLAFFIN1:3; :: thesis: verum