begin
theorem
theorem
begin
:: deftheorem TRIANG_1:def 1 :
canceled;
:: deftheorem defines symplexes TRIANG_1:def 2 :
theorem
canceled;
theorem
canceled;
theorem Th5:
theorem
theorem Th7:
theorem
canceled;
theorem
canceled;
theorem Th10:
begin
:: deftheorem Def4 defines lower_non-empty TRIANG_1:def 3 :
:: deftheorem Def5 defines FuncsSeq TRIANG_1:def 4 :
:: deftheorem defines @ TRIANG_1:def 5 :
:: deftheorem Def7 defines NatEmbSeq TRIANG_1:def 6 :
:: deftheorem TRIANG_1:def 7 :
canceled;
:: deftheorem Def9 defines lower_non-empty TRIANG_1:def 8 :
begin
definition
let T be
lower_non-empty TriangStr ;
let n be
Nat;
let x be
Symplex of
T,
(n + 1);
let f be
Face of
n;
assume A1:
the
SkeletonSeq of
T . (n + 1) <> {}
;
func face x,
f -> Symplex of
T,
n means :
Def10:
for
F,
G being
Function st
F = the
FacesAssign of
T . n &
G = F . f holds
it = G . x;
existence
ex b1 being Symplex of T,n st
for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b1 = G . x
uniqueness
for b1, b2 being Symplex of T,n st ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b1 = G . x ) & ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b2 = G . x ) holds
b1 = b2
end;
:: deftheorem Def10 defines face TRIANG_1:def 9 :
definition
let C be non
empty Poset;
func Triang C -> strict lower_non-empty TriangStr means
( the
SkeletonSeq of
it . 0 = {{} } & ( for
n being
Nat st
n > 0 holds
the
SkeletonSeq of
it . n = { (SgmX the InternalRel of C,A) where A is non empty Element of symplexes C : card A = n } ) & ( for
n being
Nat for
f being
Face of
n for
s being
Element of the
SkeletonSeq of
it . (n + 1) st
s in the
SkeletonSeq of
it . (n + 1) holds
for
A being non
empty Element of
symplexes C st
SgmX the
InternalRel of
C,
A = s holds
face s,
f = (SgmX the InternalRel of C,A) * f ) );
existence
ex b1 being strict lower_non-empty TriangStr st
( the SkeletonSeq of b1 . 0 = {{} } & ( for n being Nat st n > 0 holds
the SkeletonSeq of b1 . n = { (SgmX the InternalRel of C,A) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of b1 . (n + 1) st s in the SkeletonSeq of b1 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX the InternalRel of C,A = s holds
face s,f = (SgmX the InternalRel of C,A) * f ) )
uniqueness
for b1, b2 being strict lower_non-empty TriangStr st the SkeletonSeq of b1 . 0 = {{} } & ( for n being Nat st n > 0 holds
the SkeletonSeq of b1 . n = { (SgmX the InternalRel of C,A) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of b1 . (n + 1) st s in the SkeletonSeq of b1 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX the InternalRel of C,A = s holds
face s,f = (SgmX the InternalRel of C,A) * f ) & the SkeletonSeq of b2 . 0 = {{} } & ( for n being Nat st n > 0 holds
the SkeletonSeq of b2 . n = { (SgmX the InternalRel of C,A) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of b2 . (n + 1) st s in the SkeletonSeq of b2 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX the InternalRel of C,A = s holds
face s,f = (SgmX the InternalRel of C,A) * f ) holds
b1 = b2
end;
:: deftheorem defines Triang TRIANG_1:def 10 :