let X be set ; for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function
for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds
subdivision (P,SX) = (subdivision (P,KX)) | A
let KX be SimplicialComplexStr of X; for SX being SubSimplicialComplex of KX
for P being Function
for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds
subdivision (P,SX) = (subdivision (P,KX)) | A
let SX be SubSimplicialComplex of KX; for P being Function
for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds
subdivision (P,SX) = (subdivision (P,KX)) | A
let P be Function; for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds
subdivision (P,SX) = (subdivision (P,KX)) | A
set PK = subdivision (P,KX);
reconsider PS = subdivision (P,SX) as strict SubSimplicialComplex of subdivision (P,KX) by Th58;
let A be Subset of (subdivision (P,KX)); ( dom P c= the topology of SX & A = [#] SX implies subdivision (P,SX) = (subdivision (P,KX)) | A )
assume that
A1:
dom P c= the topology of SX
and
A2:
A = [#] SX
; subdivision (P,SX) = (subdivision (P,KX)) | A
then A6:
PS is maximal
;
[#] PS = [#] SX
by Def20;
hence
subdivision (P,SX) = (subdivision (P,KX)) | A
by A2, A6, Def16; verum